Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96417)

The rewrite relation of the following TRS is considered.

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

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

854	→	18
279	→	54
329	→	778
329	→	791
25	→	855
25	→	857
457	→	926
457	→	992
61	→	392
61	→	419
61	→	436
61	→	602
61	→	780
61	→	807
32	→	265
32	→	332
32	→	252
32	→	7
128	→	825
128	→	849
263	→	866
81	→	100
87	→	25
15	→	56
15	→	211
15	→	251
781	→	148
886	→	869
374	→	54
933	→	162
882	→	930
882	→	932
995	→	162
149	→	988
927	→	80
226	→	86
41	→	412
41	→	909
955	→	162
50	→	180
50	→	315
57	→	454
691	→	61
838	→	21
838	→	72
838	→	36
838	→	20
838	→	14
838	→	31
838	→	48
838	→	7
838	→	17
838	→	727
838	→	54
838	→	374
805	→	917
347	→	85
108	→	772
729	→	770
914	→	80
331	→	7
331	→	296
331	→	24
331	→	162
331	→	37
931	→	148
37	→	162
37	→	296
37	→	72
37	→	36
37	→	20
37	→	14
37	→	31
37	→	48
37	→	7
110	→	18
598	→	885
456	→	905
456	→	907
55	→	7
55	→	37
55	→	57
55	→	332
55	→	252
55	→	265
55	→	32
55	→	21
55	→	17
55	→	93
55	→	727
55	→	54
55	→	374
55	→	182
55	→	824
55	→	300
175	→	54
837	→	913
99	→	25
397	→	59
62	→	7
62	→	73
62	→	212
49	→	80
49	→	193
49	→	373
601	→	25
601	→	911
601	→	928
965	→	265
777	→	129
416	→	994
884	→	296
884	→	24
884	→	72
884	→	36
884	→	20
884	→	14
884	→	31
884	→	48
884	→	7
884	→	162
884	→	37
73	→	127
73	→	148
769	→	93
26	→	7
26	→	15
26	→	131
26	→	148
26	→	297
26	→	127
26	→	73
26	→	21
26	→	38
26	→	182
26	→	824
735	→	962
735	→	970
330	→	851
993	→	18
253	→	690
79	→	18
36	→	915
161	→	78
916	→	80
21	→	823
912	→	16
824	→	182
918	→	80
779	→	148
726	→	76
773	→	80
116	→	358
54	→	727
52	→	776
900	→	18
264	→	174
82	→	115
906	→	21
808	→	792
850	→	214
16	→	768
16	→	864
971	→	265
989	→	299
140	→	25
736	→	148
736	→	297
736	→	72
736	→	36
736	→	20
736	→	14
736	→	31
736	→	48
736	→	7
736	→	127
736	→	73
7	→	14
7	→	20
7	→	31
7	→	36
7	→	48
7	→	72
295	→	53
417	→	960
417	→	964
126	→	18
806	→	332
806	→	252
806	→	72
806	→	36
806	→	20
806	→	14
806	→	31
806	→	48
806	→	7
806	→	265
806	→	32
806	→	300
42	→	774
42	→	899
957	→	162
856	→	18
310	→	98
310	→	847
35	→	18
278	→	596
458	→	51
458	→	251
458	→	56
458	→	72
458	→	36
458	→	20
458	→	14
458	→	31
458	→	48
458	→	7
458	→	211
458	→	15
458	→	33
240	→	139
908	→	437
771	→	101
17	→	725
206	→	174
858	→	265
865	→	285
74	→	92
74	→	284
848	→	212
775	→	80
24	→	954
19	→	7
19	→	332
19	→	252
19	→	59
19	→	265
19	→	32
19	→	333
19	→	21
19	→	296
19	→	163
19	→	162
19	→	37
19	→	727
19	→	54
19	→	374
852	→	162
910	→	437
43	→	7
43	→	51
43	→	251
43	→	56
43	→	211
43	→	15
43	→	33
418	→	15
418	→	7
372	→	17
961	→	18
603	→	597
442	→	131
929	→	128
163	→	227
191	→	853
192	→	18
883	→	956
963	→	18
420	→	413
3₁(871)	→	872
3₁(727)	→	728
3₁(911)	→	912
3₁(186)	→	187
3₁(137)	→	138
3₁(117)	→	118
3₁(15)	→	16
3₁(82)	→	83
3₁(234)	→	235
3₁(104)	→	105
3₁(883)	→	884
3₁(265)	→	266
3₁(832)	→	833
3₁(602)	→	603
3₁(362)	→	363
3₁(728)	→	729
3₁(22)	→	23
3₁(228)	→	229
3₁(872)	→	873
3₁(885)	→	886
3₁(73)	→	74
3₁(725)	→	726
3₁(913)	→	914
3₁(102)	→	103
3₁(730)	→	731
3₁(136)	→	137
3₁(772)	→	773
3₁(319)	→	320
3₁(219)	→	220
3₁(596)	→	597
3₁(275)	→	276
3₁(252)	→	253
3₁(315)	→	316
3₁(59)	→	60
3₁(129)	→	130
3₁(915)	→	916
3₁(134)	→	135
3₁(318)	→	319
3₁(80)	→	81
3₁(232)	→	233
3₁(172)	→	173
3₁(93)	→	94
3₁(365)	→	366
3₁(24)	→	25
3₁(213)	→	214
3₁(138)	→	139
3₁(216)	→	217
3₁(266)	→	267
3₁(849)	→	850
3₁(774)	→	775
3₁(866)	→	867
3₁(868)	→	869
3₁(330)	→	331
3₁(926)	→	927
3₁(414)	→	415
3₁(416)	→	417
3₁(97)	→	98
3₁(917)	→	918
3₁(201)	→	202
3₁(346)	→	347
3₁(257)	→	258
3₁(294)	→	295
3₁(253)	→	254
3₁(368)	→	369
3₁(132)	→	133
3₁(229)	→	230
3₁(109)	→	110
3₁(202)	→	203
3₁(413)	→	414
3₁(287)	→	288
3₁(21)	→	22
3₁(227)	→	228
3₁(802)	→	803
3₁(237)	→	238
3₁(48)	→	49
3₁(75)	→	76
3₁(831)	→	832
0₂(392)	→	393
3₂(393)	→	394
3₂(438)	→	439
3₂(437)	→	438
3₂(440)	→	441
4₂(441)	→	442
4₂(394)	→	395
4₂(907)	→	908
4₂(909)	→	910
4₂(436)	→	437
0₁(103)	→	104
0₁(222)	→	223
0₁(148)	→	149
0₁(101)	→	102
0₁(195)	→	196
0₁(263)	→	264
0₁(828)	→	829
0₁(988)	→	989
0₁(78)	→	79
0₁(960)	→	961
0₁(41)	→	42
0₁(309)	→	310
0₁(770)	→	771
0₁(853)	→	854
0₁(230)	→	231
0₁(598)	→	599
0₁(14)	→	15
0₁(50)	→	51
0₁(291)	→	292
0₁(284)	→	285
0₁(798)	→	799
0₁(825)	→	826
0₁(37)	→	38
0₁(151)	→	152
0₁(32)	→	33
0₁(168)	→	169
0₁(881)	→	882
0₁(341)	→	342
0₁(224)	→	225
0₁(333)	→	334
0₁(342)	→	343
0₁(286)	→	287
0₁(119)	→	120
0₁(77)	→	78
0₁(198)	→	199
0₁(305)	→	306
0₁(456)	→	457
0₁(96)	→	97
0₁(123)	→	124
0₁(130)	→	131
0₁(98)	→	99
0₁(297)	→	298
0₁(873)	→	874
0₁(118)	→	119
0₁(298)	→	299
0₁(57)	→	58
0₁(329)	→	330
0₁(328)	→	329
0₁(361)	→	362
0₁(306)	→	307
0₁(344)	→	345
0₁(320)	→	321
0₁(61)	→	62
0₁(190)	→	191
0₁(293)	→	294
0₁(156)	→	157
0₁(855)	→	856
0₁(962)	→	963
0₁(882)	→	883
0₁(864)	→	865
0₁(278)	→	279
0₁(120)	→	121
0₁(100)	→	101
3₀(7)	→	7
5₀(7)	→	7
4₀(7)	→	7
2₁(690)	→	691
2₁(125)	→	126
2₁(299)	→	300
2₁(970)	→	971
2₁(106)	→	107
2₁(171)	→	172
2₁(364)	→	365
2₁(340)	→	341
2₁(796)	→	797
2₁(336)	→	337
2₁(58)	→	59
2₁(203)	→	204
2₁(734)	→	735
2₁(86)	→	87
2₁(335)	→	336
2₁(829)	→	830
2₁(833)	→	834
2₁(370)	→	371
2₁(597)	→	598
2₁(857)	→	858
2₁(60)	→	61
2₁(867)	→	868
2₁(236)	→	237
2₁(84)	→	85
2₁(184)	→	185
2₁(270)	→	271
2₁(339)	→	340
2₁(220)	→	221
2₁(899)	→	900
2₁(166)	→	167
2₁(107)	→	108
2₁(964)	→	965
2₁(235)	→	236
2₁(149)	→	150
2₁(49)	→	50
2₁(251)	→	252
2₁(159)	→	160
2₁(267)	→	268
2₁(289)	→	290
2₁(729)	→	730
2₁(189)	→	190
2₁(321)	→	322
2₁(31)	→	32
2₁(158)	→	159
2₁(81)	→	82
2₁(877)	→	878
2₁(292)	→	293
2₁(345)	→	346
2₁(18)	→	19
2₁(131)	→	132
2₁(874)	→	875
2₁(332)	→	333
2₁(199)	→	200
2₁(233)	→	234
2₁(732)	→	733
2₁(187)	→	188
2₁(992)	→	993
2₁(272)	→	273
2₁(258)	→	259
2₁(324)	→	325
2₁(801)	→	802
1₁(807)	→	808
1₁(262)	→	263
1₁(805)	→	806
1₁(454)	→	455
1₁(869)	→	870
1₁(290)	→	291
1₁(366)	→	367
1₁(836)	→	837
1₁(851)	→	852
1₁(827)	→	828
1₁(880)	→	881
1₁(185)	→	186
1₁(197)	→	198
1₁(155)	→	156
1₁(128)	→	129
1₁(152)	→	153
1₁(799)	→	800
1₁(994)	→	995
1₁(169)	→	170
1₁(792)	→	793
1₁(92)	→	93
1₁(54)	→	55
1₁(800)	→	801
1₁(238)	→	239
1₁(260)	→	261
1₁(803)	→	804
1₁(804)	→	805
1₁(173)	→	174
1₁(217)	→	218
1₁(183)	→	184
1₁(23)	→	24
1₁(133)	→	134
1₁(879)	→	880
1₁(776)	→	777
1₁(214)	→	215
1₁(165)	→	166
1₁(308)	→	309
1₁(38)	→	39
1₁(182)	→	183
1₁(793)	→	794
1₁(768)	→	769
1₁(256)	→	257
1₁(162)	→	163
1₁(956)	→	957
1₁(218)	→	219
1₁(174)	→	175
1₁(163)	→	164
1₁(36)	→	37
1₁(795)	→	796
1₁(316)	→	317
1₁(954)	→	955
1₁(170)	→	171
1₁(271)	→	272
1₁(304)	→	305
1₁(932)	→	933
1₁(124)	→	125
1₁(326)	→	327
1₁(56)	→	57
1₁(276)	→	277
1₁(259)	→	260
1₁(33)	→	34
1₁(285)	→	286
1₁(327)	→	328
1₁(17)	→	18
1₁(39)	→	40
1₁(791)	→	792
1₁(301)	→	302
1₁(160)	→	161
1₁(837)	→	838
1₁(415)	→	416
0₀(7)	→	7
1₀(7)	→	7
4₁(835)	→	836
4₁(164)	→	165
4₁(225)	→	226
4₁(302)	→	303
4₁(40)	→	41
4₁(823)	→	824
4₁(277)	→	278
4₁(20)	→	21
4₁(105)	→	106
4₁(373)	→	374
4₁(254)	→	255
4₁(180)	→	181
4₁(154)	→	155
4₁(153)	→	154
4₁(223)	→	224
4₁(360)	→	361
4₁(367)	→	368
4₁(878)	→	879
4₁(205)	→	206
4₁(325)	→	326
4₁(288)	→	289
4₁(181)	→	182
4₁(735)	→	736
4₁(343)	→	344
4₁(139)	→	140
4₁(188)	→	189
4₁(135)	→	136
4₁(215)	→	216
4₁(794)	→	795
4₁(191)	→	192
4₁(323)	→	324
4₁(74)	→	75
4₁(150)	→	151
4₁(273)	→	274
4₁(53)	→	54
4₁(269)	→	270
4₁(16)	→	17
4₁(157)	→	158
4₁(122)	→	123
4₁(417)	→	418
4₁(455)	→	456
4₁(95)	→	96
4₁(255)	→	256
4₁(334)	→	335
4₁(231)	→	232
4₁(25)	→	26
4₁(419)	→	420
4₁(905)	→	906
4₁(116)	→	117
4₁(876)	→	877
4₁(412)	→	413
4₁(307)	→	308
5₁(296)	→	297
5₁(359)	→	360
5₁(337)	→	338
5₁(212)	→	213
5₁(72)	→	73
5₁(194)	→	195
5₁(930)	→	931
5₁(268)	→	269
5₁(261)	→	262
5₁(211)	→	212
5₁(204)	→	205
5₁(778)	→	779
5₁(600)	→	601
5₁(780)	→	781
5₁(371)	→	372
5₁(115)	→	116
5₁(358)	→	359
5₁(830)	→	831
5₁(834)	→	835
5₁(875)	→	876
5₁(363)	→	364
5₁(731)	→	732
5₁(300)	→	301
5₁(196)	→	197
5₁(322)	→	323
5₁(274)	→	275
5₁(51)	→	52
5₁(847)	→	848
5₁(42)	→	43
5₁(870)	→	871
5₁(599)	→	600
5₁(193)	→	194
5₁(85)	→	86
5₁(121)	→	122
5₁(76)	→	77
5₁(733)	→	734
5₁(221)	→	222
5₁(167)	→	168
5₁(457)	→	458
5₁(94)	→	95
5₁(34)	→	35
5₁(928)	→	929
5₁(797)	→	798
5₁(127)	→	128
5₁(317)	→	318
5₁(826)	→	827
5₁(200)	→	201
5₁(369)	→	370
5₁(83)	→	84
5₁(303)	→	304
5₁(338)	→	339
5₁(108)	→	109
5₁(239)	→	240
5₁(52)	→	53
2₂(396)	→	397
2₀(7)	→	7
1₂(439)	→	440
1₂(395)	→	396

The automaton is closed under rewriting as it is compatible.