Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/27235)

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, 2}

• transitions:

  10(0)	→	0
  10(1)	→	0
  10(2)	→	0
  20(0)	→	1
  20(1)	→	1
  20(2)	→	1
  00(0)	→	2
  00(1)	→	2
  00(2)	→	2
  11(0)	→	10
  21(10)	→	9
  11(9)	→	8
  11(8)	→	7
  01(7)	→	6
  11(6)	→	3
  21(3)	→	5
  01(5)	→	4
  11(4)	→	3
  21(3)	→	0
  11(1)	→	10
  11(2)	→	10
  11(7)	→	10
  11(5)	→	10
  12(7)	→	18
  22(18)	→	17
  12(17)	→	16
  12(16)	→	15
  02(15)	→	14
  12(14)	→	11
  22(11)	→	13
  02(13)	→	12
  12(12)	→	11
  22(11)	→	10
  12(5)	→	18
  12(15)	→	18
  13(15)	→	26
  23(26)	→	25
  13(25)	→	24
  13(24)	→	23
  03(23)	→	22
  13(22)	→	19
  23(19)	→	21
  03(21)	→	20
  13(20)	→	19
  23(19)	→	18
  13(13)	→	26
  5	→	10
  5	→	8
  13	→	7
  13	→	18
  21	→	26