Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/64160)

The rewrite relation of the following TRS is considered.

1(2(1(1(0(0(1(0(2(1(1(0(2(x1)))))))))))))	→	1(2(2(1(0(0(2(0(1(2(2(0(1(0(0(2(2(x1)))))))))))))))))	(1)
2(0(1(2(1(2(1(2(1(0(0(1(0(x1)))))))))))))	→	2(2(0(0(2(1(1(1(0(0(0(1(1(1(2(2(0(x1)))))))))))))))))	(2)
2(1(0(0(2(1(1(1(0(1(2(2(0(x1)))))))))))))	→	0(0(2(1(0(0(1(1(2(2(2(2(2(1(2(1(0(x1)))))))))))))))))	(3)
2(2(0(0(1(0(2(1(1(1(0(0(1(x1)))))))))))))	→	2(2(1(1(2(0(0(1(2(2(0(2(0(0(2(2(2(x1)))))))))))))))))	(4)
2(2(1(0(1(0(1(1(0(0(0(2(0(x1)))))))))))))	→	0(2(2(1(0(0(1(0(0(1(1(1(1(0(0(2(0(x1)))))))))))))))))	(5)
2(2(1(1(0(2(0(0(0(2(2(0(0(x1)))))))))))))	→	0(0(1(2(0(0(0(2(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))	(6)
2(2(2(1(0(2(0(0(1(0(1(0(2(x1)))))))))))))	→	0(2(2(0(0(2(2(2(1(2(0(0(2(2(0(2(2(x1)))))))))))))))))	(7)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{4}

transitions:

339	→	367
221	→	42
176	→	25
25	→	80
25	→	208
128	→	78
128	→	175
81	→	341
81	→	352
273	→	254
374	→	66
39	→	309
209	→	377
130	→	371
380	→	24
40	→	4
26	→	163
269	→	24
269	→	41
269	→	23
269	→	4
269	→	65
79	→	4
79	→	272
79	→	24
79	→	65
79	→	80
79	→	81
79	→	25
58	→	4
58	→	114
58	→	132
349	→	379
207	→	26
220	→	369
308	→	130
174	→	126
368	→	25
67	→	373
143	→	77
4	→	23
4	→	41
28	→	328
93	→	56
370	→	64
42	→	63
42	→	129
310	→	294
340	→	80
340	→	4
340	→	24
340	→	25
353	→	341
142	→	293
132	→	80
132	→	4
132	→	24
132	→	25
132	→	44
378	→	65
24	→	206
351	→	339
43	→	114
43	→	4
43	→	24
372	→	64
56	→	253
2₀(4)	→	4
0₀(4)	→	4
1₀(4)	→	4
2₁(164)	→	165
2₁(169)	→	170
2₁(130)	→	131
2₁(132)	→	133
2₁(259)	→	260
2₁(305)	→	306
2₁(377)	→	378
2₁(37)	→	38
2₁(137)	→	138
2₁(80)	→	81
2₁(70)	→	71
2₁(23)	→	24
2₁(163)	→	164
2₁(254)	→	255
2₁(24)	→	25
2₁(367)	→	368
2₁(29)	→	30
2₁(343)	→	344
2₁(127)	→	128
2₁(76)	→	77
2₁(266)	→	267
2₁(309)	→	310
2₁(167)	→	168
2₁(131)	→	132
2₁(301)	→	302
2₁(175)	→	176
2₁(344)	→	345
2₁(298)	→	299
2₁(86)	→	87
2₁(293)	→	294
2₁(258)	→	259
2₁(57)	→	58
2₁(133)	→	134
2₁(38)	→	39
2₁(352)	→	353
2₁(256)	→	257
2₁(53)	→	54
2₁(337)	→	338
2₁(85)	→	86
2₁(294)	→	295
2₁(257)	→	258
2₁(141)	→	142
2₁(300)	→	301
2₁(83)	→	84
2₁(171)	→	172
2₁(64)	→	65
2₁(43)	→	44
2₁(295)	→	296
2₁(90)	→	91
2₁(126)	→	127
2₁(42)	→	43
2₁(136)	→	137
2₁(33)	→	34
2₁(379)	→	380
2₁(56)	→	57
2₁(220)	→	221
2₁(338)	→	339
2₁(217)	→	218
2₁(69)	→	70
2₁(260)	→	261
2₁(66)	→	67
2₁(67)	→	68
2₁(30)	→	31
2₁(170)	→	171
2₁(68)	→	69
2₁(348)	→	349
1₁(51)	→	52
1₁(330)	→	331
1₁(336)	→	337
1₁(46)	→	47
1₁(329)	→	330
1₁(117)	→	118
1₁(91)	→	92
1₁(306)	→	307
1₁(371)	→	372
1₁(65)	→	66
1₁(134)	→	135
1₁(50)	→	51
1₁(255)	→	256
1₁(36)	→	37
1₁(215)	→	216
1₁(71)	→	72
1₁(92)	→	93
1₁(373)	→	374
1₁(63)	→	64
1₁(341)	→	342
1₁(272)	→	273
1₁(214)	→	215
1₁(87)	→	88
1₁(118)	→	119
1₁(216)	→	217
1₁(125)	→	126
1₁(262)	→	263
1₁(208)	→	209
1₁(307)	→	308
1₁(27)	→	28
1₁(52)	→	53
1₁(302)	→	303
1₁(45)	→	46
1₁(75)	→	76
1₁(369)	→	370
1₁(333)	→	334
1₁(39)	→	40
1₁(142)	→	143
1₁(209)	→	210
1₁(349)	→	350
1₁(44)	→	45
1₁(253)	→	254
1₁(261)	→	262
1₁(31)	→	32
1₁(210)	→	211
1₁(328)	→	329
1₁(72)	→	73
1₁(116)	→	117
1₁(122)	→	123
1₁(265)	→	266
1₁(119)	→	120
1₁(168)	→	169
0₁(339)	→	340
0₁(82)	→	83
0₁(219)	→	220
0₁(350)	→	351
0₁(304)	→	305
0₁(129)	→	130
0₁(267)	→	268
0₁(331)	→	332
0₁(77)	→	78
0₁(47)	→	48
0₁(138)	→	139
0₁(54)	→	55
0₁(26)	→	27
0₁(115)	→	116
0₁(41)	→	42
0₁(335)	→	336
0₁(347)	→	348
0₁(346)	→	347
0₁(166)	→	167
0₁(173)	→	174
0₁(48)	→	49
0₁(124)	→	125
0₁(268)	→	269
0₁(88)	→	89
0₁(297)	→	298
0₁(211)	→	212
0₁(212)	→	213
0₁(206)	→	207
0₁(81)	→	82
0₁(342)	→	343
0₁(73)	→	74
0₁(55)	→	56
0₁(172)	→	173
0₁(213)	→	214
0₁(28)	→	29
0₁(84)	→	85
0₁(263)	→	264
0₁(74)	→	75
0₁(89)	→	90
0₁(35)	→	36
0₁(218)	→	219
0₁(135)	→	136
0₁(120)	→	121
0₁(345)	→	346
0₁(165)	→	166
0₁(332)	→	333
0₁(123)	→	124
0₁(296)	→	297
0₁(32)	→	33
0₁(139)	→	140
0₁(49)	→	50
0₁(114)	→	115
0₁(25)	→	26
0₁(303)	→	304
0₁(299)	→	300
0₁(334)	→	335
0₁(264)	→	265
0₁(140)	→	141
0₁(78)	→	79
0₁(121)	→	122
0₁(34)	→	35

The automaton is closed under rewriting as it is compatible.