Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z098)

The rewrite relation of the following TRS is considered.

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

→

b(b(b(b(a(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(b(a(a(a(x1))))))

→

a(a(a(a(b(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:

32	→	5
128	→	64
128	→	36
202	→	151
202	→	184
10	→	46
97	→	5
84	→	5
211	→	164
145	→	101
260	→	206
41	→	5
41	→	6
41	→	31
41	→	1
41	→	7
41	→	32
39	→	85
184	→	151
108	→	36
9	→	48
9	→	61
37	→	138
65	→	183
199	→	243
99	→	62
224	→	152
49	→	34
1	→	31
40	→	83
8	→	100
139	→	62
125	→	161
125	→	216
38	→	96
38	→	98
86	→	5
251	→	154
171	→	162
105	→	170
67	→	120
2	→	4
11	→	33
66	→	129
66	→	150
12	→	1
12	→	5
12	→	6
12	→	7
12	→	32
169	→	63
69	→	7
69	→	8
69	→	102
69	→	101
137	→	102
158	→	103
158	→	104
278	→	255
47	→	34
250	→	252
68	→	144
166	→	194
156	→	203
247	→	270
a₄(256)	→	257
a₄(248)	→	249
a₄(249)	→	250
a₄(247)	→	248
a₄(258)	→	259
a₄(250)	→	251
a₄(259)	→	260
a₄(257)	→	258
b₄(255)	→	256
b₄(254)	→	255
b₄(245)	→	246
b₄(243)	→	244
b₄(253)	→	254
b₄(244)	→	245
b₄(252)	→	253
b₄(246)	→	247
b₃(151)	→	152
b₃(219)	→	220
b₃(206)	→	207
b₃(150)	→	151
b₃(218)	→	219
b₃(216)	→	217
b₃(183)	→	184
b₃(217)	→	218
b₃(205)	→	206
b₃(203)	→	204
b₃(152)	→	153
b₃(194)	→	195
b₃(197)	→	198
b₃(195)	→	196
b₃(204)	→	205
b₃(196)	→	197
b₃(153)	→	154
b₁(33)	→	34
b₁(85)	→	86
b₁(5)	→	6
b₁(7)	→	8
b₁(83)	→	84
b₁(6)	→	7
b₁(31)	→	32
b₁(36)	→	37
b₁(4)	→	5
b₁(96)	→	97
b₁(46)	→	47
b₁(48)	→	49
b₁(35)	→	36
b₁(34)	→	35
a₁(11)	→	12
a₁(40)	→	41
a₁(8)	→	9
a₁(38)	→	39
a₁(9)	→	10
a₁(39)	→	40
a₁(37)	→	38
a₁(10)	→	11
a₅(277)	→	278
a₅(275)	→	276
a₅(276)	→	277
a₅(274)	→	275
b₅(273)	→	274
b₅(270)	→	271
b₅(271)	→	272
b₅(272)	→	273
a₀(1)	→	2
a₀(2)	→	2
b₂(164)	→	165
b₂(130)	→	131
b₂(132)	→	133
b₂(121)	→	122
b₂(61)	→	62
b₂(120)	→	121
b₂(122)	→	123
b₂(163)	→	164
b₂(101)	→	102
b₂(100)	→	101
b₂(131)	→	132
b₂(63)	→	64
b₂(162)	→	163
b₂(161)	→	162
b₂(138)	→	139
b₂(64)	→	65
b₂(103)	→	104
b₂(123)	→	124
b₂(98)	→	99
b₂(62)	→	63
b₂(144)	→	145
b₂(170)	→	171
b₂(102)	→	103
b₂(129)	→	130
a₃(157)	→	158
a₃(156)	→	157
a₃(220)	→	221
a₃(222)	→	223
a₃(155)	→	156
a₃(223)	→	224
a₃(198)	→	199
a₃(221)	→	222
a₃(208)	→	209
a₃(201)	→	202
a₃(154)	→	155
a₃(209)	→	210
a₃(210)	→	211
a₃(199)	→	200
a₃(200)	→	201
a₃(207)	→	208
b₀(1)	→	1
b₀(2)	→	1
a₂(66)	→	67
a₂(67)	→	68
a₂(107)	→	108
a₂(104)	→	105
a₂(134)	→	135
a₂(166)	→	167
a₂(125)	→	126
a₂(127)	→	128
a₂(124)	→	125
a₂(105)	→	106
a₂(168)	→	169
a₂(126)	→	127
a₂(106)	→	107
a₂(68)	→	69
a₂(136)	→	137
a₂(135)	→	136
a₂(165)	→	166
a₂(65)	→	66
a₂(167)	→	168
a₂(133)	→	134

The automaton is closed under rewriting as it is compatible.