Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3770)

The rewrite relation of the following TRS is considered.

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

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

3(3(1(x1)))	→	4(5(4(2(0(5(2(3(5(3(x1))))))))))	(17)
3(3(3(0(x1))))	→	0(4(4(5(0(3(5(3(4(5(x1))))))))))	(18)
1(3(3(3(0(x1)))))	→	0(1(5(0(1(3(0(4(4(5(x1))))))))))	(19)
3(3(3(2(1(x1)))))	→	5(0(4(0(5(3(2(1(1(4(x1))))))))))	(20)
2(2(4(4(1(x1)))))	→	2(2(0(1(1(1(0(2(1(1(x1))))))))))	(21)
3(4(1(3(3(0(x1))))))	→	0(0(3(0(3(2(0(3(4(4(x1))))))))))	(22)
0(4(3(3(3(3(x1))))))	→	4(5(3(5(0(1(2(0(0(3(x1))))))))))	(23)
0(4(3(1(0(4(x1))))))	→	0(0(0(5(0(0(0(3(2(2(x1))))))))))	(24)
1(4(4(4(1(4(x1))))))	→	1(4(5(5(5(3(3(0(1(4(x1))))))))))	(25)
3(2(2(5(3(1(0(x1)))))))	→	3(4(4(0(0(5(0(0(3(0(x1))))))))))	(26)
5(2(3(1(3(2(0(x1)))))))	→	0(2(3(2(3(2(1(3(4(0(x1))))))))))	(27)
1(3(5(3(3(1(1(x1)))))))	→	1(0(0(5(2(3(5(0(5(3(x1))))))))))	(28)
3(3(1(0(2(5(3(x1)))))))	→	5(5(4(4(2(3(2(3(4(3(x1))))))))))	(29)
1(0(4(2(4(1(4(x1)))))))	→	1(5(4(5(5(0(1(2(2(5(x1))))))))))	(30)
4(4(4(2(1(5(4(x1)))))))	→	4(0(1(0(3(5(4(1(1(4(x1))))))))))	(31)
3(3(3(5(4(1(5(x1)))))))	→	2(3(2(4(4(3(5(4(1(5(x1))))))))))	(32)

1.1 Bounds

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

final states:

{7}

transitions:

78	→	7
78	→	111
78	→	174
78	→	101
78	→	20
588	→	31
111	→	131
111	→	68
111	→	30
111	→	19
111	→	53
111	→	109
111	→	7
111	→	110
650	→	151
534	→	174
534	→	7
534	→	101
534	→	20
102	→	131
102	→	68
102	→	30
102	→	19
102	→	53
102	→	109
102	→	7
32	→	45
32	→	7
32	→	80
32	→	670
32	→	754
32	→	758
32	→	760
29	→	7
29	→	174
29	→	101
29	→	20
29	→	146
29	→	132
685	→	77
128	→	514
128	→	763
789	→	54
750	→	790
750	→	796
791	→	51
87	→	39
80	→	625
715	→	183
103	→	643
658	→	183
640	→	77
578	→	682
560	→	549
129	→	225
129	→	301
129	→	559
628	→	31
211	→	28
668	→	31
133	→	474
638	→	77
625	→	661
625	→	663
625	→	669
227	→	512
226	→	492
39	→	257
39	→	374
39	→	570
652	→	183
626	→	55
805	→	743
108	→	27
584	→	571
515	→	183
642	→	112
698	→	19
698	→	710
185	→	641
55	→	122
55	→	7
55	→	69
55	→	626
55	→	744
756	→	743
130	→	7
130	→	122
130	→	69
20	→	101
20	→	174
20	→	131
20	→	68
20	→	30
20	→	19
20	→	53
20	→	109
20	→	7
20	→	112
20	→	642
473	→	452
713	→	183
31	→	183
31	→	212
31	→	659
31	→	755
40	→	7
40	→	174
40	→	20
40	→	69
40	→	146
40	→	132
40	→	212
40	→	183
40	→	31
40	→	562
40	→	549
40	→	652
101	→	583
101	→	587
101	→	633
524	→	51
778	→	54
770	→	549
777	→	804
777	→	806
334	→	649
723	→	31
751	→	769
751	→	775
751	→	777
751	→	788
634	→	31
536	→	527
735	→	31
235	→	174
235	→	7
235	→	101
235	→	20
38	→	451
79	→	712
79	→	753
662	→	549
562	→	20
760	→	743
161	→	699
21	→	155
614	→	535
614	→	333
614	→	477
614	→	69
141	→	7
141	→	20
526	→	521
311	→	174
311	→	7
311	→	101
311	→	20
788	→	798
788	→	800
337	→	51
220	→	77
741	→	31
54	→	79
54	→	527
54	→	548
54	→	561
799	→	549
52	→	39
52	→	716
288	→	46
498	→	28
764	→	743
776	→	20
717	→	520
53	→	651
53	→	757
803	→	743
117	→	86
797	→	183
265	→	635
28	→	472
28	→	516
582	→	571
557	→	684
557	→	693
557	→	714
801	→	20
478	→	132
580	→	101
580	→	112
580	→	19
580	→	53
580	→	109
580	→	131
580	→	68
580	→	30
580	→	7
580	→	174
580	→	20
754	→	743
766	→	183
795	→	745
63	→	7
63	→	174
63	→	101
63	→	20
636	→	77
697	→	718
697	→	734
697	→	736
7	→	19
7	→	30
7	→	53
7	→	68
7	→	109
7	→	131
694	→	51
69	→	333
69	→	477
69	→	535
234	→	637
234	→	657
758	→	743
182	→	62
719	→	571
681	→	562
681	→	549
579	→	665
579	→	667
579	→	671
579	→	697
162	→	129
752	→	626
752	→	794
752	→	744
709	→	112
709	→	642
458	→	86
586	→	31
572	→	606
683	→	77
190	→	518
154	→	39
666	→	571
664	→	20
267	→	174
267	→	7
267	→	20
517	→	183
693	→	742
132	→	146
132	→	388
259	→	287
670	→	54
711	→	19
790	→	802
375	→	79
807	→	183
558	→	112
558	→	101
558	→	131
558	→	68
558	→	30
558	→	19
558	→	53
558	→	109
558	→	7
558	→	174
558	→	20
266	→	581
266	→	585
266	→	627
660	→	183
680	→	720
680	→	722
680	→	740
669	→	759
669	→	765
476	→	181
396	→	146
396	→	131
396	→	68
396	→	30
396	→	19
396	→	53
396	→	109
396	→	7
396	→	132
70	→	525
737	→	31
721	→	571
56	→	205
644	→	86
191	→	129
395	→	639
395	→	655
656	→	183
513	→	156
5₁(260)	→	261
5₁(156)	→	157
5₁(126)	→	127
5₁(36)	→	37
5₁(226)	→	227
5₁(765)	→	766
5₁(521)	→	522
5₁(187)	→	188
5₁(796)	→	797
5₁(657)	→	658
5₁(527)	→	528
5₁(263)	→	264
5₁(159)	→	160
5₁(190)	→	191
5₁(27)	→	28
5₁(30)	→	31
5₁(106)	→	107
5₁(587)	→	588
5₁(659)	→	660
5₁(62)	→	63
5₁(306)	→	307
5₁(214)	→	215
5₁(585)	→	586
5₁(806)	→	807
5₁(394)	→	395
5₁(667)	→	668
5₁(127)	→	128
5₁(206)	→	207
5₁(233)	→	234
5₁(392)	→	393
5₁(188)	→	189
5₁(181)	→	182
5₁(734)	→	735
5₁(712)	→	713
5₁(494)	→	495
5₁(643)	→	644
5₁(115)	→	116
5₁(50)	→	51
5₁(58)	→	59
5₁(23)	→	24
5₁(33)	→	34
5₁(475)	→	476
5₁(135)	→	136
5₁(20)	→	21
5₁(514)	→	515
5₁(310)	→	311
5₁(257)	→	258
5₁(722)	→	723
5₁(125)	→	126
5₁(229)	→	230
5₁(516)	→	517
5₁(651)	→	652
5₁(655)	→	656
5₁(457)	→	458
5₁(714)	→	715
4₂(706)	→	707
4₂(763)	→	764
4₂(755)	→	756
4₂(804)	→	805
4₂(757)	→	758
4₂(802)	→	803
4₂(557)	→	558
4₂(750)	→	751
4₂(606)	→	607
4₂(578)	→	579
4₂(753)	→	754
4₂(571)	→	572
4₂(577)	→	578
4₂(707)	→	708
4₂(555)	→	556
4₂(759)	→	760
4₂(742)	→	743
0₂(699)	→	700
0₂(702)	→	703
0₂(610)	→	611
0₂(579)	→	580
0₂(613)	→	614
0₂(705)	→	706
0₂(553)	→	554
0₂(701)	→	702
0₂(607)	→	608
0₂(744)	→	745
0₂(704)	→	705
0₂(794)	→	795
0₂(575)	→	576
1₂(609)	→	610
1₂(743)	→	744
1₂(751)	→	752
1₂(612)	→	613
0₁(134)	→	135
0₁(208)	→	209
0₁(677)	→	678
0₁(112)	→	113
0₁(680)	→	681
0₁(101)	→	102
0₁(113)	→	114
0₁(334)	→	335
0₁(160)	→	161
0₁(102)	→	103
0₁(495)	→	496
0₁(454)	→	455
0₁(114)	→	115
0₁(137)	→	138
0₁(391)	→	392
0₁(161)	→	162
0₁(309)	→	310
0₁(131)	→	132
0₁(81)	→	82
0₁(230)	→	231
0₁(492)	→	493
0₁(71)	→	72
0₁(35)	→	36
0₁(388)	→	389
0₁(262)	→	263
0₁(186)	→	187
0₁(210)	→	211
0₁(523)	→	524
0₁(697)	→	698
0₁(133)	→	134
0₁(46)	→	47
0₁(49)	→	50
0₁(674)	→	675
0₁(86)	→	87
0₁(155)	→	156
0₁(266)	→	267
0₁(24)	→	25
0₁(456)	→	457
0₁(496)	→	497
0₁(477)	→	478
0₁(39)	→	40
0₁(679)	→	680
0₁(105)	→	106
0₁(136)	→	137
0₁(512)	→	513
0₁(122)	→	123
0₁(59)	→	60
0₁(61)	→	62
0₁(455)	→	456
0₁(116)	→	117
0₁(493)	→	494
0₁(75)	→	76
0₁(84)	→	85
0₁(307)	→	308
2₀(7)	→	7
0₀(7)	→	7
2₂(551)	→	552
2₂(554)	→	555
5₀(7)	→	7
2₁(25)	→	26
2₁(218)	→	219
2₁(533)	→	534
2₁(82)	→	83
2₁(151)	→	152
2₁(153)	→	154
2₁(682)	→	683
2₁(333)	→	334
2₁(304)	→	305
2₁(184)	→	185
2₁(56)	→	57
2₁(472)	→	473
2₁(22)	→	23
2₁(451)	→	452
2₁(452)	→	453
2₁(149)	→	150
2₁(103)	→	104
2₁(70)	→	71
2₁(158)	→	159
2₁(176)	→	177
2₁(110)	→	111
2₁(183)	→	184
2₁(109)	→	110
2₁(77)	→	78
2₁(76)	→	77
2₁(228)	→	229
2₁(531)	→	532
2₁(637)	→	638
2₁(231)	→	232
2₁(684)	→	685
2₁(389)	→	390
2₁(635)	→	636
2₁(178)	→	179
2₁(639)	→	640
2₁(675)	→	676
3₁(474)	→	475
3₁(393)	→	394
3₁(673)	→	674
3₁(123)	→	124
3₁(132)	→	133
3₁(147)	→	148
3₁(261)	→	262
3₁(305)	→	306
3₁(532)	→	533
3₁(561)	→	562
3₁(152)	→	153
3₁(227)	→	228
3₁(21)	→	22
3₁(175)	→	176
3₁(157)	→	158
3₁(34)	→	35
3₁(19)	→	20
3₁(800)	→	801
3₁(32)	→	33
3₁(225)	→	226
3₁(140)	→	141
3₁(215)	→	216
3₁(676)	→	677
3₁(85)	→	86
3₁(80)	→	81
3₁(522)	→	523
3₁(775)	→	776
3₁(111)	→	112
3₁(177)	→	178
3₁(83)	→	84
3₁(453)	→	454
3₁(107)	→	108
3₁(124)	→	125
3₁(259)	→	260
3₁(47)	→	48
3₁(207)	→	208
3₁(663)	→	664
3₁(219)	→	220
3₁(678)	→	679
3₁(641)	→	642
3₁(57)	→	58
3₁(150)	→	151
3₁(528)	→	529
3₁(649)	→	650
1₀(7)	→	7
4₀(7)	→	7
1₁(72)	→	73
1₁(302)	→	303
1₁(55)	→	56
1₁(212)	→	213
1₁(129)	→	130
1₁(716)	→	717
1₁(69)	→	70
1₁(104)	→	105
1₁(335)	→	336
1₁(390)	→	391
1₁(148)	→	149
1₁(336)	→	337
1₁(788)	→	789
1₁(73)	→	74
1₁(48)	→	49
1₁(68)	→	69
1₁(518)	→	519
1₁(209)	→	210
1₁(74)	→	75
1₁(54)	→	55
1₁(303)	→	304
1₁(519)	→	520
1₁(625)	→	626
1₁(185)	→	186
1₁(51)	→	52
4₁(669)	→	670
4₁(232)	→	233
4₁(308)	→	309
4₁(53)	→	54
4₁(26)	→	27
4₁(37)	→	38
4₁(374)	→	375
4₁(736)	→	737
4₁(777)	→	778
4₁(535)	→	536
4₁(180)	→	181
4₁(710)	→	711
4₁(497)	→	498
4₁(31)	→	32
4₁(529)	→	530
4₁(205)	→	206
4₁(217)	→	218
4₁(264)	→	265
4₁(287)	→	288
4₁(45)	→	46
4₁(216)	→	217
4₁(179)	→	180
4₁(138)	→	139
4₁(525)	→	526
4₁(60)	→	61
4₁(633)	→	634
4₁(28)	→	29
4₁(258)	→	259
4₁(627)	→	628
4₁(790)	→	791
4₁(79)	→	80
4₁(139)	→	140
4₁(38)	→	39
4₁(530)	→	531
4₁(520)	→	521
4₁(265)	→	266
4₁(146)	→	147
4₁(671)	→	672
4₁(174)	→	175
4₁(672)	→	673
4₁(301)	→	302
4₁(234)	→	235
4₁(740)	→	741
4₁(395)	→	396
4₁(693)	→	694
4₁(213)	→	214
4₁(189)	→	190
4₁(128)	→	129
3₂(572)	→	573
3₂(700)	→	701
3₂(661)	→	662
3₂(708)	→	709
3₂(608)	→	609
3₂(574)	→	575
3₂(550)	→	551
3₂(746)	→	747
3₂(559)	→	560
3₂(769)	→	770
3₂(798)	→	799
3₂(745)	→	746
3₂(548)	→	549
3₀(7)	→	7
5₂(747)	→	748
5₂(549)	→	550
5₂(718)	→	719
5₂(611)	→	612
5₂(576)	→	577
5₂(556)	→	557
5₂(749)	→	750
5₂(720)	→	721
5₂(552)	→	553
5₂(573)	→	574
5₂(703)	→	704
5₂(581)	→	582
5₂(748)	→	749
5₂(583)	→	584
5₂(570)	→	571
5₂(665)	→	666

The automaton is closed under rewriting as it is compatible.