Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3268)

The rewrite relation of the following TRS is considered.

1(4(x1))	→	3(1(1(2(2(4(x1))))))	(1)
5(4(x1))	→	4(2(3(1(1(1(x1))))))	(2)
0(3(0(x1)))	→	2(1(1(0(2(0(x1))))))	(3)
0(5(5(x1)))	→	1(0(1(3(4(2(x1))))))	(4)
1(5(4(x1)))	→	0(2(5(2(0(4(x1))))))	(5)
3(5(4(x1)))	→	4(1(3(4(2(3(x1))))))	(6)
4(1(4(x1)))	→	3(3(2(2(3(1(x1))))))	(7)
5(4(0(x1)))	→	2(4(0(4(4(0(x1))))))	(8)
5(4(0(x1)))	→	5(1(5(2(1(0(x1))))))	(9)
5(4(4(x1)))	→	4(1(1(3(2(4(x1))))))	(10)
5(5(4(x1)))	→	3(4(4(1(2(2(x1))))))	(11)
0(5(5(0(x1))))	→	0(2(0(0(3(0(x1))))))	(12)
0(5(5(4(x1))))	→	0(1(3(4(3(4(x1))))))	(13)
1(4(5(4(x1))))	→	0(4(5(0(2(1(x1))))))	(14)
1(4(5(5(x1))))	→	0(0(1(3(4(1(x1))))))	(15)
2(5(4(0(x1))))	→	0(4(1(2(4(0(x1))))))	(16)
4(3(0(5(x1))))	→	3(3(2(3(5(5(x1))))))	(17)
5(4(0(0(x1))))	→	1(0(4(0(2(2(x1))))))	(18)
5(4(0(2(x1))))	→	3(0(4(5(0(2(x1))))))	(19)

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

4(1(x1))	→	4(2(2(1(1(3(x1))))))	(20)
4(5(x1))	→	1(1(1(3(2(4(x1))))))	(21)
0(3(0(x1)))	→	0(2(0(1(1(2(x1))))))	(22)
5(5(0(x1)))	→	2(4(3(1(0(1(x1))))))	(23)
4(5(1(x1)))	→	4(0(2(5(2(0(x1))))))	(24)
4(5(3(x1)))	→	3(2(4(3(1(4(x1))))))	(25)
4(1(4(x1)))	→	1(3(2(2(3(3(x1))))))	(26)
0(4(5(x1)))	→	0(4(4(0(4(2(x1))))))	(27)
0(4(5(x1)))	→	0(1(2(5(1(5(x1))))))	(28)
4(4(5(x1)))	→	4(2(3(1(1(4(x1))))))	(29)
4(5(5(x1)))	→	2(2(1(4(4(3(x1))))))	(30)
0(5(5(0(x1))))	→	0(3(0(0(2(0(x1))))))	(31)
4(5(5(0(x1))))	→	4(3(4(3(1(0(x1))))))	(32)
4(5(4(1(x1))))	→	1(2(0(5(4(0(x1))))))	(33)
5(5(4(1(x1))))	→	1(4(3(1(0(0(x1))))))	(34)
0(4(5(2(x1))))	→	0(4(2(1(4(0(x1))))))	(35)
5(0(3(4(x1))))	→	5(5(3(2(3(3(x1))))))	(36)
0(0(4(5(x1))))	→	2(2(0(4(0(1(x1))))))	(37)
2(0(4(5(x1))))	→	2(0(5(4(0(3(x1))))))	(38)

1.1 Bounds

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

final states:

{7}

transitions:

33	→	497
23	→	57
239	→	160
176	→	16
494	→	45
494	→	495
61	→	259
81	→	38
103	→	45
51	→	457
51	→	463
51	→	471
496	→	118
401	→	499
149	→	102
472	→	41
391	→	122
211	→	459
211	→	465
211	→	467
211	→	493
502	→	122
145	→	181
145	→	196
145	→	316
145	→	331
145	→	396
466	→	207
41	→	318
39	→	7
39	→	52
39	→	160
39	→	498
500	→	122
460	→	25
146	→	7
146	→	87
187	→	23
187	→	197
187	→	182
298	→	186
134	→	293
134	→	310
34	→	77
34	→	86
34	→	40
34	→	22
34	→	15
34	→	33
34	→	51
34	→	7
34	→	207
34	→	464
456	→	25
319	→	89
483	→	197
483	→	182
20	→	308
107	→	38
62	→	7
62	→	57
62	→	23
123	→	136
332	→	429
197	→	23
135	→	27
402	→	131
402	→	117
402	→	7
402	→	132
402	→	122
402	→	52
402	→	498
330	→	57
330	→	23
76	→	27
38	→	198
38	→	233
38	→	247
253	→	455
253	→	461
253	→	473
309	→	72
91	→	38
58	→	92
170	→	23
201	→	162
248	→	41
21	→	7
21	→	23
138	→	80
311	→	72
121	→	20
337	→	57
337	→	86
337	→	40
337	→	22
337	→	15
337	→	33
337	→	51
337	→	7
337	→	23
468	→	41
52	→	117
52	→	122
52	→	131
52	→	86
52	→	40
52	→	22
52	→	15
52	→	33
52	→	51
52	→	7
431	→	145
105	→	206
498	→	122
336	→	501
264	→	484
485	→	57
143	→	477
53	→	104
265	→	57
265	→	86
265	→	40
265	→	22
265	→	15
265	→	33
265	→	51
265	→	7
265	→	23
28	→	7
28	→	23
28	→	87
212	→	39
45	→	390
16	→	72
16	→	99
16	→	159
348	→	99
7	→	15
7	→	22
7	→	33
7	→	40
7	→	51
7	→	86
126	→	27
42	→	147
46	→	7
46	→	87
46	→	57
46	→	23
46	→	131
46	→	117
46	→	132
46	→	122
46	→	52
46	→	77
46	→	104
46	→	53
46	→	34
46	→	498
46	→	25
46	→	458
458	→	25
462	→	207
254	→	52
464	→	207
74	→	143
474	→	41
144	→	324
144	→	347
144	→	446
317	→	77
27	→	164
27	→	175
27	→	253
447	→	182
163	→	45
56	→	20
94	→	19
4₁(99)	→	100
4₁(259)	→	260
4₁(196)	→	197
4₁(119)	→	120
4₁(160)	→	161
4₁(22)	→	23
4₁(398)	→	399
4₁(79)	→	80
4₁(332)	→	333
4₁(59)	→	60
4₁(134)	→	135
4₁(80)	→	81
4₁(262)	→	263
4₁(122)	→	123
4₁(430)	→	431
4₁(484)	→	485
4₁(100)	→	101
4₁(20)	→	21
4₁(147)	→	148
4₁(333)	→	334
4₁(77)	→	78
4₁(44)	→	45
0₂(236)	→	237
0₂(211)	→	212
0₂(209)	→	210
0₂(238)	→	239
1₂(234)	→	235
1₂(165)	→	166
1₂(184)	→	185
1₂(478)	→	479
1₂(207)	→	208
1₂(235)	→	236
1₂(327)	→	328
1₂(166)	→	167
1₂(186)	→	187
1₂(185)	→	186
1₂(208)	→	209
2₂(465)	→	466
2₂(233)	→	234
2₂(206)	→	207
2₂(210)	→	211
2₂(328)	→	329
2₂(481)	→	482
2₂(295)	→	296
2₂(463)	→	464
2₂(182)	→	183
2₂(329)	→	330
2₂(168)	→	169
2₂(461)	→	462
2₂(296)	→	297
2₂(167)	→	168
2₂(237)	→	238
1₁(247)	→	248
1₁(40)	→	41
1₁(87)	→	88
1₁(467)	→	468
1₁(101)	→	102
1₁(334)	→	335
1₁(396)	→	397
1₁(495)	→	496
1₁(90)	→	91
1₁(35)	→	36
1₁(132)	→	133
1₁(92)	→	93
1₁(473)	→	474
1₁(260)	→	261
1₁(25)	→	26
1₁(57)	→	58
1₁(26)	→	27
1₁(471)	→	472
1₁(136)	→	137
1₁(199)	→	200
1₁(117)	→	118
1₁(200)	→	201
1₁(27)	→	28
1₁(34)	→	35
1₁(42)	→	43
1₁(17)	→	18
1₁(16)	→	17
5₀(7)	→	7
0₀(7)	→	7
3₀(7)	→	7
2₁(19)	→	20
2₁(125)	→	126
2₁(336)	→	337
2₁(335)	→	336
2₁(263)	→	264
2₁(400)	→	401
2₁(60)	→	61
2₁(198)	→	199
2₁(54)	→	55
2₁(316)	→	317
2₁(401)	→	402
2₁(89)	→	90
2₁(52)	→	53
2₁(74)	→	75
2₁(102)	→	103
2₁(137)	→	138
2₁(18)	→	19
2₁(45)	→	46
2₁(455)	→	456
2₁(33)	→	34
2₁(37)	→	38
2₁(23)	→	24
2₁(457)	→	458
2₁(73)	→	74
2₁(459)	→	460
0₁(131)	→	132
0₁(105)	→	106
0₁(55)	→	56
0₁(493)	→	494
0₁(253)	→	254
0₁(429)	→	430
0₁(497)	→	498
0₁(499)	→	500
0₁(38)	→	39
0₁(390)	→	391
0₁(148)	→	149
0₁(162)	→	163
0₁(36)	→	37
0₁(41)	→	42
0₁(399)	→	400
0₁(124)	→	125
0₁(78)	→	79
0₁(501)	→	502
0₁(51)	→	52
0₁(104)	→	105
0₁(159)	→	160
0₁(397)	→	398
1₀(7)	→	7
2₀(7)	→	7
3₁(72)	→	73
3₁(58)	→	59
3₁(331)	→	332
3₁(308)	→	309
3₁(15)	→	16
3₁(24)	→	25
3₁(133)	→	134
3₁(75)	→	76
3₁(261)	→	262
3₁(310)	→	311
3₁(43)	→	44
3₁(93)	→	94
3₁(347)	→	348
3₁(143)	→	144
3₁(61)	→	62
3₁(106)	→	107
3₁(264)	→	265
3₁(120)	→	121
3₁(175)	→	176
3₁(118)	→	119
5₁(53)	→	54
5₁(318)	→	319
5₁(123)	→	124
5₁(88)	→	89
5₁(144)	→	145
5₁(145)	→	146
5₁(161)	→	162
5₁(86)	→	87
3₂(479)	→	480
3₂(294)	→	295
3₂(297)	→	298
3₂(183)	→	184
3₂(164)	→	165
3₂(482)	→	483
3₂(293)	→	294
3₂(324)	→	325
4₀(7)	→	7
4₂(477)	→	478
4₂(480)	→	481
4₂(326)	→	327
4₂(169)	→	170
4₂(181)	→	182
4₂(446)	→	447
4₂(325)	→	326

The automaton is closed under rewriting as it is compatible.