Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z027)

The rewrite relation of the following TRS is considered.

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

→

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

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{2, 1}

transitions:

78	→	45
32	→	5
205	→	225
89	→	162
152	→	171
10	→	44
10	→	55
51	→	57
51	→	154
97	→	58
108	→	60
108	→	86
108	→	148
9	→	77
65	→	56
65	→	9
65	→	45
65	→	7
65	→	47
107	→	145
107	→	198
224	→	174
62	→	158
49	→	100
1	→	31
197	→	148
197	→	201
179	→	123
233	→	167
91	→	49
170	→	103
251	→	228
150	→	216
153	→	119
52	→	7
52	→	60
105	→	189
67	→	58
2	→	4
11	→	42
11	→	66
63	→	118
12	→	1
12	→	7
12	→	5
126	→	47
64	→	83
64	→	96
159	→	101
206	→	163
203	→	243
43	→	5
56	→	5
155	→	146
a₄(221)	→	222
a₄(190)	→	191
a₄(203)	→	204
a₄(169)	→	170
a₄(174)	→	175
a₄(195)	→	196
a₄(222)	→	223
a₄(167)	→	168
a₄(165)	→	166
a₄(199)	→	200
a₄(201)	→	202
a₄(204)	→	205
a₄(177)	→	178
a₄(205)	→	206
a₄(196)	→	197
a₄(163)	→	164
a₄(178)	→	179
a₄(223)	→	224
a₄(176)	→	177
a₄(192)	→	193
a₄(172)	→	173
a₄(168)	→	169
a₄(194)	→	195
a₄(217)	→	218
a₄(219)	→	220
b₄(175)	→	176
b₄(193)	→	194
b₄(202)	→	203
b₄(162)	→	163
b₄(173)	→	174
b₄(218)	→	219
b₄(220)	→	221
b₄(164)	→	165
b₄(198)	→	199
b₄(191)	→	192
b₄(200)	→	201
b₄(216)	→	217
b₄(166)	→	167
b₄(189)	→	190
b₄(171)	→	172
b₃(100)	→	101
b₃(147)	→	148
b₃(85)	→	86
b₃(118)	→	119
b₃(149)	→	150
b₃(120)	→	121
b₃(158)	→	159
b₃(87)	→	88
b₃(104)	→	105
b₃(154)	→	155
b₃(145)	→	146
b₃(83)	→	84
b₃(102)	→	103
b₃(122)	→	123
b₁(8)	→	9
b₁(6)	→	7
b₁(31)	→	32
b₁(55)	→	56
b₁(4)	→	5
b₁(42)	→	43
a₁(11)	→	12
a₁(9)	→	10
a₁(7)	→	8
a₁(5)	→	6
a₁(10)	→	11
a₅(246)	→	247
a₅(244)	→	245
a₅(230)	→	231
a₅(226)	→	227
a₅(248)	→	249
a₅(232)	→	233
a₅(249)	→	250
a₅(250)	→	251
a₅(228)	→	229
a₅(231)	→	232
b₅(229)	→	230
b₅(247)	→	248
b₅(227)	→	228
b₅(225)	→	226
b₅(243)	→	244
b₅(245)	→	246
a₀(1)	→	2
a₀(2)	→	2
b₂(96)	→	97
b₂(61)	→	62
b₂(44)	→	45
b₂(57)	→	58
b₂(59)	→	60
b₂(48)	→	49
b₂(46)	→	47
b₂(77)	→	78
b₂(66)	→	67
a₃(123)	→	124
a₃(90)	→	91
a₃(146)	→	147
a₃(105)	→	106
a₃(152)	→	153
a₃(107)	→	108
a₃(124)	→	125
a₃(151)	→	152
a₃(150)	→	151
a₃(89)	→	90
a₃(84)	→	85
a₃(86)	→	87
a₃(125)	→	126
a₃(121)	→	122
a₃(101)	→	102
a₃(103)	→	104
a₃(106)	→	107
a₃(88)	→	89
a₃(148)	→	149
a₃(119)	→	120
b₀(1)	→	1
b₀(2)	→	1
a₂(64)	→	65
a₂(47)	→	48
a₂(58)	→	59
a₂(60)	→	61
a₂(63)	→	64
a₂(45)	→	46
a₂(51)	→	52
a₂(49)	→	50
a₂(62)	→	63
a₂(50)	→	51

The automaton is closed under rewriting as it is compatible.