Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z029)

The rewrite relation of the following TRS is considered.

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

→

a(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 4. This is shown by the following automaton.

final states:

{2, 1}

transitions:

205	→	274
10	→	36
10	→	64
211	→	105
119	→	258
122	→	196
120	→	210
9	→	66
147	→	260
59	→	5
65	→	5
275	→	225
175	→	131
243	→	109
1	→	34
123	→	39
123	→	9
123	→	7
123	→	37
123	→	65
165	→	69
13	→	1
13	→	7
13	→	5
197	→	37
135	→	152
135	→	224
73	→	166
76	→	128
269	→	201
79	→	69
233	→	105
150	→	198
207	→	71
207	→	227
121	→	164
121	→	280
277	→	225
153	→	69
75	→	114
75	→	142
67	→	37
2	→	4
11	→	62
11	→	78
45	→	7
45	→	71
281	→	143
63	→	5
12	→	58
77	→	65
77	→	9
77	→	37
77	→	7
77	→	39
113	→	39
137	→	71
137	→	7
35	→	5
231	→	234
74	→	104
259	→	105
43	→	68
43	→	276
151	→	41
a₄(239)	→	240
a₄(240)	→	241
a₄(267)	→	268
a₄(268)	→	269
a₄(237)	→	238
a₄(261)	→	262
a₄(265)	→	266
a₄(263)	→	264
a₄(242)	→	243
a₄(266)	→	267
a₄(241)	→	242
a₄(235)	→	236
b₄(234)	→	235
b₄(260)	→	261
b₄(238)	→	239
b₄(236)	→	237
b₄(262)	→	263
b₄(264)	→	265
b₃(226)	→	227
b₃(106)	→	107
b₃(280)	→	281
b₃(170)	→	171
b₃(200)	→	201
b₃(144)	→	145
b₃(108)	→	109
b₃(166)	→	167
b₃(142)	→	143
b₃(210)	→	211
b₃(168)	→	169
b₃(258)	→	259
b₃(202)	→	203
b₃(228)	→	229
b₃(274)	→	275
b₃(276)	→	277
b₃(104)	→	105
b₃(146)	→	147
b₃(224)	→	225
b₃(198)	→	199
b₁(64)	→	65
b₁(58)	→	59
b₁(8)	→	9
b₁(6)	→	7
b₁(4)	→	5
b₁(62)	→	63
b₁(34)	→	35
a₁(11)	→	12
a₁(12)	→	13
a₁(9)	→	10
a₁(7)	→	8
a₁(5)	→	6
a₁(10)	→	11
a₀(1)	→	2
a₀(2)	→	2
b₂(164)	→	165
b₂(130)	→	131
b₂(128)	→	129
b₂(132)	→	133
b₂(152)	→	153
b₂(78)	→	79
b₂(70)	→	71
b₂(40)	→	41
b₂(118)	→	119
b₂(38)	→	39
b₂(116)	→	117
b₂(196)	→	197
b₂(36)	→	37
b₂(66)	→	67
b₂(72)	→	73
b₂(68)	→	69
b₂(114)	→	115
a₃(167)	→	168
a₃(149)	→	150
a₃(227)	→	228
a₃(204)	→	205
a₃(230)	→	231
a₃(105)	→	106
a₃(110)	→	111
a₃(232)	→	233
a₃(225)	→	226
a₃(107)	→	108
a₃(150)	→	151
a₃(206)	→	207
a₃(147)	→	148
a₃(203)	→	204
a₃(111)	→	112
a₃(173)	→	174
a₃(112)	→	113
a₃(205)	→	206
a₃(172)	→	173
a₃(201)	→	202
a₃(174)	→	175
a₃(143)	→	144
a₃(229)	→	230
a₃(109)	→	110
a₃(145)	→	146
a₃(231)	→	232
a₃(199)	→	200
a₃(148)	→	149
a₃(169)	→	170
a₃(171)	→	172
b₀(1)	→	1
b₀(2)	→	1
a₂(44)	→	45
a₂(75)	→	76
a₂(129)	→	130
a₂(71)	→	72
a₂(115)	→	116
a₂(41)	→	42
a₂(134)	→	135
a₂(76)	→	77
a₂(122)	→	123
a₂(131)	→	132
a₂(117)	→	118
a₂(73)	→	74
a₂(136)	→	137
a₂(74)	→	75
a₂(135)	→	136
a₂(120)	→	121
a₂(42)	→	43
a₂(37)	→	38
a₂(39)	→	40
a₂(43)	→	44
a₂(119)	→	120
a₂(69)	→	70
a₂(133)	→	134
a₂(121)	→	122

The automaton is closed under rewriting as it is compatible.