Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z001)

The rewrite relation of the following TRS is considered.

a(a(b(b(x1))))

→

b(b(b(a(a(a(x1))))))

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

b(b(a(a(x1))))

→

a(a(a(b(b(b(x1))))))

(2)

1.1 Bounds

The given TRS is match-(raise)-bounded by 5. This is shown by the following automaton.

final states:

{2, 1}

transitions:

272	→	296
33	→	5
33	→	1
33	→	6
33	→	26
102	→	46
32	→	65
89	→	29
87	→	123
214	→	144
10	→	1
10	→	5
10	→	6
10	→	26
51	→	6
51	→	7
51	→	84
51	→	47
274	→	193
96	→	84
129	→	46
129	→	102
211	→	289
145	→	178
184	→	142
50	→	107
213	→	252
108	→	46
9	→	27
147	→	47
31	→	59
31	→	67
49	→	90
49	→	109
1	→	25
8	→	41
8	→	45
127	→	155
60	→	46
26	→	5
161	→	141
161	→	48
302	→	195
237	→	143
230	→	92
230	→	111
2	→	4
258	→	180
66	→	5
114	→	162
112	→	192
140	→	110
7	→	83
295	→	254
113	→	215
182	→	208
30	→	101
42	→	5
216	→	209
158	→	261
115	→	85
115	→	86
115	→	142
48	→	141
198	→	164
160	→	224
168	→	125
68	→	5
159	→	231
267	→	226
94	→	139
228	→	268
a₄(211)	→	212
a₄(212)	→	213
a₄(234)	→	235
a₄(271)	→	272
a₄(195)	→	196
a₄(273)	→	274
a₄(256)	→	257
a₄(197)	→	198
a₄(272)	→	273
a₄(236)	→	237
a₄(196)	→	197
a₄(265)	→	266
a₄(213)	→	214
a₄(257)	→	258
a₄(266)	→	267
a₄(255)	→	256
a₄(235)	→	236
a₄(264)	→	265
b₄(231)	→	232
b₄(269)	→	270
b₄(261)	→	262
b₄(193)	→	194
b₄(209)	→	210
b₄(192)	→	193
b₄(263)	→	264
b₄(254)	→	255
b₄(233)	→	234
b₄(232)	→	233
b₄(270)	→	271
b₄(210)	→	211
b₄(253)	→	254
b₄(262)	→	263
b₄(268)	→	269
b₄(252)	→	253
b₄(194)	→	195
b₄(208)	→	209
b₄(215)	→	216
b₃(226)	→	227
b₃(225)	→	226
b₃(142)	→	143
b₃(156)	→	157
b₃(178)	→	179
b₃(179)	→	180
b₃(143)	→	144
b₃(110)	→	111
b₃(155)	→	156
b₃(109)	→	110
b₃(139)	→	140
b₃(164)	→	165
b₃(111)	→	112
b₃(163)	→	164
b₃(162)	→	163
b₃(180)	→	181
b₃(224)	→	225
b₃(141)	→	142
b₃(157)	→	158
b₁(29)	→	30
b₁(5)	→	6
b₁(41)	→	42
b₁(27)	→	28
b₁(25)	→	26
b₁(6)	→	7
b₁(65)	→	66
b₁(4)	→	5
b₁(67)	→	68
b₁(28)	→	29
a₁(31)	→	32
a₁(8)	→	9
a₁(32)	→	33
a₁(9)	→	10
a₁(7)	→	8
a₁(30)	→	31
a₅(301)	→	302
a₅(299)	→	300
a₅(293)	→	294
a₅(292)	→	293
a₅(294)	→	295
a₅(300)	→	301
b₅(290)	→	291
b₅(297)	→	298
b₅(291)	→	292
b₅(298)	→	299
b₅(296)	→	297
b₅(289)	→	290
a₀(1)	→	2
a₀(2)	→	2
b₂(124)	→	125
b₂(101)	→	102
b₂(91)	→	92
b₂(59)	→	60
b₂(107)	→	108
b₂(84)	→	85
b₂(85)	→	86
b₂(83)	→	84
b₂(45)	→	46
b₂(92)	→	93
b₂(90)	→	91
b₂(47)	→	48
b₂(125)	→	126
b₂(46)	→	47
b₂(123)	→	124
a₃(167)	→	168
a₃(114)	→	115
a₃(227)	→	228
a₃(146)	→	147
a₃(166)	→	167
a₃(113)	→	114
a₃(159)	→	160
a₃(181)	→	182
a₃(112)	→	113
a₃(228)	→	229
a₃(165)	→	166
a₃(183)	→	184
a₃(229)	→	230
a₃(145)	→	146
a₃(144)	→	145
a₃(158)	→	159
a₃(160)	→	161
a₃(182)	→	183
b₀(1)	→	1
b₀(2)	→	1
a₂(94)	→	95
a₂(95)	→	96
a₂(93)	→	94
a₂(127)	→	128
a₂(48)	→	49
a₂(88)	→	89
a₂(126)	→	127
a₂(86)	→	87
a₂(87)	→	88
a₂(49)	→	50
a₂(50)	→	51
a₂(128)	→	129

The automaton is closed under rewriting as it is compatible.