Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96438)

The rewrite relation of the following TRS is considered.

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

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(2(1(0(x1))))	→	3(4(1(x1)))	(26)
2(4(0(2(1(x1)))))	→	4(5(4(3(x1))))	(27)
2(3(0(3(3(x1)))))	→	1(4(2(3(x1))))	(28)
4(0(1(2(5(x1)))))	→	5(4(5(5(x1))))	(29)
5(0(5(4(1(0(x1))))))	→	5(3(0(4(0(3(x1))))))	(30)
5(1(2(5(2(0(x1))))))	→	4(5(1(2(5(x1)))))	(31)
5(5(1(5(3(0(x1))))))	→	4(5(1(5(0(x1)))))	(32)
3(4(5(4(1(5(2(2(x1))))))))	→	3(0(1(0(3(3(2(2(x1))))))))	(33)
4(2(2(1(4(2(0(0(0(x1)))))))))	→	4(4(3(3(4(0(0(0(x1))))))))	(34)
2(3(0(2(4(3(4(4(2(x1)))))))))	→	1(3(3(1(4(3(4(3(x1))))))))	(35)
3(5(3(2(3(2(3(4(1(0(x1))))))))))	→	3(5(2(4(3(0(3(4(1(x1)))))))))	(36)
2(2(4(1(3(4(0(5(1(2(0(x1)))))))))))	→	2(4(4(5(0(1(5(0(4(0(0(x1)))))))))))	(37)
5(1(4(4(2(4(2(0(3(3(4(4(x1))))))))))))	→	5(2(5(5(5(1(3(4(0(4(4(x1)))))))))))	(38)
3(3(2(2(0(2(5(5(0(0(3(5(x1))))))))))))	→	3(4(2(5(0(2(5(1(4(5(5(x1)))))))))))	(39)
2(2(5(2(0(5(1(5(5(2(0(2(0(x1)))))))))))))	→	2(5(1(0(1(0(4(1(3(4(5(x1)))))))))))	(40)
4(0(1(0(4(5(0(2(4(4(1(3(0(x1)))))))))))))	→	4(4(2(2(0(0(4(0(1(4(4(0(0(x1)))))))))))))	(41)
3(0(4(1(0(4(3(5(2(0(1(1(4(2(1(x1)))))))))))))))	→	3(3(0(0(2(5(0(2(3(0(5(4(0(1(1(x1)))))))))))))))	(42)
3(2(3(1(4(4(4(1(5(4(4(2(5(3(2(x1)))))))))))))))	→	3(2(5(3(1(5(3(3(5(1(1(1(3(3(2(x1)))))))))))))))	(43)
5(0(0(5(1(3(3(2(3(5(2(5(2(4(5(x1)))))))))))))))	→	5(3(1(4(4(4(4(1(3(1(4(5(3(2(5(x1)))))))))))))))	(44)
2(4(5(5(4(0(2(3(1(2(2(1(4(2(0(0(x1))))))))))))))))	→	1(5(3(2(5(2(0(3(4(5(3(2(0(1(1(5(0(x1)))))))))))))))))	(45)
4(3(2(0(1(0(4(2(2(4(1(0(3(5(1(1(0(x1)))))))))))))))))	→	4(5(5(2(2(2(0(4(4(5(1(0(2(2(4(0(x1))))))))))))))))	(46)
3(1(5(4(2(0(3(4(2(3(4(2(5(2(3(2(0(x1)))))))))))))))))	→	3(2(5(5(0(1(0(5(1(3(5(2(5(3(4(3(x1))))))))))))))))	(47)
2(0(0(1(0(0(3(4(0(2(0(5(4(1(2(4(5(4(5(4(x1))))))))))))))))))))	→	0(0(5(1(1(2(2(1(4(3(5(0(0(0(2(5(2(2(4(4(x1))))))))))))))))))))	(48)
1(2(3(0(4(5(4(1(1(4(2(5(4(4(4(2(5(0(1(0(3(x1)))))))))))))))))))))	→	4(1(1(2(3(5(5(0(5(3(3(3(2(2(2(5(4(0(2(4(3(x1)))))))))))))))))))))	(49)
1(1(2(2(0(4(5(3(2(1(2(0(2(1(3(0(0(1(2(3(3(x1)))))))))))))))))))))	→	1(0(1(5(5(2(4(5(4(3(5(3(4(3(4(2(5(4(3(x1)))))))))))))))))))	(50)

1.1 Bounds

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

final states:

{7}

transitions:

33	→	7
33	→	217
33	→	107
33	→	186
33	→	30
33	→	44
33	→	55
33	→	157
33	→	760
33	→	771
366	→	836
871	→	364
733	→	643
958	→	19
964	→	18
32	→	117
32	→	717
32	→	764
633	→	61
818	→	17
29	→	770
835	→	186
89	→	14
89	→	653
789	→	876
80	→	27
98	→	640
98	→	828
286	→	19
229	→	18
855	→	252
734	→	872
15	→	7
15	→	38
15	→	169
15	→	25
15	→	17
15	→	130
15	→	60
15	→	170
15	→	86
15	→	230
15	→	76
15	→	751
15	→	756
15	→	816
181	→	14
743	→	324
641	→	17
129	→	440
129	→	830
129	→	858
326	→	169
326	→	59
701	→	687
701	→	995
167	→	14
167	→	400
167	→	719
136	→	772
998	→	291
472	→	793
211	→	27
784	→	38
145	→	638
122	→	776
122	→	817
668	→	933
668	→	969
610	→	659
610	→	681
676	→	664
18	→	75
18	→	268
18	→	106
18	→	53
18	→	16
18	→	12
18	→	29
18	→	56
18	→	7
18	→	752
365	→	856
41	→	626
57	→	168
57	→	848
57	→	965
652	→	112
146	→	73
646	→	18
861	→	268
108	→	249
914	→	44
765	→	760
55	→	44
55	→	30
55	→	106
55	→	53
55	→	16
55	→	12
55	→	29
55	→	56
55	→	7
55	→	760
55	→	771
756	→	751
20	→	7
20	→	57
20	→	218
20	→	128
20	→	19
20	→	43
20	→	30
20	→	31
20	→	107
20	→	217
20	→	154
20	→	13
20	→	760
20	→	771
20	→	761
20	→	925
20	→	753
20	→	363
20	→	27
20	→	966
837	→	186
99	→	7
99	→	168
99	→	58
99	→	57
99	→	688
473	→	791
107	→	700
107	→	826
62	→	805
631	→	18
631	→	683
123	→	13
40	→	799
841	→	75
877	→	422
654	→	31
922	→	19
936	→	43
936	→	973
305	→	307
305	→	323
305	→	469
739	→	680
716	→	75
645	→	734
645	→	740
645	→	787
645	→	789
645	→	801
667	→	971
13	→	154
13	→	677
13	→	7
13	→	155
833	→	14
777	→	31
688	→	854
60	→	860
197	→	41
44	→	186
44	→	7
44	→	688
480	→	470
480	→	715
402	→	757
761	→	957
970	→	44
423	→	959
735	→	13
76	→	230
816	→	17
920	→	19
91	→	138
91	→	636
170	→	632
170	→	864
924	→	138
614	→	128
614	→	19
614	→	7
614	→	43
614	→	30
614	→	760
614	→	771
614	→	925
614	→	753
441	→	7
441	→	217
441	→	107
441	→	157
824	→	870
976	→	138
918	→	794
788	→	38
788	→	840
121	→	421
810	→	17
839	→	188
639	→	17
773	→	760
792	→	44
116	→	32
627	→	44
741	→	324
54	→	68
54	→	85
54	→	216
54	→	759
308	→	19
292	→	679
613	→	834
699	→	17
831	→	118
143	→	844
143	→	913
873	→	364
808	→	14
808	→	874
808	→	963
859	→	43
859	→	921
265	→	736
265	→	783
265	→	824
804	→	794
28	→	7
28	→	57
28	→	26
28	→	154
28	→	155
28	→	13
28	→	687
28	→	701
28	→	679
28	→	292
827	→	19
425	→	157
425	→	217
45	→	18
45	→	198
754	→	701
754	→	57
754	→	7
754	→	218
802	→	794
14	→	997
887	→	31
972	→	794
63	→	14
63	→	628
63	→	661
306	→	27
306	→	685
800	→	794
684	→	199
12	→	750
169	→	838
672	→	216
753	→	925
7	→	12
7	→	16
7	→	29
7	→	53
7	→	56
7	→	106
217	→	634
217	→	642
217	→	675
217	→	106
217	→	53
217	→	16
217	→	12
217	→	29
217	→	56
217	→	7
217	→	107
217	→	157
635	→	72
635	→	651
69	→	90
758	→	751
934	→	13
678	→	156
806	→	794
960	→	19
30	→	43
30	→	128
30	→	630
885	→	29
885	→	929
42	→	32
137	→	98
137	→	426
630	→	755
752	→	935
637	→	72
825	→	13
240	→	179
763	→	217
763	→	157
771	→	760
17	→	25
17	→	38
17	→	169
17	→	106
17	→	53
17	→	16
17	→	12
17	→	29
17	→	56
17	→	7
718	→	249
926	→	14
424	→	884
267	→	7
267	→	168
267	→	57
762	→	882
974	→	19
928	→	14
865	→	268
829	→	19
142	→	917
629	→	44
74	→	19
670	→	809
790	→	43
790	→	832
790	→	886
474	→	54
19	→	291
367	→	57
367	→	7
367	→	218
367	→	701
144	→	923
43	→	815
266	→	316
266	→	479
266	→	609
266	→	742
266	→	803
660	→	14
680	→	187
669	→	975
317	→	19
27	→	363
403	→	57
403	→	7
403	→	26
875	→	26
930	→	14
966	→	27
427	→	31
682	→	198
798	→	31
798	→	761
845	→	17
996	→	270
849	→	252
228	→	807
883	→	29
883	→	927
857	→	43
857	→	919
2₁(57)	→	58
2₁(260)	→	261
2₁(874)	→	875
2₁(226)	→	227
2₁(694)	→	695
2₁(721)	→	722
2₁(56)	→	57
2₁(700)	→	701
2₁(145)	→	146
2₁(200)	→	201
2₁(291)	→	292
2₁(208)	→	209
2₁(119)	→	120
2₁(231)	→	232
2₁(687)	→	688
2₁(218)	→	219
2₁(927)	→	928
2₁(160)	→	161
2₁(670)	→	671
2₁(696)	→	697
2₁(400)	→	401
2₁(274)	→	275
2₁(836)	→	837
2₁(929)	→	930
2₁(252)	→	253
2₁(834)	→	835
2₁(25)	→	26
2₁(206)	→	207
2₁(610)	→	611
2₁(731)	→	732
2₁(144)	→	145
2₁(122)	→	123
2₁(180)	→	181
2₁(87)	→	88
2₁(163)	→	164
2₁(301)	→	302
2₁(115)	→	116
2₁(686)	→	687
2₁(695)	→	696
2₁(283)	→	284
2₁(249)	→	250
2₁(273)	→	274
2₁(250)	→	251
2₁(268)	→	269
2₁(98)	→	99
2₁(925)	→	926
2₁(225)	→	226
2₁(261)	→	262
2₁(217)	→	218
2₁(669)	→	670
2₁(43)	→	44
2₁(272)	→	273
2₁(227)	→	228
0₂(971)	→	972
0₂(803)	→	804
0₂(917)	→	918
0₂(801)	→	802
0₂(793)	→	794
0₂(799)	→	800
0₂(805)	→	806
4₂(797)	→	798
4₂(761)	→	762
4₂(324)	→	325
4₂(737)	→	738
4₂(423)	→	424
5₂(772)	→	773
5₂(759)	→	760
5₂(422)	→	423
5₂(421)	→	422
5₂(796)	→	797
5₂(764)	→	765
5₂(424)	→	425
5₂(794)	→	795
5₂(762)	→	763
5₂(770)	→	771
5₂(760)	→	761
5₂(876)	→	877
3₁(282)	→	283
3₁(727)	→	728
3₁(757)	→	758
3₁(159)	→	160
3₁(870)	→	871
3₁(295)	→	296
3₁(204)	→	205
3₁(807)	→	808
3₁(58)	→	59
3₁(469)	→	470
3₁(363)	→	364
3₁(276)	→	277
3₁(178)	→	179
3₁(201)	→	202
3₁(78)	→	79
3₁(41)	→	42
3₁(129)	→	130
3₁(174)	→	175
3₁(275)	→	276
3₁(71)	→	72
3₁(175)	→	176
3₁(844)	→	845
3₁(14)	→	15
3₁(186)	→	187
3₁(169)	→	170
3₁(79)	→	80
3₁(168)	→	169
3₁(277)	→	278
3₁(257)	→	258
3₁(166)	→	167
3₁(72)	→	73
3₁(787)	→	788
3₁(85)	→	86
3₁(809)	→	810
3₁(755)	→	756
3₁(872)	→	873
3₁(473)	→	474
3₁(679)	→	680
3₁(297)	→	298
3₁(110)	→	111
3₁(479)	→	480
3₁(783)	→	784
3₁(636)	→	637
3₁(640)	→	641
3₁(209)	→	210
3₁(723)	→	724
3₁(233)	→	234
3₁(59)	→	60
3₁(817)	→	818
3₁(634)	→	635
3₁(190)	→	191
3₁(638)	→	639
3₁(293)	→	294
3₁(725)	→	726
3₁(815)	→	816
3₁(750)	→	751
3₁(75)	→	76
3₁(16)	→	17
3₁(933)	→	934
4₀(7)	→	7
5₀(7)	→	7
0₀(7)	→	7
1₁(170)	→	171
1₁(644)	→	645
1₁(191)	→	192
1₁(171)	→	172
1₁(135)	→	136
1₁(611)	→	612
1₁(177)	→	178
1₁(734)	→	735
1₁(824)	→	825
1₁(172)	→	173
1₁(61)	→	62
1₁(237)	→	238
1₁(263)	→	264
1₁(689)	→	690
1₁(117)	→	118
1₁(830)	→	831
1₁(44)	→	45
1₁(27)	→	28
1₁(304)	→	305
1₁(198)	→	199
1₁(196)	→	197
1₁(402)	→	403
1₁(284)	→	285
1₁(93)	→	94
1₁(234)	→	235
1₁(220)	→	221
1₁(316)	→	317
1₁(285)	→	286
1₁(651)	→	652
1₁(681)	→	682
1₁(139)	→	140
1₁(630)	→	631
1₁(307)	→	308
1₁(154)	→	155
1₁(189)	→	190
1₁(133)	→	134
1₁(664)	→	665
1₁(262)	→	263
1₁(77)	→	78
1₁(130)	→	131
1₁(259)	→	260
1₁(12)	→	13
1₁(111)	→	112
1₁(683)	→	684
0₁(224)	→	225
0₁(995)	→	996
0₁(472)	→	473
0₁(632)	→	633
0₁(919)	→	920
0₁(132)	→	133
0₁(236)	→	237
0₁(828)	→	829
0₁(677)	→	678
0₁(60)	→	61
0₁(305)	→	306
0₁(265)	→	266
0₁(266)	→	267
0₁(53)	→	54
0₁(155)	→	156
0₁(68)	→	69
0₁(205)	→	206
0₁(253)	→	254
0₁(94)	→	95
0₁(40)	→	41
0₁(120)	→	121
0₁(238)	→	239
0₁(661)	→	662
0₁(91)	→	92
0₁(140)	→	141
0₁(199)	→	200
0₁(667)	→	668
0₁(69)	→	70
0₁(269)	→	270
0₁(921)	→	922
0₁(165)	→	166
0₁(62)	→	63
0₁(645)	→	646
0₁(642)	→	643
0₁(38)	→	39
0₁(470)	→	471
0₁(279)	→	280
0₁(142)	→	143
0₁(693)	→	694
0₁(143)	→	144
0₁(255)	→	256
0₁(164)	→	165
0₁(108)	→	109
0₁(161)	→	162
0₁(134)	→	135
0₁(826)	→	827
0₁(688)	→	689
0₁(665)	→	666
0₁(158)	→	159
0₁(254)	→	255
0₁(219)	→	220
0₁(973)	→	974
0₁(668)	→	669
2₀(7)	→	7
1₀(7)	→	7
4₁(76)	→	77
4₁(832)	→	833
4₁(17)	→	18
4₁(131)	→	132
4₁(300)	→	301
4₁(858)	→	859
4₁(90)	→	91
4₁(364)	→	365
4₁(728)	→	729
4₁(692)	→	693
4₁(138)	→	139
4₁(730)	→	731
4₁(864)	→	865
4₁(216)	→	217
4₁(13)	→	14
4₁(128)	→	129
4₁(975)	→	976
4₁(856)	→	857
4₁(292)	→	293
4₁(957)	→	958
4₁(691)	→	692
4₁(31)	→	32
4₁(109)	→	110
4₁(471)	→	472
4₁(223)	→	224
4₁(719)	→	720
4₁(675)	→	676
4₁(662)	→	663
4₁(671)	→	672
4₁(366)	→	367
4₁(193)	→	194
4₁(70)	→	71
4₁(935)	→	936
4₁(923)	→	924
4₁(258)	→	259
4₁(107)	→	108
4₁(73)	→	74
4₁(294)	→	295
4₁(188)	→	189
4₁(203)	→	204
4₁(722)	→	723
4₁(659)	→	660
4₁(663)	→	664
4₁(860)	→	861
4₁(753)	→	754
4₁(401)	→	402
4₁(840)	→	841
4₁(613)	→	614
4₁(222)	→	223
4₁(270)	→	271
4₁(963)	→	964
4₁(19)	→	20
4₁(298)	→	299
4₁(156)	→	157
4₁(106)	→	107
4₁(39)	→	40
4₁(715)	→	716
4₁(195)	→	196
4₁(97)	→	98
4₁(724)	→	725
4₁(965)	→	966
4₁(751)	→	752
4₁(194)	→	195
4₁(685)	→	686
4₁(86)	→	87
4₁(96)	→	97
4₁(141)	→	142
4₁(26)	→	27
4₁(666)	→	667
4₁(717)	→	718
4₁(192)	→	193
4₁(959)	→	960
5₁(296)	→	297
5₁(235)	→	236
5₁(848)	→	849
5₁(232)	→	233
5₁(643)	→	644
5₁(207)	→	208
5₁(18)	→	19
5₁(92)	→	93
5₁(299)	→	300
5₁(271)	→	272
5₁(176)	→	177
5₁(187)	→	188
5₁(426)	→	427
5₁(653)	→	654
5₁(29)	→	30
5₁(913)	→	914
5₁(882)	→	883
5₁(88)	→	89
5₁(752)	→	753
5₁(791)	→	792
5₁(854)	→	855
5₁(264)	→	265
5₁(729)	→	730
5₁(228)	→	229
5₁(179)	→	180
5₁(612)	→	613
5₁(157)	→	158
5₁(112)	→	113
5₁(838)	→	839
5₁(121)	→	122
5₁(173)	→	174
5₁(114)	→	115
5₁(886)	→	887
5₁(278)	→	279
5₁(210)	→	211
5₁(118)	→	119
5₁(221)	→	222
5₁(697)	→	698
5₁(997)	→	998
5₁(30)	→	31
5₁(365)	→	366
5₁(609)	→	610
5₁(136)	→	137
5₁(969)	→	970
5₁(281)	→	282
5₁(256)	→	257
5₁(32)	→	33
5₁(726)	→	727
5₁(789)	→	790
5₁(302)	→	303
5₁(628)	→	629
5₁(626)	→	627
5₁(202)	→	203
5₁(230)	→	231
5₁(280)	→	281
5₁(698)	→	699
5₁(303)	→	304
5₁(776)	→	777
5₁(54)	→	55
5₁(95)	→	96
5₁(113)	→	114
5₁(440)	→	441
5₁(251)	→	252
5₁(884)	→	885
5₁(690)	→	691
5₁(239)	→	240
5₁(162)	→	163
5₁(720)	→	721
5₁(732)	→	733
1₂(740)	→	741
1₂(736)	→	737
1₂(742)	→	743
1₂(795)	→	796
1₂(323)	→	324
3₀(7)	→	7
3₂(738)	→	739
3₂(325)	→	326

The automaton is closed under rewriting as it is compatible.