Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/5011)

The rewrite relation of the following TRS is considered.

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

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

1(2(0(x1)))	→	1(0(5(1(5(4(1(0(4(0(x1))))))))))	(24)
3(1(1(x1)))	→	2(4(1(5(2(2(2(1(2(1(x1))))))))))	(25)
3(0(0(0(x1))))	→	5(4(3(3(5(2(0(4(2(4(x1))))))))))	(26)
3(2(0(1(x1))))	→	2(3(4(2(1(4(5(2(1(1(x1))))))))))	(27)
3(5(3(1(x1))))	→	4(5(2(3(4(2(5(4(5(3(x1))))))))))	(28)
3(1(3(2(0(x1)))))	→	2(1(3(1(3(1(2(1(0(1(x1))))))))))	(29)
3(5(4(3(0(x1)))))	→	5(5(4(4(2(1(5(2(0(2(x1))))))))))	(30)
3(1(2(5(0(x1)))))	→	4(2(0(3(4(2(5(2(4(2(x1))))))))))	(31)
0(1(3(1(2(x1)))))	→	0(3(2(5(5(1(5(4(1(0(x1))))))))))	(32)
0(2(2(2(5(0(x1))))))	→	1(2(1(5(2(0(3(4(5(2(x1))))))))))	(33)
0(2(5(0(0(2(x1))))))	→	1(0(4(4(4(1(2(4(0(4(x1))))))))))	(34)
2(0(3(5(0(2(x1))))))	→	2(0(0(5(4(1(5(3(5(2(x1))))))))))	(35)
5(1(2(0(1(2(x1))))))	→	5(4(5(2(2(3(1(4(5(2(x1))))))))))	(36)
2(0(1(5(1(5(x1))))))	→	4(0(1(1(3(4(0(0(5(4(x1))))))))))	(37)
0(1(2(2(2(5(0(x1)))))))	→	0(1(0(1(4(1(3(2(3(0(x1))))))))))	(38)
5(1(3(5(3(5(0(x1)))))))	→	5(1(5(4(1(0(4(3(1(0(x1))))))))))	(39)
3(4(4(1(5(1(1(x1)))))))	→	5(5(2(0(1(4(4(3(0(1(x1))))))))))	(40)
3(5(0(3(2(3(1(x1)))))))	→	5(2(3(0(4(5(1(0(4(1(x1))))))))))	(41)
1(1(2(4(2(5(1(x1)))))))	→	3(0(1(3(4(1(4(1(4(4(x1))))))))))	(42)
0(1(2(0(2(0(2(x1)))))))	→	0(4(4(4(2(4(3(2(0(2(x1))))))))))	(43)
5(3(1(5(5(4(2(x1)))))))	→	4(4(3(4(4(4(1(2(1(2(x1))))))))))	(44)
1(2(5(5(0(0(3(x1)))))))	→	3(0(1(2(3(2(3(4(2(0(x1))))))))))	(45)
5(0(3(2(5(1(3(x1)))))))	→	4(0(0(2(5(4(0(4(3(5(x1))))))))))	(46)

1.1 Bounds

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

final states:

{7}

transitions:

730	→	304
854	→	759
223	→	110
111	→	54
793	→	57
650	→	136
818	→	103
818	→	284
29	→	7
29	→	224
29	→	56
29	→	275
29	→	80
29	→	31
29	→	20
29	→	104
29	→	759
29	→	770
835	→	847
835	→	880
830	→	256
789	→	197
81	→	217
81	→	283
81	→	125
81	→	294
81	→	69
81	→	30
81	→	19
81	→	45
81	→	102
81	→	7
81	→	196
81	→	20
81	→	354
81	→	756
791	→	57
732	→	304
80	→	755
80	→	777
80	→	802
80	→	806
533	→	80
533	→	790
715	→	731
715	→	800
103	→	112
103	→	135
103	→	274
289	→	250
743	→	706
640	→	775
640	→	779
640	→	851
641	→	80
728	→	295
136	→	156
149	→	318
211	→	664
133	→	353
133	→	383
133	→	534
133	→	555
260	→	133
676	→	665
120	→	78
120	→	705
39	→	575
39	→	634
772	→	759
460	→	70
460	→	294
460	→	69
460	→	30
460	→	19
460	→	45
460	→	102
460	→	7
460	→	296
460	→	797
838	→	295
805	→	103
134	→	7
134	→	217
134	→	283
134	→	125
134	→	196
134	→	20
134	→	81
774	→	31
55	→	7
55	→	70
55	→	197
55	→	296
55	→	295
55	→	797
756	→	354
674	→	224
674	→	56
674	→	7
674	→	57
674	→	80
674	→	31
674	→	759
674	→	803
674	→	770
889	→	244
20	→	125
20	→	196
20	→	283
673	→	835
673	→	837
31	→	56
31	→	80
31	→	224
31	→	7
40	→	7
40	→	70
40	→	103
40	→	284
40	→	797
826	→	244
716	→	39
570	→	80
778	→	46
770	→	759
392	→	819
323	→	133
881	→	80
296	→	636
253	→	7
253	→	224
253	→	56
253	→	57
253	→	80
253	→	31
253	→	275
253	→	759
253	→	803
253	→	770
79	→	7
79	→	70
79	→	296
79	→	103
79	→	284
79	→	71
79	→	295
79	→	797
556	→	103
251	→	553
178	→	855
824	→	183
302	→	190
554	→	103
773	→	853
773	→	861
773	→	888
88	→	39
54	→	662
799	→	80
105	→	254
363	→	275
776	→	46
831	→	849
831	→	874
204	→	133
204	→	448
906	→	136
143	→	28
143	→	649
569	→	831
569	→	905
803	→	80
313	→	224
313	→	56
313	→	80
313	→	31
313	→	275
313	→	759
313	→	770
797	→	70
232	→	54
28	→	450
28	→	675
28	→	771
118	→	733
449	→	57
212	→	54
850	→	304
801	→	80
252	→	721
252	→	727
820	→	183
862	→	70
795	→	70
535	→	80
535	→	792
672	→	804
282	→	78
7	→	19
7	→	30
7	→	45
7	→	69
7	→	102
7	→	294
663	→	652
635	→	148
182	→	53
126	→	205
30	→	769
30	→	796
30	→	827
137	→	177
64	→	39
46	→	148
46	→	183
46	→	244
162	→	303
162	→	532
856	→	62
393	→	70
393	→	294
393	→	69
393	→	30
393	→	19
393	→	45
393	→	102
393	→	7
393	→	197
393	→	797
828	→	244
836	→	39
714	→	71
714	→	294
714	→	69
714	→	30
714	→	19
714	→	45
714	→	102
714	→	7
714	→	295
768	→	70
768	→	206
768	→	797
832	→	39
320	→	821
320	→	823
722	→	39
340	→	21
142	→	561
132	→	715
132	→	882
848	→	304
807	→	103
852	→	304
210	→	651
210	→	808
822	→	809
70	→	829
875	→	80
576	→	562
163	→	39
163	→	339
721	→	729
721	→	798
155	→	27
312	→	773
312	→	794
312	→	825
191	→	78
661	→	103
661	→	7
661	→	284
883	→	136
5₁(727)	→	728
5₁(388)	→	389
5₁(36)	→	37
5₁(54)	→	55
5₁(905)	→	906
5₁(210)	→	211
5₁(639)	→	640
5₁(458)	→	459
5₁(140)	→	141
5₁(160)	→	161
5₁(322)	→	323
5₁(451)	→	452
5₁(114)	→	115
5₁(157)	→	158
5₁(837)	→	838
5₁(127)	→	128
5₁(649)	→	650
5₁(129)	→	130
5₁(882)	→	883
5₁(566)	→	567
5₁(183)	→	184
5₁(392)	→	393
5₁(652)	→	653
5₁(181)	→	182
5₁(24)	→	25
5₁(636)	→	637
5₁(299)	→	300
5₁(110)	→	111
5₁(105)	→	106
5₁(50)	→	51
5₁(130)	→	131
5₁(58)	→	59
5₁(320)	→	321
5₁(564)	→	565
5₁(135)	→	136
5₁(453)	→	454
5₁(70)	→	71
5₁(294)	→	295
5₁(567)	→	568
5₁(26)	→	27
5₁(227)	→	228
5₁(72)	→	73
5₁(77)	→	78
3₂(785)	→	786
3₂(786)	→	787
3₂(813)	→	814
0₂(311)	→	312
0₂(303)	→	304
0₂(733)	→	734
0₂(305)	→	306
0₂(361)	→	362
0₂(810)	→	811
0₂(782)	→	783
0₂(735)	→	736
0₂(816)	→	817
0₂(851)	→	852
0₂(731)	→	732
0₂(355)	→	356
0₂(729)	→	730
0₂(811)	→	812
0₂(755)	→	756
0₂(741)	→	742
0₂(849)	→	850
0₂(847)	→	848
0₂(353)	→	354
1₂(815)	→	816
1₂(309)	→	310
1₂(736)	→	737
1₂(306)	→	307
1₂(362)	→	363
1₂(739)	→	740
1₂(312)	→	313
1₂(742)	→	743
1₂(765)	→	766
1₂(769)	→	770
1₂(814)	→	815
1₂(771)	→	772
1₂(359)	→	360
1₂(356)	→	357
1₂(760)	→	761
1₂(853)	→	854
1₁(220)	→	221
1₁(208)	→	209
1₁(247)	→	248
1₁(87)	→	88
1₁(128)	→	129
1₁(245)	→	246
1₁(874)	→	875
1₁(211)	→	212
1₁(276)	→	277
1₁(22)	→	23
1₁(790)	→	791
1₁(201)	→	202
1₁(158)	→	159
1₁(318)	→	319
1₁(792)	→	793
1₁(81)	→	82
1₁(798)	→	799
1₁(250)	→	251
1₁(141)	→	142
1₁(880)	→	881
1₁(37)	→	38
1₁(151)	→	152
1₁(32)	→	33
1₁(534)	→	535
1₁(773)	→	774
1₁(85)	→	86
1₁(562)	→	563
1₁(800)	→	801
1₁(637)	→	638
1₁(565)	→	566
1₁(707)	→	708
1₁(802)	→	803
1₁(125)	→	126
1₁(321)	→	322
1₁(28)	→	29
1₁(705)	→	706
1₁(274)	→	275
1₁(658)	→	659
1₁(177)	→	178
1₁(56)	→	57
1₁(448)	→	449
1₁(188)	→	189
1₁(106)	→	107
1₁(25)	→	26
1₁(657)	→	658
1₁(668)	→	669
1₁(30)	→	31
1₁(189)	→	190
1₁(226)	→	227
1₁(532)	→	533
1₁(199)	→	200
1₁(83)	→	84
1₁(671)	→	672
1₁(60)	→	61
1₁(203)	→	204
1₁(666)	→	667
4₀(7)	→	7
3₀(7)	→	7
2₂(763)	→	764
2₂(761)	→	762
2₂(783)	→	784
2₂(767)	→	768
2₂(762)	→	763
2₂(759)	→	760
2₂(780)	→	781
5₀(7)	→	7
4₁(827)	→	828
4₁(108)	→	109
4₁(277)	→	278
4₁(112)	→	113
4₁(186)	→	187
4₁(825)	→	826
4₁(246)	→	247
4₁(218)	→	219
4₁(296)	→	297
4₁(47)	→	48
4₁(244)	→	245
4₁(78)	→	79
4₁(279)	→	280
4₁(255)	→	256
4₁(667)	→	668
4₁(278)	→	279
4₁(281)	→	282
4₁(391)	→	392
4₁(634)	→	635
4₁(153)	→	154
4₁(829)	→	830
4₁(257)	→	258
4₁(53)	→	54
4₁(655)	→	656
4₁(136)	→	137
4₁(152)	→	153
4₁(669)	→	670
4₁(59)	→	60
4₁(775)	→	776
4₁(284)	→	285
4₁(339)	→	340
4₁(709)	→	710
4₁(823)	→	824
4₁(708)	→	709
4₁(385)	→	386
4₁(20)	→	21
4₁(651)	→	652
4₁(660)	→	661
4₁(248)	→	249
4₁(452)	→	453
4₁(209)	→	210
4₁(116)	→	117
4₁(383)	→	384
4₁(149)	→	150
4₁(159)	→	160
4₁(154)	→	155
4₁(777)	→	778
4₁(888)	→	889
4₁(298)	→	299
4₁(319)	→	320
4₁(74)	→	75
4₁(665)	→	666
4₁(206)	→	207
4₁(62)	→	63
4₁(224)	→	225
4₁(664)	→	665
4₁(712)	→	713
4₁(219)	→	220
4₁(819)	→	820
4₁(638)	→	639
4₁(662)	→	663
4₁(126)	→	127
4₁(45)	→	46
4₁(713)	→	714
4₁(109)	→	110
4₁(455)	→	456
4₁(38)	→	39
4₁(228)	→	229
4₁(23)	→	24
4₁(563)	→	564
4₁(259)	→	260
4₁(71)	→	72
4₁(710)	→	711
4₁(459)	→	460
4₁(258)	→	259
4₁(675)	→	676
4₁(200)	→	201
0₁(184)	→	185
0₁(138)	→	139
0₁(48)	→	49
0₁(229)	→	230
0₁(297)	→	298
0₁(185)	→	186
0₁(561)	→	562
0₁(575)	→	576
0₁(21)	→	22
0₁(672)	→	673
0₁(118)	→	119
0₁(19)	→	20
0₁(202)	→	203
0₁(225)	→	226
0₁(190)	→	191
0₁(133)	→	134
0₁(251)	→	252
0₁(831)	→	832
0₁(80)	→	81
0₁(640)	→	641
0₁(386)	→	387
0₁(148)	→	149
0₁(162)	→	163
0₁(715)	→	716
0₁(835)	→	836
0₁(221)	→	222
0₁(659)	→	660
0₁(721)	→	722
0₁(27)	→	28
0₁(103)	→	104
0₁(161)	→	162
0₁(654)	→	655
0₁(207)	→	208
0₁(653)	→	654
0₁(301)	→	302
2₀(7)	→	7
0₀(7)	→	7
3₁(187)	→	188
3₁(711)	→	712
3₁(861)	→	862
3₁(456)	→	457
3₁(217)	→	218
3₁(389)	→	390
3₁(670)	→	671
3₁(796)	→	797
3₁(117)	→	118
3₁(63)	→	64
3₁(254)	→	255
3₁(69)	→	70
3₁(52)	→	53
3₁(390)	→	391
3₁(75)	→	76
3₁(249)	→	250
3₁(205)	→	206
3₁(137)	→	138
3₁(280)	→	281
3₁(84)	→	85
3₁(230)	→	231
3₁(656)	→	657
3₁(196)	→	197
3₁(295)	→	296
3₁(794)	→	795
3₁(252)	→	253
3₁(132)	→	133
3₁(673)	→	674
3₁(450)	→	451
3₁(569)	→	570
3₁(285)	→	286
3₁(198)	→	199
3₁(156)	→	157
3₁(51)	→	52
3₁(287)	→	288
3₁(86)	→	87
3₁(178)	→	179
2₁(82)	→	83
2₁(855)	→	856
2₁(180)	→	181
2₁(39)	→	40
2₁(806)	→	807
2₁(115)	→	116
2₁(31)	→	32
2₁(102)	→	103
2₁(222)	→	223
2₁(275)	→	276
2₁(300)	→	301
2₁(179)	→	180
2₁(387)	→	388
2₁(73)	→	74
2₁(131)	→	132
2₁(706)	→	707
2₁(57)	→	58
2₁(107)	→	108
2₁(454)	→	455
2₁(804)	→	805
2₁(76)	→	77
2₁(150)	→	151
2₁(139)	→	140
2₁(46)	→	47
2₁(286)	→	287
2₁(457)	→	458
2₁(384)	→	385
2₁(256)	→	257
2₁(142)	→	143
2₁(34)	→	35
2₁(104)	→	105
2₁(61)	→	62
2₁(35)	→	36
2₁(33)	→	34
2₁(197)	→	198
2₁(49)	→	50
2₁(288)	→	289
2₁(553)	→	554
2₁(555)	→	556
2₁(568)	→	569
2₁(113)	→	114
2₁(231)	→	232
2₁(119)	→	120
2₁(283)	→	284
4₂(737)	→	738
4₂(781)	→	782
4₂(357)	→	358
4₂(779)	→	780
4₂(821)	→	822
4₂(734)	→	735
4₂(808)	→	809
4₂(304)	→	305
4₂(354)	→	355
4₂(817)	→	818
4₂(307)	→	308
4₂(812)	→	813
4₂(766)	→	767
4₂(787)	→	788
1₀(7)	→	7
5₂(784)	→	785
5₂(308)	→	309
5₂(764)	→	765
5₂(809)	→	810
5₂(358)	→	359
5₂(738)	→	739
5₂(788)	→	789
5₂(740)	→	741
5₂(360)	→	361
5₂(310)	→	311

The automaton is closed under rewriting as it is compatible.