Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z031)

The rewrite relation of the following TRS is considered.

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

→

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

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

→

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

(2)

1.1 Bounds

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

final states:

{3, 2, 1}

transitions:

102	→	6
356	→	371
338	→	209
98	→	42
10	→	41
10	→	71
96	→	53
120	→	205
120	→	259
3	→	35
184	→	142
50	→	7
50	→	8
50	→	88
298	→	249
130	→	42
304	→	351
246	→	44
380	→	292
1	→	5
8	→	87
60	→	7
60	→	5
60	→	1
60	→	6
44	→	207
38	→	6
58	→	101
36	→	6
268	→	208
72	→	6
150	→	89
150	→	90
54	→	129
308	→	153
308	→	143
124	→	43
124	→	7
264	→	269
350	→	301
2	→	37
244	→	299
14	→	1
14	→	7
14	→	6
12	→	51
104	→	6
216	→	117
46	→	141
46	→	151
278	→	210
240	→	341
256	→	187
48	→	115
160	→	88
190	→	237
360	→	290
242	→	329
206	→	42
148	→	247
92	→	185
144	→	289
194	→	130
56	→	97
56	→	103
156	→	183
c₄(293)	→	294
c₄(355)	→	356
c₄(277)	→	278
c₄(335)	→	336
c₄(275)	→	276
c₄(357)	→	358
c₄(349)	→	350
c₄(295)	→	296
c₄(297)	→	298
c₄(347)	→	348
c₄(273)	→	274
c₄(337)	→	338
c₄(359)	→	360
c₄(333)	→	334
c₄(345)	→	346
b₅(374)	→	375
b₅(376)	→	377
b₅(378)	→	379
c₅(379)	→	380
c₅(375)	→	376
c₅(377)	→	378
a₄(269)	→	270
a₄(331)	→	332
a₄(330)	→	331
a₄(290)	→	291
a₄(289)	→	290
a₄(271)	→	272
a₄(353)	→	354
a₄(291)	→	292
a₄(352)	→	353
a₄(270)	→	271
a₄(341)	→	342
a₄(342)	→	343
a₄(343)	→	344
a₄(329)	→	330
a₄(351)	→	352
b₂(190)	→	191
b₂(46)	→	47
b₂(92)	→	93
b₂(120)	→	121
b₂(158)	→	159
b₂(44)	→	45
b₂(48)	→	49
b₂(118)	→	119
b₂(94)	→	95
b₂(90)	→	91
b₂(122)	→	123
b₂(154)	→	155
b₂(192)	→	193
b₂(156)	→	157
b₂(188)	→	189
a₂(41)	→	42
a₂(117)	→	118
a₂(152)	→	153
a₂(205)	→	206
a₂(186)	→	187
a₂(129)	→	130
a₂(88)	→	89
a₂(42)	→	43
a₂(87)	→	88
a₂(115)	→	116
a₂(185)	→	186
a₂(89)	→	90
a₂(187)	→	188
a₂(97)	→	98
a₂(116)	→	117
a₂(43)	→	44
a₂(153)	→	154
a₂(151)	→	152
c₂(123)	→	124
c₂(91)	→	92
c₂(159)	→	160
c₂(45)	→	46
c₂(95)	→	96
c₂(155)	→	156
c₂(47)	→	48
c₂(121)	→	122
c₂(191)	→	192
c₂(189)	→	190
c₂(193)	→	194
c₂(49)	→	50
c₂(119)	→	120
c₂(93)	→	94
c₂(157)	→	158
c₀(3)	→	2
c₀(1)	→	2
c₀(2)	→	2
b₀(2)	→	3
b₀(3)	→	3
b₀(1)	→	3
c₃(255)	→	256
c₃(263)	→	264
c₃(211)	→	212
c₃(241)	→	242
c₃(305)	→	306
c₃(147)	→	148
c₃(149)	→	150
c₃(251)	→	252
c₃(307)	→	308
c₃(267)	→	268
c₃(145)	→	146
c₃(303)	→	304
c₃(265)	→	266
c₃(253)	→	254
c₃(245)	→	246
c₃(215)	→	216
c₃(243)	→	244
c₃(213)	→	214
b₃(146)	→	147
b₃(262)	→	263
b₃(302)	→	303
b₃(266)	→	267
b₃(250)	→	251
b₃(242)	→	243
b₃(214)	→	215
b₃(252)	→	253
b₃(212)	→	213
b₃(306)	→	307
b₃(144)	→	145
b₃(148)	→	149
b₃(240)	→	241
b₃(304)	→	305
b₃(264)	→	265
b₃(210)	→	211
b₃(244)	→	245
b₃(254)	→	255
a₀(1)	→	1
a₀(2)	→	1
a₀(3)	→	1
b₁(8)	→	9
b₁(54)	→	55
b₁(58)	→	59
b₁(10)	→	11
b₁(56)	→	57
b₁(12)	→	13
a₁(51)	→	52
a₁(71)	→	72
a₁(37)	→	38
a₁(6)	→	7
a₁(53)	→	54
a₁(7)	→	8
a₁(52)	→	53
a₁(35)	→	36
a₁(101)	→	102
a₁(103)	→	104
a₁(5)	→	6
b₄(346)	→	347
b₄(332)	→	333
b₄(348)	→	349
b₄(272)	→	273
b₄(292)	→	293
b₄(276)	→	277
b₄(344)	→	345
b₄(336)	→	337
b₄(356)	→	357
b₄(354)	→	355
b₄(294)	→	295
b₄(358)	→	359
b₄(274)	→	275
b₄(296)	→	297
b₄(334)	→	335
a₃(207)	→	208
a₃(261)	→	262
a₃(299)	→	300
a₃(249)	→	250
a₃(183)	→	184
a₃(237)	→	238
a₃(248)	→	249
a₃(247)	→	248
a₃(300)	→	301
a₃(208)	→	209
a₃(141)	→	142
a₃(209)	→	210
a₃(142)	→	143
a₃(143)	→	144
a₃(301)	→	302
a₃(238)	→	239
a₃(259)	→	260
a₃(260)	→	261
a₃(239)	→	240
c₁(13)	→	14
c₁(55)	→	56
c₁(59)	→	60
c₁(57)	→	58
c₁(9)	→	10
c₁(11)	→	12
a₅(371)	→	372
a₅(372)	→	373
a₅(373)	→	374

The automaton is closed under rewriting as it is compatible.