Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z040)

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:

  {2, 1}

• transitions:

  78	→	7
  78	→	40
  78	→	70
  102	→	5
  152	→	38
  10	→	37
  136	→	43
  133	→	151
  133	→	153
  146	→	40
  9	→	57
  59	→	137
  34	→	5
  130	→	157
  62	→	127
  1	→	33
  13	→	1
  13	→	7
  13	→	10
  13	→	5
  13	→	58
  13	→	70
  60	→	149
  36	→	6
  150	→	71
  6	→	69
  2	→	4
  11	→	35
  66	→	10
  66	→	43
  66	→	58
  63	→	101
  63	→	147
  100	→	39
  64	→	99
  46	→	11
  46	→	34
  46	→	8
  46	→	38
  46	→	12
  158	→	139
  154	→	129
  148	→	59
  a3(137)	→	138
  a3(144)	→	145
  a3(142)	→	143
  a3(130)	→	131
  a3(132)	→	133
  a3(143)	→	144
  a3(134)	→	135
  a3(129)	→	130
  a3(139)	→	140
  a3(140)	→	141
  a3(127)	→	128
  a3(133)	→	134
  a1(33)	→	34
  a1(7)	→	8
  a1(9)	→	10
  a1(10)	→	11
  a1(6)	→	7
  a1(101)	→	102
  a1(4)	→	5
  a1(11)	→	12
  b1(35)	→	36
  b1(8)	→	9
  b1(12)	→	13
  b1(5)	→	6
  b0(1)	→	2
  b0(2)	→	2
  a2(44)	→	45
  a2(37)	→	38
  a2(40)	→	41
  a2(75)	→	76
  a2(76)	→	77
  a2(39)	→	40
  a2(63)	→	64
  a2(57)	→	58
  a2(59)	→	60
  a2(64)	→	65
  a2(43)	→	44
  a2(151)	→	152
  a2(74)	→	75
  a2(42)	→	43
  a2(60)	→	61
  a2(71)	→	72
  a2(62)	→	63
  a2(69)	→	70
  a2(72)	→	73
  b3(157)	→	158
  b3(128)	→	129
  b3(131)	→	132
  b3(138)	→	139
  b3(135)	→	136
  b3(141)	→	142
  b3(145)	→	146
  b3(153)	→	154
  a0(1)	→	1
  a0(2)	→	1
  b2(38)	→	39
  b2(77)	→	78
  b2(58)	→	59
  b2(41)	→	42
  b2(99)	→	100
  b2(70)	→	71
  b2(45)	→	46
  b2(73)	→	74
  b2(147)	→	148
  b2(61)	→	62
  b2(149)	→	150
  b2(65)	→	66