Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/27131)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Bounds

• final states:

  {4}

• transitions:

  23	→	37
  23	→	54
  89	→	78
  87	→	72
  87	→	90
  87	→	78
  87	→	89
  34	→	17
  55	→	40
  20	→	71
  49	→	17
  49	→	69
  49	→	40
  49	→	20
  49	→	38
  49	→	34
  49	→	55
  26	→	4
  26	→	27
  26	→	19
  26	→	17
  38	→	17
  91	→	85
  72	→	40
  4	→	16
  28	→	24
  104	→	78
  69	→	77
  46	→	88
  43	→	103
  27	→	33
  27	→	39
  70	→	47
  12(41)	→	42
  12(44)	→	45
  12(71)	→	72
  12(39)	→	40
  12(42)	→	43
  12(47)	→	48
  12(54)	→	55
  02(46)	→	47
  02(69)	→	70
  02(43)	→	44
  22(45)	→	46
  22(40)	→	41
  22(48)	→	49
  20(4)	→	4
  00(4)	→	4
  23(78)	→	79
  23(86)	→	87
  23(83)	→	84
  13(77)	→	78
  13(88)	→	89
  13(79)	→	80
  13(85)	→	86
  13(80)	→	81
  13(82)	→	83
  13(103)	→	104
  10(4)	→	4
  11(19)	→	20
  11(37)	→	38
  11(18)	→	19
  11(24)	→	25
  11(16)	→	17
  11(33)	→	34
  11(21)	→	22
  01(23)	→	24
  01(27)	→	28
  01(20)	→	21
  03(84)	→	85
  03(90)	→	91
  03(81)	→	82
  21(22)	→	23
  21(17)	→	18
  21(25)	→	26