Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/40708)

The rewrite relation of the following TRS is considered.

0(1(2(3(4(5(1(x1)))))))	→	0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))	(1)
0(1(2(3(4(5(1(x1)))))))	→	1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))	(2)
0(1(2(3(4(5(1(x1)))))))	→	1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))))))))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{7}

transitions:

280	→	304
61	→	7
61	→	34
229	→	135
289	→	269
146	→	176
341	→	88
95	→	34
95	→	40
319	→	305
55	→	68
175	→	77
40	→	48
287	→	82
316	→	322
410	→	418
392	→	404
334	→	342
416	→	436
60	→	74
60	→	76
125	→	34
125	→	40
125	→	174
125	→	66
125	→	54
207	→	113
153	→	40
153	→	174
153	→	66
153	→	54
88	→	112
54	→	66
54	→	174
75	→	29
124	→	134
124	→	268
67	→	49
437	→	381
118	→	130
419	→	405
188	→	228
188	→	288
379	→	343
348	→	378
7	→	28
69	→	29
417	→	118
182	→	206
189	→	40
189	→	174
189	→	66
189	→	54
310	→	318
47	→	7
47	→	34
131	→	113
399	→	118
354	→	380
317	→	82
355	→	88
4₁(57)	→	58
4₁(49)	→	50
4₁(29)	→	30
4₁(35)	→	36
4₁(43)	→	44
5₂(130)	→	131
5₂(82)	→	83
5₂(120)	→	121
5₂(134)	→	135
5₂(148)	→	149
5₂(140)	→	141
5₂(174)	→	175
5₂(90)	→	91
5₂(228)	→	229
5₂(76)	→	77
5₂(184)	→	185
5₂(176)	→	177
5₂(112)	→	113
5₂(206)	→	207
2₂(143)	→	144
2₂(79)	→	80
2₂(85)	→	86
2₂(137)	→	138
2₂(93)	→	94
2₂(187)	→	188
2₂(123)	→	124
2₂(151)	→	152
2₂(179)	→	180
2₂(115)	→	116
1₂(119)	→	120
1₂(183)	→	184
1₂(188)	→	189
1₂(86)	→	87
1₂(138)	→	139
1₂(116)	→	117
1₂(144)	→	145
1₂(182)	→	183
1₂(80)	→	81
1₂(180)	→	181
1₂(124)	→	125
1₂(88)	→	89
1₂(118)	→	119
1₂(146)	→	147
1₂(89)	→	90
1₂(147)	→	148
4₃(337)	→	338
4₃(395)	→	396
4₃(313)	→	314
4₃(323)	→	324
4₃(305)	→	306
4₃(413)	→	414
4₃(269)	→	270
4₃(283)	→	284
4₃(329)	→	330
4₃(405)	→	406
4₃(387)	→	388
4₃(343)	→	344
4₃(275)	→	276
4₃(381)	→	382
4₃(351)	→	352
0₁(46)	→	47
0₁(39)	→	40
0₁(33)	→	34
0₁(53)	→	54
4₀(7)	→	7
5₃(436)	→	437
5₃(386)	→	387
5₃(336)	→	337
5₃(318)	→	319
5₃(394)	→	395
5₃(312)	→	313
5₃(412)	→	413
5₃(322)	→	323
5₃(268)	→	269
5₃(304)	→	305
5₃(288)	→	289
5₃(350)	→	351
5₃(274)	→	275
5₃(328)	→	329
5₃(404)	→	405
5₃(342)	→	343
5₃(378)	→	379
5₃(418)	→	419
5₃(380)	→	381
5₃(282)	→	283
3₃(396)	→	397
3₃(276)	→	277
3₃(314)	→	315
3₃(284)	→	285
3₃(414)	→	415
3₃(330)	→	331
3₃(352)	→	353
3₃(388)	→	389
3₃(344)	→	345
3₃(406)	→	407
3₃(382)	→	383
3₃(324)	→	325
3₃(338)	→	339
3₃(306)	→	307
3₃(270)	→	271
5₀(7)	→	7
0₂(139)	→	140
0₂(181)	→	182
0₂(87)	→	88
0₂(117)	→	118
0₂(81)	→	82
0₂(145)	→	146
0₂(94)	→	95
0₂(152)	→	153
2₃(277)	→	278
2₃(331)	→	332
2₃(285)	→	286
2₃(407)	→	408
2₃(307)	→	308
2₃(383)	→	384
2₃(345)	→	346
2₃(325)	→	326
2₃(315)	→	316
2₃(339)	→	340
2₃(353)	→	354
2₃(397)	→	398
2₃(271)	→	272
2₃(415)	→	416
2₃(389)	→	390
3₀(7)	→	7
1₁(60)	→	61
1₁(54)	→	55
1₁(41)	→	42
1₁(52)	→	53
1₁(40)	→	41
1₁(32)	→	33
1₁(38)	→	39
1₁(55)	→	56
2₁(31)	→	32
2₁(59)	→	60
2₁(45)	→	46
2₁(37)	→	38
2₁(51)	→	52
1₀(7)	→	7
2₀(7)	→	7
5₁(34)	→	35
5₁(48)	→	49
5₁(68)	→	69
5₁(66)	→	67
5₁(56)	→	57
5₁(74)	→	75
5₁(28)	→	29
5₁(42)	→	43
1₃(411)	→	412
1₃(334)	→	335
1₃(410)	→	411
1₃(311)	→	312
1₃(354)	→	355
1₃(308)	→	309
1₃(384)	→	385
1₃(393)	→	394
1₃(392)	→	393
1₃(332)	→	333
1₃(416)	→	417
1₃(326)	→	327
1₃(310)	→	311
1₃(348)	→	349
1₃(278)	→	279
1₃(281)	→	282
1₃(335)	→	336
1₃(280)	→	281
1₃(390)	→	391
1₃(316)	→	317
1₃(346)	→	347
1₃(349)	→	350
1₃(408)	→	409
1₃(272)	→	273
3₁(36)	→	37
3₁(44)	→	45
3₁(50)	→	51
3₁(30)	→	31
3₁(58)	→	59
4₂(113)	→	114
4₂(83)	→	84
4₂(121)	→	122
4₂(77)	→	78
4₂(141)	→	142
4₂(149)	→	150
4₂(135)	→	136
4₂(91)	→	92
4₂(185)	→	186
4₂(177)	→	178
0₃(340)	→	341
0₃(327)	→	328
0₃(409)	→	410
0₃(333)	→	334
0₃(279)	→	280
0₃(273)	→	274
0₃(385)	→	386
0₃(398)	→	399
0₃(347)	→	348
0₃(286)	→	287
0₃(391)	→	392
0₃(309)	→	310
0₀(7)	→	7
3₂(92)	→	93
3₂(178)	→	179
3₂(78)	→	79
3₂(186)	→	187
3₂(122)	→	123
3₂(136)	→	137
3₂(114)	→	115
3₂(150)	→	151
3₂(84)	→	85
3₂(142)	→	143

The automaton is closed under rewriting as it is compatible.