Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96563)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

3(2(1(0(x1))))	→	3(2(2(0(x1))))	(26)
5(4(4(1(1(x1)))))	→	5(0(0(1(5(x1)))))	(27)
5(2(3(3(2(x1)))))	→	5(5(4(5(3(x1)))))	(28)
3(5(1(1(5(x1)))))	→	3(5(4(1(5(x1)))))	(29)
4(1(1(5(2(0(x1))))))	→	5(4(2(2(3(0(x1))))))	(30)
3(0(4(1(2(1(x1))))))	→	3(5(4(5(2(4(x1))))))	(31)
3(4(0(2(5(1(x1))))))	→	1(1(1(0(5(x1)))))	(32)
0(4(5(1(2(2(x1))))))	→	3(0(4(5(3(2(x1))))))	(33)
4(4(1(3(2(0(4(x1)))))))	→	5(0(5(0(3(1(4(x1)))))))	(34)
2(2(2(3(4(5(3(4(x1))))))))	→	4(1(4(3(2(1(4(x1)))))))	(35)
3(3(3(4(3(2(2(2(0(x1)))))))))	→	3(5(5(3(5(0(4(5(0(x1)))))))))	(36)
2(5(0(1(1(4(3(5(4(x1)))))))))	→	2(5(0(2(3(1(3(4(4(x1)))))))))	(37)
2(5(1(5(4(0(1(4(3(3(x1))))))))))	→	4(2(0(3(0(5(1(4(3(3(x1))))))))))	(38)
2(4(1(2(1(5(5(0(4(5(4(2(x1))))))))))))	→	2(4(1(0(3(3(1(1(0(1(4(x1)))))))))))	(39)
0(4(5(1(5(4(3(4(5(4(0(0(1(x1)))))))))))))	→	3(1(3(0(1(1(2(1(3(3(5(x1)))))))))))	(40)
2(3(0(0(4(4(2(3(2(1(2(2(1(x1)))))))))))))	→	5(4(2(2(1(3(1(0(2(3(4(4(4(x1)))))))))))))	(41)
0(2(0(2(1(3(3(3(5(4(5(1(4(x1)))))))))))))	→	5(1(1(3(1(0(4(4(3(4(1(4(x1))))))))))))	(42)
1(3(0(1(5(5(5(0(5(2(0(2(0(3(3(2(2(x1)))))))))))))))))	→	1(3(3(4(1(2(3(4(0(0(5(2(0(2(5(5(5(x1)))))))))))))))))	(43)
2(5(2(5(1(5(1(1(3(3(3(3(0(3(1(1(5(1(x1))))))))))))))))))	→	2(5(1(4(2(5(2(1(1(4(3(1(5(0(2(4(5(3(x1))))))))))))))))))	(44)
0(3(3(0(3(2(0(4(0(4(5(3(2(4(3(3(4(2(x1))))))))))))))))))	→	5(1(0(5(0(3(0(1(2(5(1(4(4(0(3(1(2(x1)))))))))))))))))	(45)
2(3(1(0(1(3(3(0(0(3(0(5(3(2(1(5(5(2(x1))))))))))))))))))	→	3(3(4(0(5(0(1(3(2(2(2(5(1(0(0(5(1(2(x1))))))))))))))))))	(46)
2(4(1(3(0(4(5(4(2(2(0(5(0(0(3(1(5(3(2(x1)))))))))))))))))))	→	2(1(5(5(3(1(4(2(2(5(3(2(3(0(2(0(2(5(x1))))))))))))))))))	(47)
4(5(4(4(1(5(0(4(3(2(1(0(5(5(2(1(4(3(2(3(x1))))))))))))))))))))	→	4(2(2(5(2(4(2(0(3(2(1(5(5(1(0(5(1(0(2(3(x1))))))))))))))))))))	(48)
3(2(2(0(1(2(1(2(5(3(0(5(5(4(4(0(2(5(5(3(x1))))))))))))))))))))	→	3(4(2(5(4(3(0(5(3(2(1(4(2(4(5(0(3(3(1(3(x1))))))))))))))))))))	(49)
4(0(1(5(4(4(2(1(2(0(5(3(5(5(1(3(5(4(1(5(4(x1)))))))))))))))))))))	→	4(5(3(0(2(2(5(5(3(2(2(5(4(0(2(5(1(2(0(4(4(x1)))))))))))))))))))))	(50)

1.1 Bounds

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

final states:

{7}

transitions:

730	→	155
23	→	7
23	→	240
23	→	132
23	→	57
23	→	164
23	→	19
23	→	94
23	→	72
23	→	46
23	→	95
23	→	63
23	→	42
23	→	262
23	→	87
23	→	40
23	→	14
23	→	263
23	→	743
239	→	16
200	→	224
200	→	723
200	→	729
61	→	7
61	→	279
61	→	110
61	→	261
61	→	29
61	→	280
61	→	650
61	→	657
102	→	7
102	→	63
102	→	241
102	→	47
102	→	741
32	→	22
29	→	110
29	→	261
29	→	279
29	→	725
685	→	200
745	→	280
202	→	721
732	→	164
732	→	740
734	→	29
15	→	391
15	→	693
15	→	742
743	→	263
655	→	649
655	→	701
728	→	119
149	→	41
659	→	72
466	→	748
466	→	761
638	→	199
638	→	62
638	→	28
638	→	13
638	→	18
638	→	45
638	→	7
638	→	63
469	→	279
469	→	110
469	→	62
469	→	28
469	→	13
469	→	18
469	→	45
469	→	7
469	→	261
469	→	29
469	→	650
469	→	657
653	→	21
213	→	162
347	→	342
347	→	476
347	→	666
95	→	142
95	→	302
95	→	727
59	→	341
34	→	648
255	→	432
696	→	241
749	→	57
20	→	33
467	→	709
467	→	757
31	→	185
31	→	579
631	→	73
127	→	101
667	→	133
101	→	393
101	→	662
101	→	678
477	→	466
392	→	29
60	→	346
60	→	434
60	→	682
197	→	464
747	→	303
44	→	22
44	→	654
73	→	77
73	→	119
73	→	154
179	→	60
687	→	200
76	→	21
297	→	16
297	→	632
296	→	684
675	→	165
702	→	303
141	→	16
679	→	164
679	→	695
726	→	112
468	→	711
468	→	719
468	→	733
345	→	18
88	→	674
741	→	241
394	→	29
433	→	46
67	→	16
657	→	650
657	→	717
82	→	7
82	→	630
82	→	199
82	→	63
82	→	241
82	→	94
82	→	72
82	→	46
82	→	741
117	→	660
118	→	81
118	→	686
14	→	40
14	→	87
93	→	34
63	→	199
581	→	87
581	→	7
581	→	40
581	→	14
581	→	744
581	→	303
581	→	747
720	→	46
736	→	200
7	→	13
7	→	18
7	→	28
7	→	45
7	→	62
663	→	72
694	→	101
758	→	29
710	→	19
724	→	78
42	→	658
681	→	29
46	→	72
46	→	94
46	→	656
46	→	731
46	→	746
162	→	474
162	→	680
35	→	16
278	→	117
256	→	101
48	→	33
198	→	100
17	→	7
17	→	279
17	→	110
17	→	64
17	→	261
17	→	29
17	→	133
17	→	41
17	→	87
17	→	40
17	→	14
17	→	111
17	→	63
17	→	262
17	→	303
17	→	747
47	→	7
47	→	735
683	→	29
718	→	30
712	→	19
762	→	29
320	→	81
722	→	21
19	→	57
19	→	132
19	→	164
19	→	240
19	→	7
19	→	740
19	→	732
163	→	22
475	→	465
661	→	72
435	→	46
0₁(57)	→	58
0₁(99)	→	100
0₁(226)	→	227
0₁(186)	→	187
0₁(579)	→	580
0₁(145)	→	146
0₁(210)	→	211
0₁(74)	→	75
0₁(234)	→	235
0₁(291)	→	292
0₁(265)	→	266
0₁(208)	→	209
0₁(170)	→	171
0₁(119)	→	120
0₁(344)	→	345
0₁(124)	→	125
0₁(158)	→	159
0₁(167)	→	168
0₁(236)	→	237
0₁(282)	→	283
0₁(243)	→	244
0₁(114)	→	115
0₁(476)	→	477
0₁(212)	→	213
0₁(66)	→	67
0₁(262)	→	263
0₁(138)	→	139
0₁(465)	→	466
0₁(13)	→	14
0₁(89)	→	90
0₁(317)	→	318
0₁(241)	→	242
0₁(307)	→	308
0₁(116)	→	117
0₁(171)	→	172
0₁(225)	→	226
0₁(746)	→	747
0₁(20)	→	21
0₁(701)	→	702
0₁(201)	→	202
0₁(302)	→	303
0₁(742)	→	743
0₁(272)	→	273
0₁(21)	→	22
0₁(343)	→	344
1₁(192)	→	193
1₁(134)	→	135
1₁(727)	→	728
1₁(159)	→	160
1₁(269)	→	270
1₁(112)	→	113
1₁(467)	→	468
1₁(148)	→	149
1₁(140)	→	141
1₁(204)	→	205
1₁(650)	→	651
1₁(263)	→	264
1₁(58)	→	59
1₁(162)	→	163
1₁(255)	→	256
1₁(137)	→	138
1₁(161)	→	162
1₁(287)	→	288
1₁(227)	→	228
1₁(175)	→	176
1₁(207)	→	208
1₁(468)	→	469
1₁(121)	→	122
1₁(191)	→	192
1₁(279)	→	280
1₁(686)	→	687
1₁(72)	→	73
1₁(342)	→	343
1₁(251)	→	252
1₁(630)	→	631
1₁(266)	→	267
1₁(125)	→	126
1₁(197)	→	198
1₁(96)	→	97
1₁(146)	→	147
1₁(744)	→	745
1₁(304)	→	305
1₁(188)	→	189
1₁(632)	→	633
1₁(466)	→	467
1₁(80)	→	81
1₁(636)	→	637
1₁(136)	→	137
1₁(19)	→	20
1₁(233)	→	234
1₁(59)	→	60
1₁(735)	→	736
1₁(199)	→	200
1₁(60)	→	61
1₁(684)	→	685
1₁(120)	→	121
5₀(7)	→	7
4₀(7)	→	7
0₀(7)	→	7
4₁(286)	→	287
4₁(432)	→	433
4₁(296)	→	297
4₁(142)	→	143
4₁(293)	→	294
4₁(203)	→	204
4₁(172)	→	173
4₁(88)	→	89
4₁(237)	→	238
4₁(94)	→	95
4₁(202)	→	203
4₁(157)	→	158
4₁(196)	→	197
4₁(43)	→	44
4₁(284)	→	285
4₁(658)	→	659
4₁(660)	→	661
4₁(156)	→	157
4₁(154)	→	155
4₁(729)	→	730
4₁(30)	→	31
4₁(308)	→	309
4₁(648)	→	649
4₁(65)	→	66
4₁(274)	→	275
4₁(190)	→	191
4₁(81)	→	82
4₁(176)	→	177
4₁(250)	→	251
4₁(662)	→	663
4₁(79)	→	80
4₁(126)	→	127
4₁(45)	→	46
4₁(33)	→	34
4₁(637)	→	638
4₁(111)	→	112
4₁(725)	→	726
4₁(434)	→	435
4₁(635)	→	636
4₁(654)	→	655
4₁(719)	→	720
5₁(224)	→	225
5₁(267)	→	268
5₁(64)	→	65
5₁(235)	→	236
5₁(90)	→	91
5₁(474)	→	475
5₁(31)	→	32
5₁(674)	→	675
5₁(290)	→	291
5₁(87)	→	88
5₁(748)	→	749
5₁(717)	→	718
5₁(305)	→	306
5₁(247)	→	248
5₁(18)	→	19
5₁(464)	→	465
5₁(709)	→	710
5₁(268)	→	269
5₁(205)	→	206
5₁(253)	→	254
5₁(34)	→	35
5₁(169)	→	170
5₁(341)	→	342
5₁(92)	→	93
5₁(211)	→	212
5₁(22)	→	23
5₁(194)	→	195
5₁(165)	→	166
5₁(731)	→	732
5₁(314)	→	315
5₁(711)	→	712
5₁(113)	→	114
5₁(228)	→	229
5₁(75)	→	76
5₁(693)	→	694
5₁(721)	→	722
5₁(264)	→	265
5₁(29)	→	30
5₁(319)	→	320
5₁(164)	→	165
5₁(276)	→	277
5₁(346)	→	347
5₁(47)	→	48
5₁(294)	→	295
5₁(313)	→	314
5₁(187)	→	188
5₁(254)	→	255
5₁(100)	→	101
5₁(678)	→	679
5₁(283)	→	284
5₁(309)	→	310
2₀(7)	→	7
1₀(7)	→	7
2₁(101)	→	102
2₁(166)	→	167
2₁(98)	→	99
2₁(277)	→	278
2₁(652)	→	653
2₁(117)	→	118
2₁(15)	→	16
2₁(144)	→	145
2₁(306)	→	307
2₁(695)	→	696
2₁(41)	→	42
2₁(206)	→	207
2₁(248)	→	249
2₁(249)	→	250
2₁(77)	→	78
2₁(62)	→	63
2₁(193)	→	194
2₁(288)	→	289
2₁(229)	→	230
2₁(245)	→	246
2₁(168)	→	169
2₁(230)	→	231
2₁(316)	→	317
2₁(135)	→	136
2₁(261)	→	262
2₁(740)	→	741
2₁(242)	→	243
2₁(14)	→	15
2₁(46)	→	47
2₁(295)	→	296
2₁(310)	→	311
2₁(315)	→	316
2₁(240)	→	241
2₁(723)	→	724
2₁(273)	→	274
2₁(303)	→	304
2₁(270)	→	271
2₁(285)	→	286
2₁(633)	→	634
2₁(195)	→	196
2₁(231)	→	232
2₁(185)	→	186
2₁(275)	→	276
2₁(42)	→	43
2₁(311)	→	312
2₁(174)	→	175
3₁(666)	→	667
3₁(160)	→	161
3₁(232)	→	233
3₁(147)	→	148
3₁(318)	→	319
3₁(271)	→	272
3₁(123)	→	124
3₁(16)	→	17
3₁(40)	→	41
3₁(246)	→	247
3₁(244)	→	245
3₁(63)	→	64
3₁(115)	→	116
3₁(649)	→	650
3₁(177)	→	178
3₁(110)	→	111
3₁(580)	→	581
3₁(122)	→	123
3₁(252)	→	253
3₁(682)	→	683
3₁(97)	→	98
3₁(178)	→	179
3₁(73)	→	74
3₁(680)	→	681
3₁(289)	→	290
3₁(391)	→	392
3₁(393)	→	394
3₁(173)	→	174
3₁(28)	→	29
3₁(292)	→	293
3₁(656)	→	657
3₁(733)	→	734
3₁(91)	→	92
3₁(155)	→	156
3₁(757)	→	758
3₁(139)	→	140
3₁(312)	→	313
3₁(132)	→	133
3₁(209)	→	210
3₁(281)	→	282
3₁(133)	→	134
3₁(651)	→	652
3₁(761)	→	762
3₁(143)	→	144
3₁(200)	→	201
3₁(280)	→	281
3₁(634)	→	635
3₁(95)	→	96
3₁(238)	→	239
3₁(78)	→	79
3₁(189)	→	190
3₀(7)	→	7

The automaton is closed under rewriting as it is compatible.