Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3385)

The rewrite relation of the following TRS is considered.

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

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:

{6, 5, 4, 3, 2, 1}

transitions:

272	→	747
314	→	290
314	→	28
314	→	115
314	→	279
314	→	202
314	→	69
314	→	1
366	→	361
364	→	343
111	→	301
111	→	325
111	→	327
322	→	316
793	→	237
376	→	370
280	→	269
534	→	302
102	→	1
102	→	376
102	→	378
102	→	533
29	→	9
29	→	237
750	→	416
338	→	2
338	→	358
338	→	354
338	→	55
338	→	151
338	→	70
338	→	721
338	→	445
338	→	762
791	→	302
658	→	101
152	→	195
286	→	269
286	→	375
229	→	203
229	→	365
809	→	702
274	→	3
274	→	327
274	→	301
274	→	325
274	→	111
273	→	427
273	→	549
742	→	415
97	→	55
97	→	352
734	→	9
289	→	774
781	→	183
374	→	6
374	→	529
374	→	367
374	→	203
438	→	151
560	→	237
129	→	111
129	→	412
326	→	316
530	→	302
655	→	763
728	→	373
167	→	152
167	→	287
461	→	152
550	→	237
469	→	183
227	→	203
815	→	702
3	→	52
3	→	96
3	→	128
3	→	228
3	→	277
57	→	462
218	→	203
218	→	360
382	→	373
817	→	111
500	→	269
500	→	4
500	→	280
405	→	58
405	→	727
9	→	193
9	→	266
9	→	310
331	→	437
331	→	439
331	→	477
5	→	44
5	→	84
5	→	110
5	→	217
5	→	268
443	→	418
59	→	13
199	→	3
199	→	327
199	→	301
199	→	111
199	→	321
199	→	140
483	→	327
483	→	301
483	→	277
483	→	128
483	→	52
483	→	96
483	→	228
483	→	3
483	→	325
483	→	111
241	→	198
55	→	177
55	→	358
243	→	238
756	→	440
467	→	183
31	→	9
31	→	183
31	→	253
1	→	28
1	→	69
1	→	115
1	→	202
1	→	279
305	→	290
127	→	111
127	→	315
13	→	466
13	→	508
13	→	626
332	→	5
332	→	310
332	→	193
332	→	9
332	→	237
332	→	29
332	→	736
101	→	414
101	→	557
777	→	445
392	→	9
505	→	240
428	→	415
426	→	415
751	→	818
748	→	415
343	→	391
343	→	444
343	→	568
269	→	377
309	→	288
309	→	393
783	→	203
58	→	580
58	→	714
208	→	3
208	→	327
208	→	301
208	→	325
208	→	111
385	→	372
186	→	12
72	→	55
72	→	166
72	→	356
552	→	237
178	→	152
178	→	299
178	→	379
509	→	502
509	→	602
207	→	468
207	→	501
207	→	615
779	→	446
6	→	8
6	→	54
6	→	126
6	→	226
6	→	283
726	→	373
773	→	302
773	→	420
116	→	111
116	→	319
116	→	402
627	→	616
153	→	453
799	→	315
394	→	101
498	→	240
764	→	56
270	→	333
270	→	497
368	→	361
569	→	315
53	→	9
53	→	187
803	→	111
2	→	42
2	→	82
2	→	141
2	→	209
2	→	285
180	→	101
313	→	681
797	→	315
797	→	806
4	→	30
4	→	71
4	→	139
4	→	215
4	→	281
528	→	377
528	→	269
528	→	280
344	→	2
344	→	358
344	→	354
344	→	55
344	→	151
344	→	70
463	→	101
284	→	269
801	→	55
188	→	184
300	→	288
580	→	753
580	→	755
580	→	782
45	→	9
45	→	191
45	→	255
754	→	151
318	→	289
359	→	340
114	→	58
114	→	336
14	→	1
14	→	302
481	→	808
373	→	425
373	→	551
357	→	340
581	→	310
581	→	193
581	→	9
581	→	268
581	→	110
581	→	44
581	→	84
581	→	217
581	→	5
581	→	237
581	→	29
581	→	736
12	→	522
12	→	539
12	→	559
720	→	367
720	→	203
85	→	55
85	→	168
85	→	339
169	→	152
112	→	404
450	→	376
450	→	378
140	→	111
140	→	321
100	→	743
335	→	330
282	→	269
282	→	369
736	→	9
621	→	358
621	→	354
621	→	55
621	→	285
621	→	141
621	→	42
621	→	82
621	→	209
621	→	2
621	→	151
621	→	70
621	→	816
621	→	445
621	→	762
69	→	735
69	→	761
69	→	798
290	→	460
758	→	445
216	→	203
681	→	733
681	→	757
681	→	796
752	→	101
752	→	790
752	→	800
278	→	269
458	→	751
458	→	792
393	→	741
240	→	776
256	→	238
256	→	306
707	→	365
707	→	367
707	→	203
707	→	229
83	→	55
83	→	155
198	→	499
198	→	654
190	→	184
154	→	58
154	→	179
206	→	701
254	→	238
267	→	238
762	→	445
413	→	58
324	→	316
320	→	316
203	→	367
722	→	370
353	→	340
523	→	570
142	→	111
142	→	323
482	→	780
482	→	784
482	→	802
744	→	415
378	→	370
775	→	445
807	→	112
575	→	310
575	→	193
575	→	9
575	→	237
575	→	29
575	→	736
558	→	237
43	→	9
43	→	189
43	→	242
210	→	203
785	→	166
194	→	184
603	→	329
403	→	58
403	→	725
70	→	55
70	→	151
70	→	354
70	→	285
70	→	141
70	→	42
70	→	82
70	→	209
70	→	2
70	→	445
70	→	762
544	→	527
544	→	778
442	→	767
682	→	358
682	→	354
682	→	55
682	→	285
682	→	141
682	→	42
682	→	82
682	→	209
682	→	2
682	→	151
682	→	70
56	→	98
56	→	383
312	→	814
192	→	184
156	→	152
238	→	308
819	→	415
291	→	4
291	→	377
291	→	269
291	→	280
355	→	340
459	→	14
459	→	749
459	→	716
420	→	302
420	→	534
307	→	288
3₁(323)	→	324
3₁(328)	→	329
3₁(466)	→	467
3₁(602)	→	603
3₁(30)	→	31
3₁(468)	→	469
3₁(360)	→	361
3₁(9)	→	10
3₁(55)	→	56
3₁(559)	→	560
3₁(580)	→	581
3₁(238)	→	239
3₁(763)	→	764
3₁(735)	→	736
3₁(42)	→	43
3₁(8)	→	9
3₁(325)	→	326
3₁(319)	→	320
3₁(315)	→	316
3₁(52)	→	53
3₁(733)	→	734
3₁(780)	→	781
3₁(365)	→	366
3₁(367)	→	368
3₁(391)	→	392
3₁(551)	→	552
3₁(792)	→	793
3₁(321)	→	322
3₁(549)	→	550
3₁(269)	→	270
3₁(288)	→	289
3₁(380)	→	381
3₁(331)	→	332
3₁(504)	→	505
3₁(28)	→	29
3₁(270)	→	271
3₁(152)	→	153
3₁(557)	→	558
3₁(44)	→	45
3₂(455)	→	456
3₂(441)	→	442
3₂(542)	→	543
3₂(571)	→	572
3₂(446)	→	447
3₂(574)	→	575
3₂(539)	→	540
1₂(522)	→	523
1₂(414)	→	415
1₂(416)	→	417
1₂(425)	→	426
1₂(458)	→	459
1₂(415)	→	416
1₂(703)	→	704
1₂(706)	→	707
1₂(524)	→	525
1₂(573)	→	574
1₂(743)	→	744
1₂(741)	→	742
1₂(716)	→	717
1₂(818)	→	819
1₂(526)	→	527
1₂(449)	→	450
1₂(749)	→	750
1₂(719)	→	720
1₂(747)	→	748
1₂(427)	→	428
5₂(525)	→	526
5₂(541)	→	542
5₂(457)	→	458
5₂(448)	→	449
5₂(705)	→	706
5₂(718)	→	719
3₃(769)	→	770
2₁(253)	→	254
2₁(618)	→	619
2₁(371)	→	372
2₁(113)	→	114
2₁(58)	→	59
2₁(402)	→	403
2₁(363)	→	364
2₁(412)	→	413
2₁(255)	→	256
2₁(290)	→	291
2₁(337)	→	338
2₁(285)	→	286
2₁(620)	→	621
2₁(279)	→	280
2₁(268)	→	269
2₁(281)	→	282
2₁(312)	→	313
2₁(404)	→	405
2₁(277)	→	278
2₁(481)	→	482
2₁(333)	→	334
2₁(185)	→	186
2₁(266)	→	267
2₁(237)	→	238
2₁(242)	→	243
2₁(10)	→	11
2₁(98)	→	99
2₁(206)	→	207
2₁(283)	→	284
2₁(499)	→	500
2₁(379)	→	380
3₀(3)	→	5
3₀(6)	→	5
3₀(5)	→	5
3₀(4)	→	5
3₀(2)	→	5
3₀(1)	→	5
4₃(770)	→	771
4₃(768)	→	769
4₃(767)	→	768
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
4₂(454)	→	455
4₂(774)	→	775
4₂(440)	→	441
4₂(543)	→	544
4₂(445)	→	446
4₂(447)	→	448
4₂(776)	→	777
4₂(761)	→	762
4₂(453)	→	454
4₂(757)	→	758
4₂(444)	→	445
4₂(570)	→	571
4₂(442)	→	443
4₂(572)	→	573
4₂(439)	→	440
4₂(755)	→	756
4₂(778)	→	779
4₂(456)	→	457
5₃(771)	→	772
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
1₁(101)	→	102
1₁(617)	→	618
1₁(112)	→	113
1₁(626)	→	627
1₁(100)	→	101
1₁(802)	→	803
1₁(479)	→	480
1₁(796)	→	797
1₁(342)	→	343
1₁(362)	→	363
1₁(330)	→	331
1₁(141)	→	142
1₁(370)	→	371
1₁(655)	→	656
1₁(358)	→	359
1₁(304)	→	305
1₁(616)	→	617
1₁(128)	→	129
1₁(373)	→	374
1₁(798)	→	799
1₁(184)	→	185
1₁(393)	→	394
1₁(339)	→	340
1₁(356)	→	357
1₁(139)	→	140
1₁(568)	→	569
1₁(273)	→	274
1₁(384)	→	385
1₁(806)	→	807
1₁(480)	→	481
1₁(354)	→	355
1₁(197)	→	198
1₁(311)	→	312
1₁(195)	→	196
1₁(57)	→	58
1₁(302)	→	303
1₁(110)	→	111
1₁(126)	→	127
1₁(205)	→	206
1₁(615)	→	616
1₁(115)	→	116
1₁(352)	→	353
1₁(12)	→	13
1₁(111)	→	112
1₁(204)	→	205
1₁(751)	→	752
1₁(272)	→	273
1₁(317)	→	318
5₁(340)	→	341
5₁(303)	→	304
5₁(179)	→	180
5₁(99)	→	100
5₁(782)	→	783
5₁(462)	→	463
5₁(198)	→	199
5₁(477)	→	478
5₁(202)	→	203
5₁(217)	→	218
5₁(215)	→	216
5₁(308)	→	309
5₁(306)	→	307
5₁(727)	→	728
5₁(656)	→	657
5₁(228)	→	229
5₁(725)	→	726
5₁(372)	→	373
5₁(336)	→	337
5₁(619)	→	620
5₁(226)	→	227
5₁(209)	→	210
4₀(3)	→	2
4₀(5)	→	2
4₀(2)	→	2
4₀(4)	→	2
4₀(1)	→	2
4₀(6)	→	2
1₀(2)	→	3
1₀(4)	→	3
1₀(3)	→	3
1₀(6)	→	3
1₀(1)	→	3
1₀(5)	→	3
4₁(177)	→	178
4₁(166)	→	167
4₁(437)	→	438
4₁(508)	→	509
4₁(341)	→	342
4₁(69)	→	70
4₁(501)	→	502
4₁(71)	→	72
4₁(153)	→	154
4₁(681)	→	682
4₁(657)	→	658
4₁(271)	→	272
4₁(361)	→	362
4₁(502)	→	503
4₁(84)	→	85
4₁(168)	→	169
4₁(343)	→	344
4₁(151)	→	152
4₁(329)	→	330
4₁(316)	→	317
4₁(654)	→	655
4₁(196)	→	197
4₁(310)	→	311
4₁(155)	→	156
4₁(299)	→	300
4₁(460)	→	461
4₁(56)	→	57
4₁(240)	→	241
4₁(753)	→	754
4₁(82)	→	83
4₁(54)	→	55
4₁(327)	→	328
4₁(11)	→	12
4₁(800)	→	801
4₁(289)	→	290
4₁(287)	→	288
4₁(96)	→	97
4₁(784)	→	785
4₁(503)	→	504
1₃(772)	→	773
0₁(383)	→	384
0₁(207)	→	208
0₁(187)	→	188
0₁(478)	→	479
0₁(183)	→	184
0₁(497)	→	498
0₁(529)	→	530
0₁(191)	→	192
0₁(334)	→	335
0₁(203)	→	204
0₁(313)	→	314
0₁(13)	→	14
0₁(482)	→	483
0₁(193)	→	194
0₁(790)	→	791
0₁(533)	→	534
0₁(816)	→	817
0₁(375)	→	376
0₁(721)	→	722
0₁(301)	→	302
0₁(369)	→	370
0₁(381)	→	382
0₁(239)	→	240
0₁(189)	→	190
0₁(377)	→	378
0₂(523)	→	524
0₂(702)	→	703
0₂(715)	→	716
0₂(419)	→	420
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
2₂(527)	→	528
2₂(714)	→	715
2₂(808)	→	809
2₂(717)	→	718
2₂(814)	→	815
2₂(417)	→	418
2₂(540)	→	541
2₂(701)	→	702
2₂(418)	→	419
2₂(704)	→	705

The automaton is closed under rewriting as it is compatible.