Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4002)

The rewrite relation of the following TRS is considered.

2(5(3(0(x1))))	→	1(0(0(1(3(0(4(5(1(2(x1))))))))))	(1)
1(3(5(4(3(x1)))))	→	2(1(4(1(4(0(3(0(1(1(x1))))))))))	(2)
5(1(3(5(0(x1)))))	→	5(1(4(3(0(4(4(5(2(1(x1))))))))))	(3)
5(4(4(2(5(x1)))))	→	4(3(1(1(1(1(5(3(3(5(x1))))))))))	(4)
2(2(5(0(5(4(x1))))))	→	2(1(4(1(3(3(2(2(5(4(x1))))))))))	(5)
3(0(5(5(4(3(x1))))))	→	3(3(0(3(2(3(5(5(1(0(x1))))))))))	(6)
3(5(4(3(5(2(x1))))))	→	2(0(5(2(0(5(2(2(3(2(x1))))))))))	(7)
4(4(2(5(5(0(x1))))))	→	4(4(0(0(3(3(3(2(2(3(x1))))))))))	(8)
4(5(3(5(5(0(x1))))))	→	4(2(2(3(0(2(4(1(1(5(x1))))))))))	(9)
5(4(5(1(1(2(x1))))))	→	5(4(0(3(3(3(3(2(5(5(x1))))))))))	(10)
5(5(5(5(5(3(x1))))))	→	5(5(0(1(4(0(0(5(0(1(x1))))))))))	(11)
3(5(0(0(5(4(3(x1)))))))	→	0(1(2(1(1(5(5(2(1(0(x1))))))))))	(12)
3(5(4(2(5(2(3(x1)))))))	→	4(0(4(0(0(2(2(3(4(4(x1))))))))))	(13)
3(5(4(5(1(4(0(x1)))))))	→	1(1(1(0(0(3(3(1(2(5(x1))))))))))	(14)

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:

503	→	105
272	→	28
29	→	7
29	→	20
29	→	186
29	→	111
29	→	57
29	→	491
338	→	271
87	→	7
87	→	111
152	→	412
152	→	435
152	→	504
561	→	53
374	→	78
438	→	124
438	→	478
530	→	554
436	→	124
119	→	64
39	→	439
184	→	64
499	→	56
499	→	72
499	→	489
499	→	53
499	→	518
584	→	124
65	→	7
65	→	56
65	→	72
65	→	71
65	→	177
65	→	111
65	→	57
65	→	489
65	→	53
65	→	518
65	→	491
55	→	500
20	→	101
20	→	334
20	→	110
20	→	70
20	→	30
20	→	19
20	→	55
20	→	77
20	→	7
193	→	28
31	→	45
31	→	146
40	→	7
40	→	146
40	→	45
40	→	31
40	→	101
40	→	20
40	→	111
40	→	57
40	→	491
542	→	111
542	→	57
542	→	491
71	→	176
71	→	7
477	→	111
477	→	110
477	→	70
477	→	30
477	→	19
477	→	55
477	→	77
477	→	7
477	→	57
477	→	491
183	→	467
590	→	490
76	→	36
235	→	519
86	→	241
86	→	394
86	→	443
86	→	521
86	→	532
79	→	155
518	→	53
208	→	20
208	→	7
208	→	186
141	→	53
554	→	589
109	→	39
54	→	7
54	→	185
54	→	124
54	→	133
54	→	56
54	→	72
54	→	134
54	→	489
54	→	53
54	→	518
555	→	56
498	→	564
565	→	53
569	→	505
53	→	489
528	→	568
528	→	581
528	→	583
582	→	111
501	→	490
419	→	183
520	→	53
479	→	469
440	→	133
421	→	413
516	→	505
63	→	226
63	→	373
497	→	545
497	→	566
514	→	71
514	→	177
236	→	146
236	→	7
236	→	45
236	→	31
7	→	19
7	→	30
7	→	55
7	→	70
7	→	77
7	→	110
113	→	502
453	→	111
453	→	110
453	→	70
453	→	30
453	→	19
453	→	55
453	→	77
453	→	7
453	→	57
453	→	491
162	→	198
162	→	264
162	→	420
162	→	437
162	→	515
531	→	56
531	→	134
531	→	72
531	→	489
531	→	53
531	→	518
531	→	54
154	→	53
242	→	227
242	→	441
567	→	78
132	→	64
451	→	543
19	→	517
546	→	31
544	→	185
442	→	147
163	→	7
163	→	111
163	→	57
163	→	491
56	→	124
56	→	133
56	→	185
56	→	110
56	→	70
56	→	30
56	→	19
56	→	55
56	→	77
56	→	7
56	→	490
56	→	501
395	→	78
513	→	560
2₁(82)	→	83
2₁(45)	→	46
2₁(265)	→	266
2₁(447)	→	448
2₁(446)	→	447
2₁(106)	→	107
2₁(468)	→	469
2₁(155)	→	156
2₁(160)	→	161
2₁(103)	→	104
2₁(235)	→	236
2₁(73)	→	74
2₁(102)	→	103
2₁(111)	→	112
2₁(198)	→	199
2₁(127)	→	128
2₁(134)	→	135
2₁(112)	→	113
2₁(130)	→	131
2₁(131)	→	132
2₁(414)	→	415
2₁(334)	→	335
2₁(19)	→	20
2₁(39)	→	40
2₁(178)	→	179
2₁(478)	→	479
2₁(185)	→	186
2₁(179)	→	180
2₁(413)	→	414
2₁(72)	→	73
5₂(492)	→	493
5₂(500)	→	501
5₂(489)	→	490
5₂(529)	→	530
5₂(589)	→	590
5₂(530)	→	531
5₂(523)	→	524
4₂(541)	→	542
4₂(539)	→	540
4₂(498)	→	499
4₂(532)	→	533
4₂(513)	→	514
4₂(533)	→	534
4₂(512)	→	513
4₂(526)	→	527
0₂(525)	→	526
0₂(522)	→	523
0₂(537)	→	538
0₂(538)	→	539
0₂(510)	→	511
0₂(511)	→	512
0₂(540)	→	541
0₂(524)	→	525
0₂(528)	→	529
4₁(70)	→	71
4₁(452)	→	453
4₁(140)	→	141
4₁(267)	→	268
4₁(48)	→	49
4₁(126)	→	127
4₁(22)	→	23
4₁(201)	→	202
4₁(271)	→	272
4₁(35)	→	36
4₁(51)	→	52
4₁(37)	→	38
4₁(268)	→	269
4₁(443)	→	444
4₁(450)	→	451
4₁(564)	→	565
4₁(47)	→	48
4₁(176)	→	177
4₁(444)	→	445
4₁(118)	→	119
4₁(182)	→	183
4₁(560)	→	561
4₁(64)	→	65
4₁(233)	→	234
4₁(150)	→	151
4₁(231)	→	232
1₀(7)	→	7
4₀(7)	→	7
1₂(493)	→	494
1₂(521)	→	522
1₂(496)	→	497
1₂(494)	→	495
1₂(495)	→	496
1₂(527)	→	528
0₀(7)	→	7
1₁(125)	→	126
1₁(25)	→	26
1₁(186)	→	187
1₁(191)	→	192
1₁(78)	→	79
1₁(192)	→	193
1₁(227)	→	228
1₁(151)	→	152
1₁(476)	→	477
1₁(61)	→	62
1₁(124)	→	125
1₁(59)	→	60
1₁(60)	→	61
1₁(475)	→	476
1₁(226)	→	227
1₁(36)	→	37
1₁(241)	→	242
1₁(28)	→	29
1₁(207)	→	208
1₁(474)	→	475
1₁(234)	→	235
1₁(469)	→	470
1₁(20)	→	21
1₁(161)	→	162
1₁(545)	→	546
1₁(232)	→	233
1₁(52)	→	53
1₁(159)	→	160
1₁(31)	→	32
1₁(30)	→	31
1₁(62)	→	63
1₁(158)	→	159
1₁(38)	→	39
1₁(199)	→	200
1₁(204)	→	205
1₁(264)	→	265
1₁(337)	→	338
0₁(146)	→	147
0₁(472)	→	473
0₁(180)	→	181
0₁(418)	→	419
0₁(449)	→	450
0₁(77)	→	78
0₁(105)	→	106
0₁(230)	→	231
0₁(189)	→	190
0₁(566)	→	567
0₁(128)	→	129
0₁(152)	→	153
0₁(394)	→	395
0₁(448)	→	449
0₁(205)	→	206
0₁(139)	→	140
0₁(34)	→	35
0₁(202)	→	203
0₁(32)	→	33
0₁(190)	→	191
0₁(181)	→	182
0₁(183)	→	184
0₁(23)	→	24
0₁(206)	→	207
0₁(269)	→	270
0₁(441)	→	442
0₁(84)	→	85
0₁(117)	→	118
0₁(373)	→	374
0₁(49)	→	50
0₁(148)	→	149
0₁(162)	→	163
0₁(228)	→	229
0₁(26)	→	27
0₁(473)	→	474
0₁(27)	→	28
0₁(116)	→	117
0₁(149)	→	150
0₁(108)	→	109
0₁(451)	→	452
5₀(7)	→	7
3₀(7)	→	7
5₁(266)	→	267
5₁(437)	→	438
5₁(58)	→	59
5₁(55)	→	56
5₁(543)	→	544
5₁(71)	→	72
5₁(104)	→	105
5₁(153)	→	154
5₁(133)	→	134
5₁(554)	→	555
5₁(21)	→	22
5₁(200)	→	201
5₁(147)	→	148
5₁(107)	→	108
5₁(502)	→	503
5₁(467)	→	468
5₁(79)	→	80
5₁(46)	→	47
5₁(517)	→	518
5₁(439)	→	440
5₁(435)	→	436
5₁(53)	→	54
5₁(519)	→	520
5₁(157)	→	158
5₁(583)	→	584
5₁(156)	→	157
5₁(80)	→	81
3₁(417)	→	418
3₁(581)	→	582
3₁(129)	→	130
3₁(470)	→	471
3₁(187)	→	188
3₁(24)	→	25
3₁(188)	→	189
3₁(420)	→	421
3₁(63)	→	64
3₁(115)	→	116
3₁(74)	→	75
3₁(177)	→	178
3₁(110)	→	111
3₁(50)	→	51
3₁(415)	→	416
3₁(137)	→	138
3₁(203)	→	204
3₁(229)	→	230
3₁(270)	→	271
3₁(138)	→	139
3₁(336)	→	337
3₁(471)	→	472
3₁(57)	→	58
3₁(56)	→	57
3₁(85)	→	86
3₁(114)	→	115
3₁(86)	→	87
3₁(136)	→	137
3₁(75)	→	76
3₁(335)	→	336
3₁(135)	→	136
3₁(412)	→	413
3₁(33)	→	34
3₁(101)	→	102
3₁(445)	→	446
3₁(83)	→	84
3₁(81)	→	82
3₁(416)	→	417
3₁(113)	→	114
3₂(515)	→	516
3₂(568)	→	569
3₂(509)	→	510
3₂(507)	→	508
3₂(504)	→	505
3₂(490)	→	491
3₂(534)	→	535
3₂(491)	→	492
3₂(497)	→	498
3₂(508)	→	509
2₀(7)	→	7
2₂(506)	→	507
2₂(505)	→	506
2₂(535)	→	536
2₂(536)	→	537

The automaton is closed under rewriting as it is compatible.