Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96065)

The rewrite relation of the following TRS is considered.

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

final states:

{7}

transitions:

503	→	866
157	→	46
157	→	502
157	→	807
239	→	761
871	→	17
176	→	886
176	→	920
869	→	507
102	→	69
917	→	25
1056	→	88
860	→	126
87	→	327
80	→	14
658	→	72
15	→	7
15	→	72
15	→	177
15	→	242
15	→	272
15	→	135
15	→	134
15	→	118
15	→	88
15	→	939
915	→	25
915	→	985
915	→	993
743	→	98
326	→	304
1140	→	1144
1008	→	25
511	→	503
511	→	1096
1097	→	330
1107	→	30
119	→	944
784	→	30
145	→	19
260	→	69
1103	→	25
978	→	209
1141	→	52
41	→	417
939	→	88
988	→	29
652	→	176
652	→	979
980	→	52
1062	→	91
108	→	166
919	→	25
919	→	987
919	→	995
931	→	72
147	→	196
34	→	19
598	→	155
1139	→	16
175	→	115
947	→	166
756	→	118
1095	→	25
20	→	7
20	→	13
20	→	96
20	→	110
20	→	288
20	→	107
20	→	17
20	→	61
20	→	14
20	→	917
20	→	973
20	→	62
20	→	925
473	→	12
473	→	742
467	→	52
304	→	870
304	→	876
31	→	146
380	→	27
380	→	472
380	→	981
968	→	30
1105	→	30
40	→	208
786	→	30
1010	→	30
287	→	206
287	→	803
877	→	449
1040	→	25
936	→	1013
936	→	1037
71	→	880
71	→	916
305	→	936
305	→	942
305	→	971
127	→	14
127	→	288
127	→	107
127	→	17
13	→	25
13	→	95
13	→	241
13	→	7
13	→	273
222	→	19
101	→	421
101	→	448
778	→	272
778	→	7
778	→	134
778	→	118
777	→	934
777	→	940
777	→	969
1052	→	72
505	→	1136
428	→	68
428	→	977
44	→	1041
970	→	30
842	→	328
26	→	48
26	→	7
26	→	887
1137	→	25
881	→	30
1070	→	14
343	→	872
343	→	983
86	→	311
86	→	841
86	→	938
79	→	596
79	→	884
1099	→	93
868	→	1132
868	→	1138
994	→	93
177	→	117
177	→	71
177	→	16
177	→	12
177	→	29
177	→	85
177	→	7
177	→	72
72	→	117
72	→	71
72	→	16
72	→	12
72	→	29
72	→	85
72	→	7
509	→	86
509	→	7
509	→	289
824	→	272
824	→	135
824	→	117
824	→	71
824	→	16
824	→	12
824	→	29
824	→	85
824	→	7
824	→	134
824	→	118
207	→	52
976	→	209
911	→	289
949	→	14
1053	→	1106
1053	→	1130
116	→	46
116	→	805
921	→	25
1051	→	1104
1051	→	1128
1042	→	25
986	→	29
823	→	882
823	→	918
823	→	991
982	→	242
799	→	1069
1092	→	1102
1131	→	25
1101	→	25
67	→	1059
657	→	878
657	→	914
923	→	25
53	→	7
53	→	176
53	→	39
53	→	30
53	→	788
53	→	881
53	→	887
873	→	17
1014	→	30
808	→	289
1060	→	88
937	→	72
979	→	1007
941	→	118
804	→	242
28	→	7
28	→	61
28	→	288
28	→	107
28	→	17
28	→	14
118	→	134
118	→	272
118	→	843
344	→	13
1018	→	25
419	→	1039
419	→	1090
45	→	783
45	→	930
45	→	1092
802	→	17
802	→	117
802	→	71
802	→	16
802	→	12
802	→	29
802	→	85
802	→	7
802	→	119
508	→	874
66	→	657
114	→	496
114	→	888
14	→	61
14	→	7
887	→	30
1094	→	1100
972	→	30
306	→	14
800	→	948
1012	→	30
925	→	62
925	→	973
1145	→	25
497	→	30
1143	→	242
77	→	975
1091	→	16
1044	→	25
1020	→	25
1020	→	1094
1020	→	1098
1020	→	1142
7	→	12
7	→	16
7	→	29
7	→	71
7	→	85
7	→	117
506	→	1134
991	→	1051
69	→	643
69	→	755
69	→	785
934	→	1011
934	→	1019
126	→	946
806	→	273
30	→	39
30	→	176
30	→	809
1038	→	25
885	→	30
46	→	427
1133	→	25
240	→	52
893	→	451
990	→	329
905	→	999
47	→	7
47	→	86
47	→	289
47	→	272
47	→	134
47	→	118
47	→	176
47	→	39
47	→	30
47	→	810
47	→	845
47	→	881
47	→	330
47	→	1097
17	→	107
17	→	288
17	→	510
17	→	787
17	→	924
945	→	137
651	→	922
1129	→	25
68	→	989
206	→	466
974	→	210
1054	→	72
1093	→	52
74	→	227
74	→	1061
378	→	33
422	→	68
1002	→	909
451	→	1049
452	→	273
452	→	95
452	→	7
452	→	25
452	→	241
452	→	13
452	→	917
943	→	118
935	→	72
1050	→	13
43	→	1043
507	→	967
507	→	1053
507	→	1140
27	→	379
70	→	7
70	→	311
70	→	86
70	→	272
70	→	134
70	→	118
70	→	274
875	→	17
930	→	1009
930	→	1017
984	→	289
992	→	67
992	→	1055
155	→	902
996	→	93
94	→	46
312	→	361
191	→	69
1135	→	25
879	→	30
883	→	30
420	→	45
2₁(247)	→	248
2₁(1092)	→	1093
2₁(156)	→	157
2₁(874)	→	875
2₁(1094)	→	1095
2₁(323)	→	324
2₁(187)	→	188
2₁(339)	→	340
2₁(644)	→	645
2₁(234)	→	235
2₁(371)	→	372
2₁(196)	→	197
2₁(208)	→	209
2₁(277)	→	278
2₁(820)	→	821
2₁(27)	→	28
2₁(88)	→	89
2₁(819)	→	820
2₁(815)	→	816
2₁(324)	→	325
2₁(327)	→	328
2₁(316)	→	317
2₁(246)	→	247
2₁(49)	→	50
2₁(872)	→	873
2₁(987)	→	988
2₁(274)	→	275
2₁(421)	→	422
2₁(166)	→	167
2₁(61)	→	62
2₁(325)	→	326
2₁(289)	→	290
2₁(76)	→	77
2₁(168)	→	169
2₁(219)	→	220
2₁(985)	→	986
2₁(369)	→	370
2₁(342)	→	343
2₁(252)	→	253
2₁(315)	→	316
2₁(67)	→	68
2₁(206)	→	207
2₁(318)	→	319
2₁(16)	→	17
2₁(841)	→	842
2₁(118)	→	119
2₁(850)	→	851
2₁(285)	→	286
2₁(122)	→	123
2₁(150)	→	151
2₁(795)	→	796
2₁(812)	→	813
2₁(113)	→	114
2₁(312)	→	313
2₁(810)	→	811
2₁(979)	→	980
2₁(1140)	→	1141
2₁(173)	→	174
2₁(216)	→	217
2₁(427)	→	428
2₁(764)	→	765
2₁(852)	→	853
2₁(503)	→	504
2₁(320)	→	321
2₁(768)	→	769
2₁(818)	→	819
2₁(336)	→	337
2₁(13)	→	14
2₁(135)	→	136
2₁(330)	→	331
2₁(317)	→	318
2₁(977)	→	978
2₁(773)	→	774
2₁(199)	→	200
2₁(171)	→	172
2₁(813)	→	814
2₁(245)	→	246
2₁(975)	→	976
2₁(41)	→	42
2₁(39)	→	40
2₁(201)	→	202
2₁(648)	→	649
2₁(178)	→	179
2₁(811)	→	812
2₁(125)	→	126
2₁(182)	→	183
2₁(244)	→	245
2₁(256)	→	257
2₁(924)	→	925
2₁(254)	→	255
2₁(870)	→	871
2₁(72)	→	73
4₂(910)	→	911
4₂(891)	→	892
3₂(889)	→	890
3₂(890)	→	891
3₂(866)	→	867
3₂(451)	→	452
3₂(449)	→	450
3₂(417)	→	418
1₂(909)	→	910
1₂(906)	→	907
1₂(450)	→	451
5₁(794)	→	795
5₁(253)	→	254
5₁(884)	→	885
5₁(331)	→	332
5₁(93)	→	94
5₁(1104)	→	1105
5₁(221)	→	222
5₁(1009)	→	1010
5₁(650)	→	651
5₁(48)	→	49
5₁(296)	→	297
5₁(211)	→	212
5₁(78)	→	79
5₁(292)	→	293
5₁(1106)	→	1107
5₁(761)	→	762
5₁(597)	→	598
5₁(29)	→	30
5₁(967)	→	968
5₁(291)	→	292
5₁(284)	→	285
5₁(1011)	→	1012
5₁(337)	→	338
5₁(647)	→	648
5₁(472)	→	473
5₁(141)	→	142
5₁(880)	→	881
5₁(948)	→	949
5₁(332)	→	333
5₁(210)	→	211
5₁(801)	→	802
5₁(73)	→	74
5₁(179)	→	180
5₁(646)	→	647
5₁(645)	→	646
5₁(300)	→	301
5₁(52)	→	53
5₁(787)	→	788
5₁(765)	→	766
5₁(155)	→	156
5₁(74)	→	75
5₁(1013)	→	1014
5₁(886)	→	887
5₁(96)	→	97
5₁(123)	→	124
5₁(259)	→	260
5₁(89)	→	90
5₁(496)	→	497
5₁(362)	→	363
5₁(785)	→	786
5₁(297)	→	298
5₁(364)	→	365
5₁(25)	→	26
5₁(783)	→	784
5₁(969)	→	970
5₁(218)	→	219
5₁(843)	→	844
5₁(64)	→	65
5₁(878)	→	879
5₁(1069)	→	1070
5₁(233)	→	234
5₁(845)	→	846
5₁(971)	→	972
5₁(313)	→	314
5₁(205)	→	206
5₁(882)	→	883
5₁(75)	→	76
5₁(278)	→	279
4₀(7)	→	7
3₃(999)	→	1000
5₀(7)	→	7
5₂(902)	→	903
5₂(888)	→	889
2₃(1000)	→	1001
3₀(7)	→	7
3₁(170)	→	171
3₁(19)	→	20
3₁(797)	→	798
3₁(286)	→	287
3₁(108)	→	109
3₁(1039)	→	1040
3₁(17)	→	18
3₁(341)	→	342
3₁(973)	→	974
3₁(1136)	→	1137
3₁(142)	→	143
3₁(774)	→	775
3₁(796)	→	797
3₁(99)	→	100
3₁(771)	→	772
3₁(281)	→	282
3₁(372)	→	373
3₁(1128)	→	1129
3₁(335)	→	336
3₁(370)	→	371
3₁(1037)	→	1038
3₁(124)	→	125
3₁(26)	→	27
3₁(242)	→	243
3₁(649)	→	650
3₁(198)	→	199
3₁(1007)	→	1008
3₁(236)	→	237
3₁(775)	→	776
3₁(295)	→	296
3₁(90)	→	91
3₁(1061)	→	1062
3₁(220)	→	221
3₁(1017)	→	1018
3₁(147)	→	148
3₁(248)	→	249
3₁(1144)	→	1145
3₁(209)	→	210
3₁(914)	→	915
3₁(235)	→	236
3₁(848)	→	849
3₁(817)	→	818
3₁(853)	→	854
3₁(290)	→	291
3₁(119)	→	120
3₁(1102)	→	1103
3₁(298)	→	299
3₁(918)	→	919
3₁(189)	→	190
3₁(922)	→	923
3₁(31)	→	32
3₁(1019)	→	1020
3₁(30)	→	31
3₁(338)	→	339
3₁(805)	→	806
3₁(311)	→	312
3₁(916)	→	917
3₁(1134)	→	1135
3₁(95)	→	96
3₁(379)	→	380
3₁(121)	→	122
3₁(185)	→	186
3₁(367)	→	368
3₁(144)	→	145
3₁(126)	→	127
3₁(596)	→	597
3₁(851)	→	852
3₁(1043)	→	1044
3₁(109)	→	110
3₁(51)	→	52
3₁(77)	→	78
3₁(214)	→	215
3₁(212)	→	213
3₁(920)	→	921
3₁(1049)	→	1050
3₁(174)	→	175
3₁(68)	→	69
3₁(303)	→	304
3₁(1100)	→	1101
3₁(1130)	→	1131
3₁(12)	→	13
3₁(111)	→	112
3₁(188)	→	189
3₁(231)	→	232
3₁(466)	→	467
3₁(322)	→	323
3₁(272)	→	273
3₁(792)	→	793
3₁(1041)	→	1042
3₁(1132)	→	1133
0₁(340)	→	341
0₁(502)	→	503
0₁(138)	→	139
0₁(146)	→	147
0₁(857)	→	858
0₁(1055)	→	1056
0₁(742)	→	743
0₁(176)	→	177
0₁(376)	→	377
0₁(936)	→	937
0₁(934)	→	935
0₁(1142)	→	1143
0₁(368)	→	369
0₁(1053)	→	1054
0₁(643)	→	644
0₁(87)	→	88
0₁(859)	→	860
0₁(506)	→	507
0₁(849)	→	850
0₁(1090)	→	1091
0₁(328)	→	329
0₁(79)	→	80
0₁(200)	→	201
0₁(227)	→	228
0₁(799)	→	800
0₁(930)	→	931
0₁(97)	→	98
0₁(40)	→	41
0₁(169)	→	170
0₁(510)	→	511
0₁(120)	→	121
0₁(762)	→	763
0₁(800)	→	801
0₁(238)	→	239
0₁(91)	→	92
0₁(803)	→	804
0₁(114)	→	115
0₁(1138)	→	1139
0₁(183)	→	184
0₁(215)	→	216
0₁(251)	→	252
0₁(823)	→	824
0₁(854)	→	855
0₁(71)	→	72
0₁(989)	→	990
0₁(241)	→	242
0₁(373)	→	374
0₁(769)	→	770
0₁(938)	→	939
0₁(14)	→	15
0₁(239)	→	240
0₁(1051)	→	1052
0₁(43)	→	44
0₁(944)	→	945
0₁(657)	→	658
0₁(299)	→	300
0₁(651)	→	652
0₁(44)	→	45
0₁(1059)	→	1060
0₁(319)	→	320
0₁(375)	→	376
0₁(149)	→	150
0₁(788)	→	789
0₁(858)	→	859
0₁(505)	→	506
0₁(276)	→	277
0₁(856)	→	857
0₁(33)	→	34
0₁(294)	→	295
0₁(136)	→	137
0₁(100)	→	101
0₁(377)	→	378
0₁(814)	→	815
0₁(981)	→	982
0₁(112)	→	113
1₀(7)	→	7
2₀(7)	→	7
4₁(92)	→	93
4₁(101)	→	102
4₁(186)	→	187
4₁(940)	→	941
4₁(237)	→	238
4₁(821)	→	822
4₁(134)	→	135
4₁(217)	→	218
4₁(302)	→	303
4₁(993)	→	994
4₁(508)	→	509
4₁(98)	→	99
4₁(279)	→	280
4₁(232)	→	233
4₁(365)	→	366
4₁(791)	→	792
4₁(790)	→	791
4₁(117)	→	118
4₁(63)	→	64
4₁(154)	→	155
4₁(184)	→	185
4₁(228)	→	229
4₁(809)	→	810
4₁(153)	→	154
4₁(798)	→	799
4₁(32)	→	33
4₁(167)	→	168
4₁(946)	→	947
4₁(181)	→	182
4₁(229)	→	230
4₁(258)	→	259
4₁(137)	→	138
4₁(107)	→	108
4₁(767)	→	768
4₁(361)	→	362
4₁(280)	→	281
4₁(343)	→	344
4₁(230)	→	231
4₁(203)	→	204
4₁(942)	→	943
4₁(304)	→	305
4₁(46)	→	47
4₁(202)	→	203
4₁(110)	→	111
4₁(772)	→	773
4₁(844)	→	845
4₁(282)	→	283
4₁(115)	→	116
4₁(846)	→	847
4₁(314)	→	315
4₁(143)	→	144
4₁(50)	→	51
4₁(204)	→	205
4₁(197)	→	198
4₁(793)	→	794
4₁(770)	→	771
4₁(995)	→	996
4₁(789)	→	790
4₁(755)	→	756
4₁(1098)	→	1099
4₁(301)	→	302
4₁(363)	→	364
0₃(1001)	→	1002
1₁(65)	→	66
1₁(366)	→	367
1₁(18)	→	19
1₁(305)	→	306
1₁(329)	→	330
1₁(983)	→	984
1₁(766)	→	767
1₁(249)	→	250
1₁(190)	→	191
1₁(374)	→	375
1₁(777)	→	778
1₁(855)	→	856
1₁(180)	→	181
1₁(822)	→	823
1₁(321)	→	322
1₁(333)	→	334
1₁(255)	→	256
1₁(177)	→	178
1₁(807)	→	808
1₁(334)	→	335
1₁(293)	→	294
1₁(66)	→	67
1₁(275)	→	276
1₁(69)	→	70
1₁(45)	→	46
1₁(1096)	→	1097
1₁(504)	→	505
1₁(847)	→	848
1₁(42)	→	43
1₁(85)	→	86
1₁(273)	→	274
1₁(243)	→	244
1₁(86)	→	87
1₁(991)	→	992
1₁(140)	→	141
1₁(152)	→	153
1₁(139)	→	140
1₁(151)	→	152
1₁(816)	→	817
1₁(172)	→	173
1₁(257)	→	258
1₁(507)	→	508
1₁(148)	→	149
1₁(288)	→	289
1₁(250)	→	251
1₁(776)	→	777
1₁(213)	→	214
1₁(283)	→	284
1₁(62)	→	63
1₁(763)	→	764
0₂(907)	→	908
0₂(892)	→	893
0₂(904)	→	905
0₂(868)	→	869
0₂(908)	→	909
0₂(419)	→	420
0₀(7)	→	7
2₂(903)	→	904
2₂(905)	→	906
2₂(876)	→	877
2₂(867)	→	868
2₂(418)	→	419
2₂(448)	→	449

The automaton is closed under rewriting as it is compatible.