Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z051)

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:

  b0(0)	→	0
  b0(1)	→	0
  a0(0)	→	1
  a0(1)	→	1
  a1(0)	→	7
  a1(7)	→	6
  b1(6)	→	5
  b1(5)	→	4
  b1(4)	→	3
  a1(3)	→	2
  a1(2)	→	0
  a1(1)	→	7
  a1(4)	→	7
  a2(5)	→	13
  a2(13)	→	12
  b2(12)	→	11
  b2(11)	→	10
  b2(10)	→	9
  a2(9)	→	8
  a2(8)	→	0
  a1(10)	→	7
  a2(6)	→	13
  a2(8)	→	10
  a2(11)	→	13
  a3(12)	→	19
  a3(19)	→	18
  b3(18)	→	17
  b3(17)	→	16
  b3(16)	→	15
  a3(15)	→	14
  a3(14)	→	10
  0	→	4
  0	→	3