Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z095)

The rewrite relation of the following TRS is considered.

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

→

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 String Reversal

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

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

→

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

{3}

transitions:

25	→	240
29	→	98
89	→	44
263	→	448
87	→	195
80	→	23
286	→	197
136	→	24
149	→	23
391	→	354
18	→	81
3	→	13
50	→	15
50	→	13
50	→	3
50	→	14
382	→	289
134	→	287
411	→	384
331	→	179
95	→	23
65	→	14
199	→	305
456	→	414
483	→	449
185	→	121
185	→	152
20	→	42
99	→	23
293	→	361
49	→	66
123	→	383
127	→	108
127	→	109
127	→	241
101	→	23
26	→	177
125	→	352
309	→	484
512	→	451
201	→	260
268	→	240
268	→	25
248	→	130
21	→	3
21	→	15
21	→	14
257	→	206
311	→	475
54	→	14
105	→	23
67	→	14
264	→	439
313	→	262
265	→	412
28	→	119
28	→	150
212	→	109
479	→	513
45	→	148
16	→	106
114	→	83
481	→	504
85	→	278
295	→	241
30	→	15
30	→	16
30	→	24
30	→	107
46	→	100
362	→	353
158	→	107
48	→	64
48	→	79
17	→	94
47	→	104
360	→	243
154	→	249
267	→	323
492	→	477
203	→	149
521	→	506
340	→	242
132	→	374
19	→	22
19	→	53
266	→	332
27	→	128
447	→	334
156	→	204
291	→	410
420	→	325
a₄(451)	→	452
a₄(355)	→	356
a₄(387)	→	388
a₄(489)	→	490
a₄(380)	→	381
a₄(378)	→	379
a₄(415)	→	416
a₄(480)	→	481
a₄(359)	→	360
a₄(478)	→	479
a₄(454)	→	455
a₄(487)	→	488
a₄(335)	→	336
a₄(445)	→	446
a₄(482)	→	483
a₄(337)	→	338
a₄(481)	→	482
a₄(443)	→	444
a₄(377)	→	378
a₄(491)	→	492
a₄(419)	→	420
a₄(388)	→	389
a₄(356)	→	357
a₄(339)	→	340
a₄(381)	→	382
a₄(452)	→	453
a₄(416)	→	417
a₄(442)	→	443
a₄(453)	→	454
a₄(336)	→	337
a₄(379)	→	380
a₄(390)	→	391
a₄(418)	→	419
a₄(444)	→	445
a₄(386)	→	387
a₄(488)	→	489
a₄(338)	→	339
a₄(455)	→	456
a₄(417)	→	418
a₄(357)	→	358
a₄(358)	→	359
a₄(446)	→	447
a₄(490)	→	491
a₄(479)	→	480
a₄(389)	→	390
b₄(410)	→	411
b₄(440)	→	441
b₄(486)	→	487
b₄(475)	→	476
b₄(354)	→	355
b₄(375)	→	376
b₄(361)	→	362
b₄(441)	→	442
b₄(477)	→	478
b₄(353)	→	354
b₄(383)	→	384
b₄(376)	→	377
b₄(332)	→	333
b₄(374)	→	375
b₄(333)	→	334
b₄(334)	→	335
b₄(412)	→	413
b₄(485)	→	486
b₄(439)	→	440
b₄(450)	→	451
b₄(448)	→	449
b₄(384)	→	385
b₄(476)	→	477
b₄(385)	→	386
b₄(449)	→	450
b₄(413)	→	414
b₄(352)	→	353
b₄(414)	→	415
b₄(484)	→	485
b₃(280)	→	281
b₃(241)	→	242
b₃(177)	→	178
b₃(206)	→	207
b₃(260)	→	261
b₃(306)	→	307
b₃(279)	→	280
b₃(250)	→	251
b₃(251)	→	252
b₃(289)	→	290
b₃(278)	→	279
b₃(178)	→	179
b₃(130)	→	131
b₃(205)	→	206
b₃(179)	→	180
b₃(262)	→	263
b₃(307)	→	308
b₃(120)	→	121
b₃(242)	→	243
b₃(323)	→	324
b₃(129)	→	130
b₃(249)	→	250
b₃(121)	→	122
b₃(324)	→	325
b₃(288)	→	289
b₃(204)	→	205
b₃(128)	→	129
b₃(261)	→	262
b₃(305)	→	306
b₃(287)	→	288
b₃(325)	→	326
b₃(119)	→	120
b₃(240)	→	241
b₁(64)	→	65
b₁(43)	→	44
b₁(15)	→	16
b₁(14)	→	15
b₁(66)	→	67
b₁(42)	→	43
b₁(44)	→	45
b₁(13)	→	14
b₁(53)	→	54
a₁(17)	→	18
a₁(16)	→	17
a₁(49)	→	50
a₁(20)	→	21
a₁(45)	→	46
a₁(46)	→	47
a₁(19)	→	20
a₁(48)	→	49
a₁(18)	→	19
a₁(47)	→	48
a₅(507)	→	508
a₅(510)	→	511
a₅(511)	→	512
a₅(509)	→	510
a₅(516)	→	517
a₅(518)	→	519
a₅(517)	→	518
a₅(519)	→	520
a₅(520)	→	521
a₅(508)	→	509
b₅(506)	→	507
b₅(513)	→	514
b₅(504)	→	505
b₅(514)	→	515
b₅(505)	→	506
b₅(515)	→	516
a₀(3)	→	3
b₂(104)	→	105
b₂(152)	→	153
b₂(22)	→	23
b₂(79)	→	80
b₂(23)	→	24
b₂(24)	→	25
b₂(100)	→	101
b₂(148)	→	149
b₂(94)	→	95
b₂(82)	→	83
b₂(81)	→	82
b₂(107)	→	108
b₂(83)	→	84
b₂(108)	→	109
b₂(106)	→	107
b₂(151)	→	152
b₂(197)	→	198
b₂(150)	→	151
b₂(196)	→	197
b₂(98)	→	99
b₂(195)	→	196
a₃(330)	→	331
a₃(329)	→	330
a₃(123)	→	124
a₃(263)	→	264
a₃(133)	→	134
a₃(134)	→	135
a₃(184)	→	185
a₃(246)	→	247
a₃(309)	→	310
a₃(310)	→	311
a₃(252)	→	253
a₃(255)	→	256
a₃(308)	→	309
a₃(294)	→	295
a₃(247)	→	248
a₃(291)	→	292
a₃(131)	→	132
a₃(124)	→	125
a₃(292)	→	293
a₃(244)	→	245
a₃(254)	→	255
a₃(181)	→	182
a₃(281)	→	282
a₃(264)	→	265
a₃(282)	→	283
a₃(284)	→	285
a₃(135)	→	136
a₃(211)	→	212
a₃(245)	→	246
a₃(311)	→	312
a₃(256)	→	257
a₃(132)	→	133
a₃(125)	→	126
a₃(208)	→	209
a₃(312)	→	313
a₃(290)	→	291
a₃(180)	→	181
a₃(267)	→	268
a₃(293)	→	294
a₃(183)	→	184
a₃(126)	→	127
a₃(243)	→	244
a₃(209)	→	210
a₃(266)	→	267
a₃(253)	→	254
a₃(285)	→	286
a₃(210)	→	211
a₃(328)	→	329
a₃(327)	→	328
a₃(283)	→	284
a₃(207)	→	208
a₃(122)	→	123
a₃(265)	→	266
a₃(326)	→	327
a₃(182)	→	183
b₀(3)	→	3
a₂(109)	→	110
a₂(26)	→	27
a₂(110)	→	111
a₂(85)	→	86
a₂(29)	→	30
a₂(112)	→	113
a₂(88)	→	89
a₂(202)	→	203
a₂(198)	→	199
a₂(154)	→	155
a₂(201)	→	202
a₂(113)	→	114
a₂(153)	→	154
a₂(199)	→	200
a₂(86)	→	87
a₂(87)	→	88
a₂(28)	→	29
a₂(84)	→	85
a₂(157)	→	158
a₂(111)	→	112
a₂(200)	→	201
a₂(27)	→	28
a₂(156)	→	157
a₂(25)	→	26
a₂(155)	→	156

The automaton is closed under rewriting as it is compatible.