Certification Problem

Input (TPDB TRS_Standard/Rubio_04/aoto)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

1.1 Bounds

• final states:

  {0, 1}

• transitions:

  f0(0)	→	0
  f0(1)	→	0
  g0(0)	→	1
  g0(1)	→	1
  f1(0)	→	4
  g1(4)	→	2
  f1(2)	→	3
  g1(3)	→	2
  f1(2)	→	0
  f1(1)	→	4
  f2(2)	→	7
  g2(7)	→	5
  f2(5)	→	6
  g2(6)	→	5
  f2(5)	→	4
  f2(0)	→	7
  g2(7)	→	0
  f2(1)	→	7
  f1(5)	→	4
  f3(2)	→	8
  g3(8)	→	4
  f3(0)	→	8
  f3(1)	→	8
  f3(5)	→	8
  2	→	0
  2	→	4
  5	→	4
  5	→	3
  4	→	7
  4	→	6
  4	→	8