Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/86636)

The rewrite relation of the following TRS is considered.

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

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:

279	→	73
314	→	263
871	→	233
871	→	184
871	→	7
871	→	144
871	→	197
871	→	115
871	→	965
871	→	265
871	→	15
871	→	980
221	→	923
958	→	74
958	→	961
61	→	83
61	→	92
61	→	284
61	→	341
61	→	159
61	→	60
61	→	31
61	→	13
61	→	44
61	→	114
61	→	7
61	→	85
61	→	370
61	→	971
61	→	491
61	→	20
61	→	976
61	→	948
32	→	49
32	→	67
32	→	324
32	→	159
32	→	60
32	→	31
32	→	13
32	→	44
32	→	114
32	→	7
32	→	847
32	→	982
29	→	1016
750	→	1046
15	→	18
15	→	265
15	→	915
15	→	965
383	→	29
383	→	660
383	→	894
882	→	14
84	→	405
167	→	26
956	→	74
956	→	959
122	→	29
299	→	15
978	→	15
39	→	7
39	→	168
39	→	234
39	→	105
39	→	45
39	→	33
39	→	389
39	→	107
39	→	848
980	→	15
298	→	913
914	→	15
931	→	1044
209	→	16
209	→	1048
147	→	949
37	→	594
515	→	233
515	→	184
515	→	7
515	→	144
515	→	197
515	→	115
891	→	342
889	→	342
20	→	491
62	→	513
942	→	62
31	→	947
31	→	957
31	→	979
246	→	28
968	→	342
922	→	14
716	→	20
716	→	890
490	→	234
884	→	266
402	→	881
488	→	883
179	→	29
235	→	251
235	→	7
235	→	160
38	→	432
38	→	749
86	→	369
920	→	405
91	→	16
36	→	925
170	→	943
916	→	15
924	→	27
21	→	7
21	→	251
21	→	160
21	→	235
21	→	61
21	→	51
21	→	198
21	→	888
21	→	266
186	→	388
912	→	324
912	→	49
912	→	7
912	→	106
912	→	67
912	→	32
976	→	20
918	→	15
911	→	941
911	→	973
1053	→	406
404	→	74
116	→	300
1051	→	19
1051	→	1052
982	→	406
75	→	7
75	→	220
75	→	26
75	→	135
75	→	134
75	→	14
75	→	160
75	→	892
75	→	74
75	→	961
75	→	958
1047	→	94
433	→	208
368	→	313
264	→	29
143	→	38
53	→	19
232	→	90
843	→	74
843	→	857
45	→	105
45	→	168
1015	→	930
66	→	28
16	→	715
16	→	842
16	→	917
14	→	26
14	→	134
14	→	220
14	→	846
1045	→	38
1045	→	1050
972	→	342
63	→	358
514	→	1009
100	→	74
944	→	65
7	→	13
7	→	31
7	→	44
7	→	60
7	→	114
7	→	159
234	→	921
1049	→	287
758	→	300
758	→	7
758	→	160
758	→	116
758	→	287
758	→	966
934	→	15
113	→	19
960	→	221
30	→	7
30	→	233
30	→	184
30	→	144
30	→	197
30	→	115
30	→	61
30	→	300
30	→	160
30	→	116
30	→	221
30	→	145
30	→	251
30	→	235
30	→	93
30	→	27
30	→	50
30	→	343
30	→	169
30	→	324
30	→	49
30	→	106
30	→	67
30	→	32
30	→	370
30	→	965
30	→	265
30	→	15
30	→	980
30	→	971
30	→	976
30	→	948
30	→	287
30	→	966
30	→	962
30	→	916
30	→	893
962	→	221
950	→	96
856	→	251
856	→	7
856	→	160
856	→	235
948	→	20
948	→	971
115	→	144
115	→	184
115	→	197
115	→	233
115	→	951
893	→	61
952	→	94
48	→	27
198	→	933
17	→	7
17	→	324
17	→	49
17	→	67
17	→	32
17	→	106
17	→	185
17	→	233
17	→	184
17	→	144
17	→	197
17	→	115
17	→	388
17	→	186
17	→	917
17	→	715
17	→	842
17	→	16
17	→	965
17	→	265
17	→	15
17	→	980
946	→	20
946	→	967
160	→	975
160	→	981
1017	→	1010
154	→	121
870	→	945
870	→	955
870	→	977
492	→	487
974	→	19
340	→	15
353	→	263
353	→	919
74	→	892
422	→	263
932	→	85
932	→	370
932	→	971
932	→	491
932	→	61
932	→	976
932	→	948
266	→	888
403	→	486
966	→	287
599	→	60
661	→	62
196	→	28
0₁(260)	→	261
0₁(99)	→	100
0₁(293)	→	294
0₁(756)	→	757
0₁(15)	→	16
0₁(753)	→	754
0₁(170)	→	171
0₁(231)	→	232
0₁(381)	→	382
0₁(255)	→	256
0₁(140)	→	141
0₁(370)	→	371
0₁(851)	→	852
0₁(153)	→	154
0₁(360)	→	361
0₁(235)	→	236
0₁(1052)	→	1053
0₁(981)	→	982
0₁(846)	→	847
0₁(136)	→	137
0₁(111)	→	112
0₁(405)	→	406
0₁(417)	→	418
0₁(107)	→	108
0₁(52)	→	53
0₁(16)	→	17
0₁(890)	→	891
0₁(86)	→	87
0₁(118)	→	119
0₁(312)	→	313
0₁(204)	→	205
0₁(138)	→	139
0₁(341)	→	342
0₁(184)	→	185
0₁(853)	→	854
0₁(105)	→	106
0₁(888)	→	889
0₁(295)	→	296
0₁(230)	→	231
0₁(298)	→	299
0₁(336)	→	337
0₁(177)	→	178
0₁(868)	→	869
0₁(971)	→	972
0₁(395)	→	396
0₁(867)	→	868
0₁(909)	→	910
0₁(98)	→	99
0₁(967)	→	968
0₁(31)	→	32
0₁(175)	→	176
0₁(253)	→	254
0₁(300)	→	301
0₁(185)	→	186
0₁(121)	→	122
0₁(898)	→	899
0₁(870)	→	871
1₂(926)	→	927
1₂(1012)	→	1013
4₂(927)	→	928
4₂(930)	→	931
5₂(1014)	→	1015
5₂(1011)	→	1012
5₂(1016)	→	1017
5₂(1013)	→	1014
5₂(931)	→	932
5₂(1009)	→	1010
3₁(208)	→	209
3₁(923)	→	924
3₁(159)	→	160
3₁(308)	→	309
3₁(866)	→	867
3₁(919)	→	920
3₁(377)	→	378
3₁(148)	→	149
3₁(296)	→	297
3₁(402)	→	403
3₁(162)	→	163
3₁(20)	→	21
3₁(289)	→	290
3₁(201)	→	202
3₁(115)	→	116
3₁(401)	→	402
3₁(229)	→	230
3₁(243)	→	244
3₁(14)	→	15
3₁(389)	→	390
3₁(69)	→	70
3₁(1050)	→	1051
3₁(285)	→	286
3₁(37)	→	38
3₁(965)	→	966
3₁(905)	→	906
3₁(277)	→	278
3₁(139)	→	140
3₁(244)	→	245
3₁(347)	→	348
3₁(345)	→	346
3₁(973)	→	974
3₁(286)	→	287
3₁(1048)	→	1049
3₁(85)	→	86
3₁(47)	→	48
3₁(409)	→	410
3₁(848)	→	849
3₁(259)	→	260
3₁(89)	→	90
3₁(252)	→	253
3₁(33)	→	34
3₁(364)	→	365
3₁(343)	→	344
3₁(403)	→	404
3₁(256)	→	257
3₁(172)	→	173
3₁(487)	→	488
3₁(896)	→	897
3₁(596)	→	597
3₁(329)	→	330
3₁(306)	→	307
3₁(313)	→	314
3₁(83)	→	84
3₁(894)	→	895
3₁(200)	→	201
3₁(203)	→	204
3₁(750)	→	751
3₁(234)	→	235
4₀(7)	→	7
5₀(7)	→	7
3₀(7)	→	7
5₁(19)	→	20
5₁(892)	→	893
5₁(29)	→	30
5₁(399)	→	400
5₁(406)	→	407
5₁(327)	→	328
5₁(192)	→	193
5₁(164)	→	165
5₁(278)	→	279
5₁(489)	→	490
5₁(391)	→	392
5₁(362)	→	363
5₁(349)	→	350
5₁(335)	→	336
5₁(50)	→	51
5₁(358)	→	359
5₁(26)	→	27
5₁(369)	→	370
5₁(60)	→	61
5₁(226)	→	227
5₁(304)	→	305
5₁(202)	→	203
5₁(84)	→	85
5₁(975)	→	976
5₁(207)	→	208
5₁(411)	→	412
5₁(376)	→	377
5₁(911)	→	912
5₁(348)	→	349
5₁(67)	→	68
5₁(334)	→	335
5₁(897)	→	898
5₁(904)	→	905
5₁(149)	→	150
5₁(350)	→	351
5₁(267)	→	268
5₁(119)	→	120
5₁(1044)	→	1045
5₁(416)	→	417
5₁(35)	→	36
5₁(346)	→	347
5₁(206)	→	207
5₁(261)	→	262
5₁(70)	→	71
5₁(62)	→	63
5₁(947)	→	948
5₁(197)	→	198
5₁(65)	→	66
5₁(943)	→	944
5₁(910)	→	911
5₁(302)	→	303
5₁(757)	→	758
5₁(754)	→	755
5₁(945)	→	946
5₁(514)	→	515
5₁(895)	→	896
5₁(394)	→	395
5₁(382)	→	383
5₁(863)	→	864
5₁(361)	→	362
5₁(326)	→	327
5₁(419)	→	420
5₁(109)	→	110
5₁(64)	→	65
5₁(883)	→	884
5₁(331)	→	332
5₁(418)	→	419
5₁(291)	→	292
5₁(352)	→	353
5₁(325)	→	326
5₁(855)	→	856
5₁(265)	→	266
5₁(412)	→	413
5₁(359)	→	360
5₁(187)	→	188
5₁(71)	→	72
5₁(715)	→	716
5₁(272)	→	273
5₁(168)	→	169
2₁(303)	→	304
2₁(90)	→	91
2₁(262)	→	263
2₁(147)	→	148
2₁(263)	→	264
2₁(236)	→	237
2₁(275)	→	276
2₁(330)	→	331
2₁(869)	→	870
2₁(859)	→	860
2₁(407)	→	408
2₁(305)	→	306
2₁(137)	→	138
2₁(233)	→	234
2₁(72)	→	73
2₁(198)	→	199
2₁(273)	→	274
2₁(193)	→	194
2₁(152)	→	153
2₁(68)	→	69
2₁(862)	→	863
2₁(268)	→	269
2₁(205)	→	206
2₁(311)	→	312
2₁(34)	→	35
2₁(906)	→	907
2₁(120)	→	121
2₁(258)	→	259
2₁(388)	→	389
2₁(32)	→	33
2₁(61)	→	62
2₁(225)	→	226
2₁(222)	→	223
2₁(378)	→	379
2₁(251)	→	252
2₁(269)	→	270
2₁(38)	→	39
2₁(241)	→	242
2₁(755)	→	756
2₁(847)	→	848
2₁(420)	→	421
2₁(344)	→	345
2₁(307)	→	308
2₁(151)	→	152
2₁(171)	→	172
2₁(163)	→	164
2₁(228)	→	229
2₁(865)	→	866
2₁(36)	→	37
2₁(941)	→	942
2₁(27)	→	28
2₁(374)	→	375
2₁(44)	→	45
2₁(292)	→	293
2₁(400)	→	401
2₁(660)	→	661
2₁(106)	→	107
2₁(332)	→	333
2₁(254)	→	255
2₁(339)	→	340
2₁(414)	→	415
2₁(902)	→	903
2₁(597)	→	598
2₁(309)	→	310
2₁(150)	→	151
2₁(160)	→	161
2₁(408)	→	409
2₁(257)	→	258
2₁(397)	→	398
2₁(338)	→	339
2₁(112)	→	113
1₀(7)	→	7
2₀(7)	→	7
4₁(92)	→	93
4₁(186)	→	187
4₁(861)	→	862
4₁(94)	→	95
4₁(949)	→	950
4₁(351)	→	352
4₁(166)	→	167
4₁(917)	→	918
4₁(595)	→	596
4₁(365)	→	366
4₁(513)	→	514
4₁(146)	→	147
4₁(114)	→	115
4₁(117)	→	118
4₁(979)	→	980
4₁(372)	→	373
4₁(144)	→	145
4₁(290)	→	291
4₁(276)	→	277
4₁(410)	→	411
4₁(165)	→	166
4₁(900)	→	901
4₁(220)	→	221
4₁(88)	→	89
4₁(189)	→	190
4₁(49)	→	50
4₁(390)	→	391
4₁(752)	→	753
4₁(392)	→	393
4₁(367)	→	368
4₁(366)	→	367
4₁(977)	→	978
4₁(913)	→	914
4₁(297)	→	298
4₁(294)	→	295
4₁(188)	→	189
4₁(135)	→	136
4₁(242)	→	243
4₁(46)	→	47
4₁(310)	→	311
4₁(110)	→	111
4₁(274)	→	275
4₁(191)	→	192
4₁(961)	→	962
4₁(380)	→	381
4₁(328)	→	329
4₁(857)	→	858
4₁(908)	→	909
4₁(852)	→	853
4₁(176)	→	177
4₁(270)	→	271
4₁(224)	→	225
4₁(749)	→	750
4₁(28)	→	29
4₁(398)	→	399
4₁(238)	→	239
4₁(396)	→	397
4₁(598)	→	599
4₁(915)	→	916
4₁(95)	→	96
4₁(195)	→	196
4₁(97)	→	98
4₁(194)	→	195
4₁(287)	→	288
4₁(393)	→	394
4₁(96)	→	97
4₁(342)	→	343
4₁(363)	→	364
4₁(959)	→	960
1₁(337)	→	338
1₁(266)	→	267
1₁(134)	→	135
1₁(849)	→	850
1₁(18)	→	19
1₁(199)	→	200
1₁(271)	→	272
1₁(190)	→	191
1₁(860)	→	861
1₁(488)	→	489
1₁(324)	→	325
1₁(955)	→	956
1₁(850)	→	851
1₁(237)	→	238
1₁(116)	→	117
1₁(333)	→	334
1₁(371)	→	372
1₁(63)	→	64
1₁(74)	→	75
1₁(486)	→	487
1₁(223)	→	224
1₁(169)	→	170
1₁(415)	→	416
1₁(854)	→	855
1₁(921)	→	922
1₁(903)	→	904
1₁(45)	→	46
1₁(240)	→	241
1₁(145)	→	146
1₁(933)	→	934
1₁(178)	→	179
1₁(858)	→	859
1₁(227)	→	228
1₁(13)	→	14
1₁(73)	→	74
1₁(51)	→	52
1₁(161)	→	162
1₁(594)	→	595
1₁(173)	→	174
1₁(413)	→	414
1₁(901)	→	902
1₁(141)	→	142
1₁(221)	→	222
1₁(93)	→	94
1₁(432)	→	433
1₁(957)	→	958
1₁(491)	→	492
1₁(864)	→	865
1₁(284)	→	285
1₁(751)	→	752
1₁(142)	→	143
1₁(375)	→	376
1₁(174)	→	175
1₁(951)	→	952
1₁(288)	→	289
1₁(87)	→	88
1₁(301)	→	302
1₁(379)	→	380
1₁(899)	→	900
1₁(881)	→	882
1₁(373)	→	374
1₁(421)	→	422
1₁(245)	→	246
1₁(842)	→	843
1₁(1046)	→	1047
1₁(108)	→	109
1₁(907)	→	908
1₁(239)	→	240
3₂(928)	→	929
0₀(7)	→	7
2₂(1010)	→	1011
2₂(925)	→	926
2₂(929)	→	930

The automaton is closed under rewriting as it is compatible.