Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/68989)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{7}

transitions:

730	→	284
730	→	57
730	→	7
730	→	216
730	→	74
730	→	15
854	→	182
33	→	7
33	→	232
33	→	102
33	→	82
33	→	182
33	→	21
33	→	31
33	→	41
33	→	94
33	→	75
33	→	32
33	→	185
33	→	217
33	→	284
33	→	57
33	→	216
33	→	74
33	→	15
33	→	498
33	→	517
33	→	854
33	→	156
33	→	834
33	→	780
33	→	772
33	→	103
23	→	217
23	→	103
846	→	172
650	→	324
917	→	898
29	→	779
29	→	853
29	→	1026
89	→	18
745	→	15
81	→	32
1117	→	22
152	→	16
214	→	48
214	→	496
286	→	707
880	→	63
15	→	57
15	→	74
15	→	284
15	→	516
15	→	805
181	→	32
915	→	898
743	→	15
886	→	29
886	→	987
1073	→	182
882	→	285
998	→	41
706	→	129
1097	→	15
784	→	74
784	→	869
784	→	883
878	→	63
610	→	648
610	→	705
18	→	326
18	→	433
18	→	677
18	→	922
1103	→	15
227	→	193
227	→	835
1141	→	1013
226	→	754
226	→	887
226	→	930
226	→	981
226	→	1044
41	→	63
41	→	947
184	→	797
1079	→	182
499	→	232
499	→	102
499	→	7
499	→	82
499	→	182
499	→	21
499	→	854
988	→	22
652	→	65
812	→	156
772	→	32
1011	→	41
980	→	971
411	→	232
411	→	102
411	→	7
411	→	82
411	→	182
411	→	21
411	→	854
411	→	156
411	→	834
331	→	284
331	→	57
331	→	153
331	→	29
331	→	14
331	→	20
331	→	40
331	→	7
331	→	74
331	→	15
331	→	105
331	→	749
331	→	806
331	→	898
331	→	917
774	→	30
931	→	898
110	→	32
1000	→	41
1071	→	182
1027	→	1013
891	→	1090
891	→	1096
891	→	1112
891	→	1128
1139	→	1013
325	→	7
325	→	155
696	→	685
1110	→	1134
1110	→	1140
1110	→	1146
749	→	15
892	→	105
892	→	805
892	→	284
892	→	57
892	→	7
892	→	15
892	→	806
193	→	742
193	→	760
193	→	785
193	→	928
20	→	857
99	→	851
99	→	879
62	→	23
31	→	142
31	→	7
31	→	234
31	→	1013
31	→	1027
49	→	7
49	→	201
49	→	34
49	→	30
49	→	233
49	→	47
49	→	858
1077	→	182
826	→	156
786	→	82
654	→	32
739	→	285
716	→	182
165	→	61
127	→	32
755	→	30
1112	→	1132
1112	→	1138
1112	→	1144
101	→	31
778	→	41
1111	→	30
44	→	18
884	→	285
1029	→	1013
609	→	736
761	→	30
751	→	15
612	→	744
612	→	762
612	→	787
612	→	920
735	→	16
330	→	750
330	→	773
330	→	799
330	→	914
1137	→	41
662	→	781
58	→	118
868	→	16
760	→	997
760	→	1028
760	→	1076
21	→	82
21	→	102
21	→	182
21	→	232
21	→	748
21	→	916
1127	→	82
844	→	88
894	→	15
788	→	82
171	→	653
810	→	143
773	→	995
773	→	1034
773	→	1078
921	→	898
1042	→	1136
1042	→	1142
741	→	310
741	→	825
982	→	971
1037	→	1013
22	→	153
22	→	29
22	→	14
22	→	20
22	→	40
22	→	7
22	→	827
75	→	94
1131	→	14
1047	→	82
613	→	30
613	→	153
613	→	29
613	→	14
613	→	20
613	→	40
613	→	7
613	→	308
613	→	886
613	→	858
283	→	17
665	→	656
665	→	734
143	→	811
923	→	898
301	→	22
301	→	809
808	→	57
180	→	683
876	→	63
244	→	16
258	→	48
843	→	1048
850	→	182
1035	→	1013
754	→	1001
754	→	1020
754	→	1070
1015	→	1110
1015	→	1114
1043	→	29
1043	→	1116
16	→	170
1059	→	118
704	→	118
1045	→	82
800	→	82
1125	→	1013
1145	→	182
1143	→	1013
708	→	173
834	→	156
100	→	783
753	→	30
1091	→	898
7	→	14
7	→	20
7	→	29
7	→	40
7	→	153
663	→	30
1021	→	1013
694	→	94
694	→	232
694	→	102
694	→	7
694	→	82
694	→	182
694	→	21
694	→	75
694	→	854
69	→	32
234	→	771
1085	→	898
1049	→	74
902	→	805
902	→	284
902	→	57
902	→	15
902	→	749
902	→	898
902	→	917
806	→	105
30	→	34
30	→	201
30	→	7
30	→	740
885	→	1122
885	→	1124
42	→	45
42	→	128
137	→	31
64	→	267
216	→	94
216	→	232
216	→	102
216	→	7
216	→	82
216	→	182
216	→	21
216	→	75
216	→	854
46	→	715
1133	→	41
752	→	1010
752	→	1012
752	→	1064
434	→	408
434	→	651
856	→	201
856	→	1042
35	→	22
948	→	805
948	→	284
948	→	57
948	→	857
948	→	779
948	→	40
948	→	20
948	→	14
948	→	29
948	→	153
948	→	7
948	→	74
948	→	516
948	→	15
828	→	155
763	→	30
83	→	719
48	→	608
48	→	717
48	→	1036
17	→	245
47	→	655
190	→	777
190	→	1038
718	→	182
1017	→	853
1017	→	29
1017	→	886
154	→	215
154	→	306
154	→	885
1129	→	82
870	→	16
762	→	999
762	→	1022
762	→	1072
324	→	664
517	→	498
858	→	201
974	→	156
974	→	834
285	→	833
848	→	182
782	→	74
782	→	867
782	→	881
649	→	847
649	→	875
1002	→	41
1113	→	30
24	→	7
24	→	284
24	→	57
24	→	74
24	→	15
24	→	232
24	→	102
24	→	82
24	→	182
24	→	21
24	→	94
24	→	75
24	→	854
19	→	7
19	→	284
19	→	57
19	→	74
19	→	15
19	→	30
19	→	308
19	→	306
19	→	22
19	→	215
19	→	154
19	→	105
19	→	749
19	→	806
19	→	886
19	→	858
19	→	898
19	→	917
19	→	948
852	→	182
1016	→	1084
1016	→	1102
1016	→	1126
1016	→	1130
611	→	752
611	→	893
611	→	897
611	→	970
611	→	1046
43	→	407
43	→	979
1065	→	182
660	→	807
194	→	31
888	→	1058
929	→	898
682	→	79
1023	→	1013
798	→	84
737	→	267
1123	→	41
155	→	845
996	→	41
1147	→	182
192	→	855
780	→	41
656	→	738
661	→	849
661	→	877
327	→	695
327	→	703
1039	→	1013
1135	→	41
1115	→	971
2₁(57)	→	58
2₁(1042)	→	1043
2₁(99)	→	100
2₁(721)	→	722
2₁(187)	→	188
2₁(145)	→	146
2₁(46)	→	47
2₁(1058)	→	1059
2₁(277)	→	278
2₁(703)	→	704
2₁(190)	→	191
2₁(689)	→	690
2₁(687)	→	688
2₁(255)	→	256
2₁(1110)	→	1111
2₁(286)	→	287
2₁(290)	→	291
2₁(238)	→	239
2₁(60)	→	61
2₁(885)	→	886
2₁(223)	→	224
2₁(79)	→	80
2₁(282)	→	283
2₁(248)	→	249
2₁(407)	→	408
2₁(63)	→	64
2₁(212)	→	213
2₁(752)	→	753
2₁(292)	→	293
2₁(107)	→	108
2₁(275)	→	276
2₁(857)	→	858
2₁(649)	→	650
2₁(59)	→	60
2₁(134)	→	135
2₁(120)	→	121
2₁(86)	→	87
2₁(308)	→	309
2₁(232)	→	233
2₁(144)	→	145
2₁(754)	→	755
2₁(1112)	→	1113
2₁(96)	→	97
2₁(188)	→	189
2₁(690)	→	691
2₁(213)	→	214
2₁(64)	→	65
2₁(762)	→	763
2₁(94)	→	95
2₁(299)	→	300
2₁(661)	→	662
2₁(29)	→	30
2₁(58)	→	59
2₁(320)	→	321
2₁(296)	→	297
2₁(760)	→	761
2₁(241)	→	242
2₁(307)	→	308
2₁(736)	→	737
2₁(723)	→	724
2₁(773)	→	774
2₁(98)	→	99
2₁(269)	→	270
2₁(855)	→	856
2₁(294)	→	295
2₁(685)	→	686
2₁(109)	→	110
2₁(121)	→	122
2₁(651)	→	652
2₁(254)	→	255
2₁(237)	→	238
2₁(221)	→	222
2₁(278)	→	279
2₁(48)	→	49
2₁(433)	→	434
2₂(979)	→	980
2₂(1114)	→	1115
2₂(970)	→	971
2₂(981)	→	982
1₂(1016)	→	1017
1₂(899)	→	900
1₂(898)	→	899
1₂(901)	→	902
1₂(1015)	→	1016
5₂(1020)	→	1021
5₂(973)	→	974
5₂(1028)	→	1029
5₂(1140)	→	1141
5₂(1034)	→	1035
5₂(1038)	→	1039
5₂(1026)	→	1027
5₂(1138)	→	1139
5₂(1014)	→	1015
5₂(1124)	→	1125
5₂(1142)	→	1143
5₂(1036)	→	1037
5₂(1012)	→	1013
5₂(1022)	→	1023
5₂(971)	→	972
1₁(727)	→	728
1₁(1130)	→	1131
1₁(330)	→	331
1₁(867)	→	868
1₁(21)	→	22
1₁(204)	→	205
1₁(842)	→	843
1₁(660)	→	661
1₁(734)	→	735
1₁(327)	→	328
1₁(211)	→	212
1₁(178)	→	179
1₁(201)	→	202
1₁(78)	→	79
1₁(161)	→	162
1₁(841)	→	842
1₁(246)	→	247
1₁(207)	→	208
1₁(726)	→	727
1₁(612)	→	613
1₁(250)	→	251
1₁(273)	→	274
1₁(270)	→	271
1₁(889)	→	890
1₁(888)	→	889
1₁(240)	→	241
1₁(18)	→	19
1₁(686)	→	687
1₁(153)	→	154
1₁(869)	→	870
1₁(176)	→	177
1₁(43)	→	44
1₁(66)	→	67
1₁(193)	→	194
1₁(891)	→	892
1₁(611)	→	612
1₁(274)	→	275
1₁(658)	→	659
1₁(177)	→	178
1₁(130)	→	131
1₁(679)	→	680
1₁(95)	→	96
1₁(76)	→	77
1₁(843)	→	844
1₁(15)	→	16
1₁(189)	→	190
1₁(328)	→	329
1₁(180)	→	181
1₁(306)	→	307
1₁(226)	→	227
1₁(83)	→	84
1₁(61)	→	62
1₁(797)	→	798
1₁(288)	→	289
1₁(16)	→	17
4₀(7)	→	7
5₀(7)	→	7
0₂(922)	→	923
0₂(1084)	→	1085
0₂(930)	→	931
0₂(916)	→	917
0₂(928)	→	929
0₂(897)	→	898
0₂(1090)	→	1091
0₂(920)	→	921
0₂(914)	→	915
0₂(900)	→	901
3₀(7)	→	7
3₁(170)	→	171
3₁(87)	→	88
3₁(827)	→	828
3₁(108)	→	109
3₁(143)	→	144
3₁(100)	→	101
3₁(171)	→	172
3₁(218)	→	219
3₁(160)	→	161
3₁(47)	→	48
3₁(142)	→	143
3₁(97)	→	98
3₁(82)	→	83
3₁(740)	→	741
3₁(881)	→	882
3₁(164)	→	165
3₁(151)	→	152
3₁(203)	→	204
3₁(837)	→	838
3₁(172)	→	173
3₁(146)	→	147
3₁(157)	→	158
3₁(128)	→	129
3₁(657)	→	658
3₁(738)	→	739
3₁(284)	→	285
3₁(239)	→	240
3₁(148)	→	149
3₁(220)	→	221
3₁(41)	→	42
3₁(147)	→	148
3₁(67)	→	68
3₁(285)	→	286
3₁(688)	→	689
3₁(235)	→	236
3₁(249)	→	250
3₁(314)	→	315
3₁(840)	→	841
3₁(154)	→	155
3₁(80)	→	81
3₁(678)	→	679
3₁(835)	→	836
3₁(311)	→	312
3₁(219)	→	220
3₁(707)	→	708
3₁(173)	→	174
3₁(175)	→	176
3₁(185)	→	186
3₁(809)	→	810
3₁(183)	→	184
3₁(131)	→	132
3₁(691)	→	692
3₁(662)	→	663
3₁(836)	→	837
3₁(883)	→	884
3₁(205)	→	206
3₁(268)	→	269
3₁(609)	→	610
3₁(75)	→	76
3₁(705)	→	706
3₁(719)	→	720
3₁(720)	→	721
3₁(845)	→	846
3₁(324)	→	325
3₁(838)	→	839
3₁(309)	→	310
4₁(31)	→	32
4₁(695)	→	696
4₁(692)	→	693
4₁(677)	→	678
4₁(1072)	→	1073
4₁(1064)	→	1065
4₁(717)	→	718
4₁(851)	→	852
4₁(1046)	→	1047
4₁(20)	→	21
4₁(849)	→	850
4₁(1128)	→	1129
4₁(312)	→	313
4₁(155)	→	156
4₁(247)	→	248
4₁(1126)	→	1127
4₁(681)	→	682
4₁(1044)	→	1045
4₁(799)	→	800
4₁(728)	→	729
4₁(118)	→	119
4₁(771)	→	772
4₁(853)	→	854
4₁(684)	→	685
4₁(295)	→	296
4₁(1078)	→	1079
4₁(251)	→	252
4₁(811)	→	812
4₁(648)	→	649
4₁(1146)	→	1147
4₁(1070)	→	1071
4₁(833)	→	834
4₁(119)	→	120
4₁(192)	→	193
4₁(182)	→	183
4₁(85)	→	86
4₁(847)	→	848
4₁(74)	→	75
4₁(656)	→	657
4₁(245)	→	246
4₁(281)	→	282
4₁(1144)	→	1145
4₁(715)	→	716
4₁(45)	→	46
4₁(319)	→	320
4₁(210)	→	211
4₁(1076)	→	1077
4₁(276)	→	277
4₁(825)	→	826
4₁(785)	→	786
4₁(323)	→	324
4₁(272)	→	273
4₁(787)	→	788
4₁(315)	→	316
4₁(409)	→	410
4₁(150)	→	151
4₁(159)	→	160
1₀(7)	→	7
2₀(7)	→	7
5₁(186)	→	187
5₁(999)	→	1000
5₁(179)	→	180
5₁(1122)	→	1123
5₁(497)	→	498
5₁(300)	→	301
5₁(40)	→	41
5₁(1134)	→	1135
5₁(256)	→	257
5₁(22)	→	23
5₁(610)	→	611
5₁(279)	→	280
5₁(779)	→	780
5₁(408)	→	409
5₁(879)	→	880
5₁(216)	→	217
5₁(1010)	→	1011
5₁(184)	→	185
5₁(729)	→	730
5₁(410)	→	411
5₁(313)	→	314
5₁(88)	→	89
5₁(1001)	→	1002
5₁(133)	→	134
5₁(102)	→	103
5₁(126)	→	127
5₁(32)	→	33
5₁(680)	→	681
5₁(318)	→	319
5₁(280)	→	281
5₁(84)	→	85
5₁(997)	→	998
5₁(297)	→	298
5₁(135)	→	136
5₁(124)	→	125
5₁(202)	→	203
5₁(252)	→	253
5₁(209)	→	210
5₁(132)	→	133
5₁(30)	→	31
5₁(149)	→	150
5₁(1132)	→	1133
5₁(516)	→	517
5₁(224)	→	225
5₁(125)	→	126
5₁(875)	→	876
5₁(156)	→	157
5₁(123)	→	124
5₁(106)	→	107
5₁(777)	→	778
5₁(233)	→	234
5₁(877)	→	878
5₁(724)	→	725
5₁(995)	→	996
5₁(287)	→	288
5₁(163)	→	164
5₁(1136)	→	1137
5₁(291)	→	292
5₁(42)	→	43
5₁(693)	→	694
5₁(293)	→	294
5₁(608)	→	609
0₁(267)	→	268
0₁(65)	→	66
0₁(129)	→	130
0₁(890)	→	891
0₁(1048)	→	1049
0₁(329)	→	330
0₁(1116)	→	1117
0₁(271)	→	272
0₁(326)	→	327
0₁(653)	→	654
0₁(103)	→	104
0₁(17)	→	18
0₁(215)	→	216
0₁(105)	→	106
0₁(683)	→	684
0₁(321)	→	322
0₁(498)	→	499
0₁(781)	→	782
0₁(191)	→	192
0₁(807)	→	808
0₁(23)	→	24
0₁(236)	→	237
0₁(783)	→	784
0₁(947)	→	948
0₁(664)	→	665
0₁(217)	→	218
0₁(222)	→	223
0₁(122)	→	123
0₁(748)	→	749
0₁(722)	→	723
0₁(750)	→	751
0₁(1096)	→	1097
0₁(322)	→	323
0₁(208)	→	209
0₁(289)	→	290
0₁(225)	→	226
0₁(887)	→	888
0₁(14)	→	15
0₁(316)	→	317
0₁(1102)	→	1103
0₁(987)	→	988
0₁(243)	→	244
0₁(68)	→	69
0₁(77)	→	78
0₁(158)	→	159
0₁(742)	→	743
0₁(136)	→	137
0₁(310)	→	311
0₁(893)	→	894
0₁(34)	→	35
0₁(104)	→	105
0₁(257)	→	258
0₁(655)	→	656
0₁(805)	→	806
0₁(317)	→	318
0₁(174)	→	175
0₁(298)	→	299
0₁(496)	→	497
0₁(659)	→	660
0₁(744)	→	745
0₁(234)	→	235
0₁(242)	→	243
0₁(725)	→	726
0₁(253)	→	254
0₁(206)	→	207
0₁(162)	→	163
0₁(839)	→	840
4₂(972)	→	973
0₀(7)	→	7
3₂(1013)	→	1014

The automaton is closed under rewriting as it is compatible.