Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z097)

The rewrite relation of the following TRS is considered.

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

→

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

272	→	149
239	→	138
364	→	307
111	→	273
61	→	168
102	→	87
102	→	58
87	→	57
98	→	229
10	→	69
145	→	61
145	→	60
213	→	387
9	→	86
443	→	479
65	→	90
130	→	106
193	→	169
193	→	148
397	→	309
445	→	425
62	→	146
1	→	37
305	→	243
316	→	151
316	→	150
13	→	41
44	→	5
38	→	5
235	→	468
91	→	57
141	→	365
441	→	503
237	→	435
283	→	186
283	→	309
143	→	207
143	→	262
2	→	4
11	→	67
478	→	438
66	→	7
66	→	8
66	→	9
66	→	59
66	→	87
14	→	1
14	→	6
14	→	5
14	→	38
14	→	7
421	→	274
63	→	105
12	→	43
12	→	56
169	→	147
140	→	424
100	→	135
217	→	148
113	→	183
113	→	363
42	→	5
64	→	92
64	→	129
189	→	420
434	→	298
115	→	59
115	→	60
115	→	169
250	→	149
68	→	57
215	→	306
340	→	307
142	→	295
489	→	428
375	→	210
375	→	265
144	→	240
70	→	57
191	→	339
156	→	95
156	→	108
513	→	482
b₄(279)	→	280
b₄(394)	→	395
b₄(440)	→	441
b₄(371)	→	372
b₄(429)	→	430
b₄(392)	→	393
b₄(372)	→	373
b₄(278)	→	279
b₄(301)	→	302
b₄(300)	→	301
b₄(270)	→	271
b₄(374)	→	375
b₄(430)	→	431
b₄(271)	→	272
b₄(303)	→	304
b₄(280)	→	281
b₄(477)	→	478
b₄(373)	→	374
b₄(267)	→	268
b₄(312)	→	313
b₄(313)	→	314
b₄(268)	→	269
b₄(443)	→	444
b₄(433)	→	434
b₄(315)	→	316
b₄(304)	→	305
b₄(311)	→	312
b₄(432)	→	433
b₄(442)	→	443
b₄(314)	→	315
b₄(302)	→	303
b₄(396)	→	397
b₄(474)	→	475
b₄(431)	→	432
b₄(444)	→	445
b₄(269)	→	270
b₄(281)	→	282
b₄(441)	→	442
b₄(473)	→	474
b₄(395)	→	396
b₄(282)	→	283
b₄(476)	→	477
b₄(475)	→	476
b₄(393)	→	394
b₄(370)	→	371
a₄(366)	→	367
a₄(339)	→	340
a₄(388)	→	389
a₄(295)	→	296
a₄(275)	→	276
a₄(469)	→	470
a₄(435)	→	436
a₄(297)	→	298
a₄(310)	→	311
a₄(389)	→	390
a₄(420)	→	421
a₄(266)	→	267
a₄(436)	→	437
a₄(309)	→	310
a₄(263)	→	264
a₄(369)	→	370
a₄(427)	→	428
a₄(426)	→	427
a₄(468)	→	469
a₄(471)	→	472
a₄(308)	→	309
a₄(387)	→	388
a₄(472)	→	473
a₄(390)	→	391
a₄(296)	→	297
a₄(470)	→	471
a₄(298)	→	299
a₄(277)	→	278
a₄(265)	→	266
a₄(273)	→	274
a₄(438)	→	439
a₄(439)	→	440
a₄(276)	→	277
a₄(367)	→	368
a₄(428)	→	429
a₄(262)	→	263
a₄(299)	→	300
a₄(363)	→	364
a₄(424)	→	425
a₄(365)	→	366
a₄(306)	→	307
a₄(274)	→	275
a₄(437)	→	438
a₄(307)	→	308
a₄(264)	→	265
a₄(368)	→	369
a₄(391)	→	392
a₄(425)	→	426
a₃(244)	→	245
a₃(106)	→	107
a₃(137)	→	138
a₃(241)	→	242
a₃(148)	→	149
a₃(150)	→	151
a₃(183)	→	184
a₃(147)	→	148
a₃(230)	→	231
a₃(108)	→	109
a₃(207)	→	208
a₃(136)	→	137
a₃(210)	→	211
a₃(105)	→	106
a₃(168)	→	169
a₃(231)	→	232
a₃(107)	→	108
a₃(187)	→	188
a₃(149)	→	150
a₃(242)	→	243
a₃(209)	→	210
a₃(129)	→	130
a₃(109)	→	110
a₃(185)	→	186
a₃(243)	→	244
a₃(139)	→	140
a₃(184)	→	185
a₃(232)	→	233
a₃(146)	→	147
a₃(208)	→	209
a₃(135)	→	136
a₃(233)	→	234
a₃(229)	→	230
a₃(138)	→	139
a₃(211)	→	212
a₃(186)	→	187
a₃(240)	→	241
a₁(37)	→	38
a₁(5)	→	6
a₁(7)	→	8
a₁(43)	→	44
a₁(8)	→	9
a₁(41)	→	42
a₁(6)	→	7
a₁(4)	→	5
b₁(11)	→	12
b₁(13)	→	14
b₁(12)	→	13
b₁(9)	→	10
b₁(10)	→	11
b₅(512)	→	513
b₅(488)	→	489
b₅(510)	→	511
b₅(511)	→	512
b₅(509)	→	510
b₅(487)	→	488
b₅(486)	→	487
b₅(484)	→	485
b₅(485)	→	486
b₅(508)	→	509
a₅(506)	→	507
a₅(483)	→	484
a₅(481)	→	482
a₅(503)	→	504
a₅(504)	→	505
a₅(479)	→	480
a₅(507)	→	508
a₅(505)	→	506
a₅(482)	→	483
a₅(480)	→	481
b₀(1)	→	2
b₀(2)	→	2
a₂(96)	→	97
a₂(93)	→	94
a₂(95)	→	96
a₂(58)	→	59
a₂(86)	→	87
a₂(57)	→	58
a₂(94)	→	95
a₂(59)	→	60
a₂(92)	→	93
a₂(90)	→	91
a₂(56)	→	57
a₂(60)	→	61
a₂(69)	→	70
a₂(67)	→	68
b₃(114)	→	115
b₃(237)	→	238
b₃(110)	→	111
b₃(213)	→	214
b₃(191)	→	192
b₃(246)	→	247
b₃(113)	→	114
b₃(215)	→	216
b₃(152)	→	153
b₃(235)	→	236
b₃(247)	→	248
b₃(189)	→	190
b₃(234)	→	235
b₃(236)	→	237
b₃(155)	→	156
b₃(151)	→	152
b₃(248)	→	249
b₃(214)	→	215
b₃(249)	→	250
b₃(192)	→	193
b₃(245)	→	246
b₃(141)	→	142
b₃(238)	→	239
b₃(140)	→	141
b₃(216)	→	217
b₃(111)	→	112
b₃(112)	→	113
b₃(143)	→	144
b₃(154)	→	155
b₃(142)	→	143
b₃(212)	→	213
b₃(188)	→	189
b₃(190)	→	191
b₃(144)	→	145
b₃(153)	→	154
a₀(1)	→	1
a₀(2)	→	1
b₂(64)	→	65
b₂(97)	→	98
b₂(101)	→	102
b₂(100)	→	101
b₂(99)	→	100
b₂(63)	→	64
b₂(98)	→	99
b₂(61)	→	62
b₂(65)	→	66
b₂(62)	→	63

The automaton is closed under rewriting as it is compatible.