Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4970)

The rewrite relation of the following TRS is considered.

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

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

5(5(x1))	→	1(2(5(4(5(2(0(4(5(0(x1))))))))))	(22)
5(5(x1))	→	4(0(4(4(1(1(1(1(4(3(x1))))))))))	(23)
5(5(2(x1)))	→	2(1(1(0(0(4(4(5(2(4(x1))))))))))	(24)
4(2(5(x1)))	→	2(4(2(4(3(3(2(0(5(0(x1))))))))))	(25)
2(5(5(x1)))	→	3(5(2(3(0(3(2(3(1(0(x1))))))))))	(26)
3(5(5(x1)))	→	0(5(1(0(1(4(4(5(3(0(x1))))))))))	(27)
5(5(5(x1)))	→	0(0(5(4(1(0(1(4(3(5(x1))))))))))	(28)
4(0(5(2(x1))))	→	0(0(1(5(4(4(2(3(4(4(x1))))))))))	(29)
4(2(5(4(x1))))	→	3(3(1(3(0(2(5(5(1(4(x1))))))))))	(30)
5(5(5(4(x1))))	→	5(0(1(2(3(0(2(1(5(1(x1))))))))))	(31)
4(3(5(2(0(x1)))))	→	4(3(1(1(5(1(3(4(2(3(x1))))))))))	(32)
4(3(5(5(2(x1)))))	→	4(4(2(0(4(1(3(4(5(4(x1))))))))))	(33)
4(1(5(5(5(x1)))))	→	0(4(4(3(4(0(5(0(3(3(x1))))))))))	(34)
5(5(5(4(4(0(x1))))))	→	1(3(1(4(3(3(4(4(4(0(x1))))))))))	(35)
4(2(5(4(2(1(x1))))))	→	3(1(3(0(4(0(3(5(3(3(x1))))))))))	(36)
4(0(5(5(1(4(x1))))))	→	4(3(4(4(2(4(0(3(0(1(x1))))))))))	(37)
5(1(5(5(2(4(x1))))))	→	5(2(4(3(1(1(2(4(3(2(x1))))))))))	(38)
4(0(5(5(2(5(x1))))))	→	4(4(1(2(5(3(3(2(4(0(x1))))))))))	(39)
0(5(4(2(5(5(x1))))))	→	0(2(4(0(4(2(4(1(1(2(x1))))))))))	(40)
5(3(5(5(5(1(0(x1)))))))	→	5(0(2(1(0(1(5(2(3(5(x1))))))))))	(41)
2(2(4(2(5(4(4(x1)))))))	→	1(2(2(1(5(4(5(5(0(4(x1))))))))))	(42)

1.1 Bounds

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

final states:

{7}

transitions:

503	→	103
33	→	524
871	→	31
221	→	248
869	→	794
733	→	133
958	→	147
964	→	208
32	→	284
32	→	123
32	→	7
32	→	111
32	→	156
32	→	46
731	→	965
29	→	7
29	→	102
29	→	248
29	→	221
29	→	978
263	→	140
87	→	7
87	→	178
87	→	103
87	→	147
87	→	31
87	→	102
87	→	284
87	→	123
87	→	188
87	→	111
87	→	156
87	→	46
87	→	187
87	→	68
87	→	78
87	→	20
87	→	956
87	→	978
732	→	883
732	→	894
103	→	257
794	→	102
897	→	69
229	→	141
882	→	798
956	→	147
391	→	126
668	→	28
133	→	208
133	→	805
133	→	848
133	→	870
133	→	971
227	→	724
978	→	102
815	→	591
815	→	102
815	→	978
39	→	648
39	→	736
772	→	62
817	→	925
980	→	102
907	→	592
134	→	590
134	→	220
134	→	101
134	→	30
134	→	19
134	→	45
134	→	132
134	→	7
134	→	102
134	→	978
209	→	827
209	→	896
209	→	969
110	→	86
319	→	466
55	→	7
55	→	102
55	→	284
55	→	123
55	→	111
55	→	156
55	→	46
55	→	978
20	→	68
20	→	78
20	→	187
20	→	220
20	→	101
20	→	30
20	→	19
20	→	45
20	→	132
20	→	7
62	→	734
31	→	147
31	→	178
31	→	951
968	→	222
40	→	7
40	→	102
40	→	104
40	→	284
40	→	123
40	→	111
40	→	156
40	→	46
40	→	32
40	→	188
40	→	978
826	→	794
936	→	284
936	→	123
936	→	188
936	→	111
936	→	156
936	→	46
316	→	957
316	→	979
895	→	46
334	→	494
334	→	917
884	→	927
884	→	959
723	→	178
402	→	102
402	→	591
402	→	978
970	→	230
796	→	837
796	→	872
179	→	200
423	→	46
735	→	725
343	→	102
343	→	591
343	→	978
38	→	973
86	→	661
86	→	793
920	→	80
924	→	495
21	→	56
186	→	86
141	→	316
141	→	333
141	→	359
141	→	392
141	→	765
207	→	76
918	→	899
597	→	284
597	→	123
597	→	7
597	→	111
597	→	156
597	→	46
302	→	287
54	→	422
124	→	318
124	→	381
525	→	106
717	→	104
53	→	720
803	→	961
804	→	248
804	→	220
804	→	101
804	→	30
804	→	19
804	→	45
804	→	132
804	→	7
804	→	221
28	→	722
118	→	109
188	→	230
425	→	542
425	→	708
972	→	248
63	→	54
85	→	816
85	→	859
77	→	7
77	→	221
77	→	284
77	→	123
77	→	111
77	→	156
77	→	46
236	→	163
7	→	19
7	→	30
7	→	45
7	→	101
7	→	132
7	→	220
113	→	718
806	→	898
806	→	923
960	→	709
962	→	178
719	→	192
46	→	111
46	→	123
46	→	156
46	→	284
434	→	102
434	→	591
434	→	978
847	→	798
828	→	21
893	→	591
893	→	102
893	→	978
256	→	86
952	→	133
360	→	31
164	→	39
164	→	795
926	→	495
148	→	967
858	→	591
858	→	102
858	→	978
215	→	154
974	→	102
285	→	292
285	→	348
142	→	7
142	→	102
142	→	134
142	→	978
131	→	76
649	→	133
358	→	287
195	→	28
19	→	955
19	→	977
328	→	126
210	→	919
317	→	20
551	→	188
551	→	284
551	→	123
551	→	111
551	→	156
551	→	46
966	→	221
163	→	963
737	→	725
721	→	178
475	→	127
155	→	39
228	→	407
228	→	424
291	→	27
408	→	46
4₁(36)	→	37
4₁(187)	→	188
4₁(45)	→	46
4₁(192)	→	193
4₁(160)	→	161
4₁(103)	→	104
4₁(798)	→	799
4₁(49)	→	50
4₁(60)	→	61
4₁(62)	→	63
4₁(422)	→	423
4₁(214)	→	215
4₁(114)	→	115
4₁(111)	→	112
4₁(407)	→	408
4₁(157)	→	158
4₁(81)	→	82
4₁(107)	→	108
4₁(252)	→	253
4₁(25)	→	26
4₁(731)	→	732
4₁(80)	→	81
4₁(188)	→	189
4₁(213)	→	214
4₁(203)	→	204
4₁(37)	→	38
4₁(163)	→	164
4₁(184)	→	185
4₁(115)	→	116
4₁(768)	→	769
4₁(894)	→	895
4₁(770)	→	771
4₁(250)	→	251
4₁(31)	→	32
4₁(39)	→	40
4₁(189)	→	190
4₁(726)	→	727
4₁(969)	→	970
4₁(185)	→	186
4₁(182)	→	183
4₁(287)	→	288
4₁(148)	→	149
4₁(254)	→	255
4₁(21)	→	22
4₁(211)	→	212
4₁(222)	→	223
4₁(663)	→	664
4₁(227)	→	228
4₁(48)	→	49
3₂(392)	→	393
3₂(543)	→	544
3₂(923)	→	924
3₂(903)	→	904
3₂(901)	→	902
3₂(928)	→	929
3₂(710)	→	711
3₂(494)	→	495
3₂(474)	→	475
3₂(471)	→	472
3₂(925)	→	926
3₂(872)	→	873
3₂(467)	→	468
3₂(348)	→	349
3₂(859)	→	860
3₂(469)	→	470
3₂(848)	→	849
3₂(906)	→	907
3₂(381)	→	382
3₂(899)	→	900
4₂(715)	→	716
4₂(496)	→	497
4₂(354)	→	355
4₂(349)	→	350
4₂(855)	→	856
4₂(545)	→	546
4₂(849)	→	850
4₂(388)	→	389
4₂(324)	→	325
4₂(390)	→	391
4₂(546)	→	547
4₂(873)	→	874
4₂(927)	→	928
4₂(879)	→	880
4₂(887)	→	888
4₂(839)	→	840
4₂(868)	→	869
4₂(886)	→	887
4₂(854)	→	855
4₂(393)	→	394
4₂(857)	→	858
4₂(335)	→	336
4₂(355)	→	356
4₂(807)	→	808
4₂(401)	→	402
4₂(712)	→	713
4₂(866)	→	867
4₂(298)	→	299
4₂(428)	→	429
4₂(339)	→	340
4₂(497)	→	498
4₂(860)	→	861
4₂(931)	→	932
4₂(865)	→	866
4₂(542)	→	543
4₂(709)	→	710
4₂(424)	→	425
4₂(320)	→	321
4₂(843)	→	844
4₂(399)	→	400
4₂(822)	→	823
4₂(716)	→	717
4₂(818)	→	819
4₂(811)	→	812
4₂(357)	→	358
4₂(294)	→	295
4₂(382)	→	383
4₂(398)	→	399
4₂(881)	→	882
4₂(930)	→	931
4₂(427)	→	428
4₂(883)	→	884
4₂(878)	→	879
4₂(387)	→	388
2₂(326)	→	327
2₂(433)	→	434
2₂(544)	→	545
2₂(341)	→	342
2₂(468)	→	469
2₂(472)	→	473
2₂(884)	→	885
2₂(904)	→	905
2₂(337)	→	338
2₂(841)	→	842
2₂(425)	→	426
2₂(845)	→	846
2₂(809)	→	810
2₂(300)	→	301
2₂(820)	→	821
2₂(714)	→	715
2₂(322)	→	323
2₂(900)	→	901
2₂(824)	→	825
2₂(296)	→	297
2₂(892)	→	893
2₂(929)	→	930
2₂(813)	→	814
3₁(870)	→	871
3₁(128)	→	129
3₁(957)	→	958
3₁(112)	→	113
3₁(961)	→	962
3₁(221)	→	222
3₁(58)	→	59
3₁(102)	→	103
3₁(178)	→	179
3₁(183)	→	184
3₁(137)	→	138
3₁(201)	→	202
3₁(154)	→	155
3₁(158)	→	159
3₁(78)	→	79
3₁(71)	→	72
3₁(967)	→	968
3₁(69)	→	70
3₁(194)	→	195
3₁(191)	→	192
3₁(593)	→	594
3₁(73)	→	74
3₁(661)	→	662
3₁(232)	→	233
3₁(730)	→	731
3₁(718)	→	719
3₁(130)	→	131
3₁(720)	→	721
3₁(76)	→	77
3₁(359)	→	360
3₁(596)	→	597
3₁(595)	→	596
3₁(955)	→	956
3₁(209)	→	210
3₁(30)	→	31
3₁(59)	→	60
3₁(226)	→	227
3₁(190)	→	191
3₁(205)	→	206
3₁(725)	→	726
3₁(149)	→	150
3₁(231)	→	232
3₁(722)	→	723
3₁(664)	→	665
0₀(7)	→	7
3₀(7)	→	7
5₂(812)	→	813
5₂(325)	→	326
5₂(293)	→	294
5₂(932)	→	933
5₂(501)	→	502
5₂(426)	→	427
5₂(838)	→	839
5₂(299)	→	300
5₂(810)	→	811
5₂(842)	→	843
5₂(708)	→	709
5₂(323)	→	324
5₂(338)	→	339
5₂(905)	→	906
5₂(297)	→	298
5₂(340)	→	341
5₂(844)	→	845
5₂(823)	→	824
5₂(821)	→	822
5₂(319)	→	320
5₂(547)	→	548
5₂(495)	→	496
5₂(959)	→	960
5₂(473)	→	474
5₂(334)	→	335
5₂(817)	→	818
5₂(806)	→	807
5₂(885)	→	886
4₀(7)	→	7
1₁(106)	→	107
1₁(132)	→	133
1₁(82)	→	83
1₁(800)	→	801
1₁(667)	→	668
1₁(123)	→	124
1₁(153)	→	154
1₁(594)	→	595
1₁(53)	→	54
1₁(129)	→	130
1₁(117)	→	118
1₁(152)	→	153
1₁(728)	→	729
1₁(896)	→	897
1₁(28)	→	29
1₁(84)	→	85
1₁(248)	→	249
1₁(139)	→	140
1₁(803)	→	804
1₁(235)	→	236
1₁(249)	→	250
1₁(52)	→	53
1₁(951)	→	952
1₁(193)	→	194
1₁(159)	→	160
1₁(289)	→	290
1₁(729)	→	730
1₁(35)	→	36
1₁(665)	→	666
1₁(206)	→	207
1₁(261)	→	262
1₁(648)	→	649
1₁(224)	→	225
1₁(34)	→	35
1₁(150)	→	151
1₁(32)	→	33
1₁(963)	→	964
1₁(134)	→	135
1₁(33)	→	34
1₁(68)	→	69
1₁(767)	→	768
1₁(259)	→	260
1₁(104)	→	105
1₁(225)	→	226
1₁(766)	→	767
2₁(138)	→	139
2₁(70)	→	71
2₁(262)	→	263
2₁(765)	→	766
2₁(147)	→	148
2₁(135)	→	136
2₁(290)	→	291
2₁(230)	→	231
2₁(732)	→	733
2₁(802)	→	803
2₁(54)	→	55
2₁(61)	→	62
2₁(46)	→	47
2₁(736)	→	737
2₁(23)	→	24
2₁(251)	→	252
2₁(591)	→	592
2₁(126)	→	127
2₁(212)	→	213
2₁(734)	→	735
2₁(724)	→	725
2₁(727)	→	728
2₁(74)	→	75
2₁(769)	→	770
2₁(162)	→	163
2₁(113)	→	114
2₁(228)	→	229
2₁(965)	→	966
2₁(27)	→	28
2₁(255)	→	256
2₁(971)	→	972
2₁(801)	→	802
2₁(662)	→	663
2₁(234)	→	235
2₁(223)	→	224
2₁(57)	→	58
2₁(257)	→	258
2₁(220)	→	221
1₀(7)	→	7
2₀(7)	→	7
0₁(136)	→	137
0₁(72)	→	73
0₁(179)	→	180
0₁(127)	→	128
0₁(771)	→	772
0₁(22)	→	23
0₁(161)	→	162
0₁(105)	→	106
0₁(592)	→	593
0₁(109)	→	110
0₁(38)	→	39
0₁(83)	→	84
0₁(181)	→	182
0₁(795)	→	796
0₁(316)	→	317
0₁(202)	→	203
0₁(56)	→	57
0₁(284)	→	285
0₁(253)	→	254
0₁(208)	→	209
0₁(19)	→	20
0₁(50)	→	51
0₁(204)	→	205
0₁(524)	→	525
0₁(51)	→	52
0₁(140)	→	141
0₁(86)	→	87
0₁(260)	→	261
0₁(210)	→	211
5₁(666)	→	667
5₁(285)	→	286
5₁(26)	→	27
5₁(24)	→	25
5₁(180)	→	181
5₁(116)	→	117
5₁(793)	→	794
5₁(979)	→	980
5₁(124)	→	125
5₁(796)	→	797
5₁(827)	→	828
5₁(47)	→	48
5₁(919)	→	920
5₁(156)	→	157
5₁(799)	→	800
5₁(85)	→	86
5₁(125)	→	126
5₁(258)	→	259
5₁(977)	→	978
5₁(141)	→	142
5₁(79)	→	80
5₁(233)	→	234
5₁(75)	→	76
5₁(286)	→	287
5₁(151)	→	152
5₁(590)	→	591
5₁(133)	→	134
5₁(797)	→	798
5₁(20)	→	21
5₁(101)	→	102
5₁(288)	→	289
5₁(200)	→	201
5₁(973)	→	974
5₁(108)	→	109
1₂(397)	→	398
1₂(383)	→	384
1₂(891)	→	892
1₂(864)	→	865
1₂(846)	→	847
1₂(851)	→	852
1₂(431)	→	432
1₂(875)	→	876
1₂(861)	→	862
1₂(862)	→	863
1₂(711)	→	712
1₂(814)	→	815
1₂(933)	→	934
1₂(498)	→	499
1₂(352)	→	353
1₂(466)	→	467
1₂(825)	→	826
1₂(898)	→	899
1₂(327)	→	328
1₂(850)	→	851
1₂(386)	→	387
1₂(384)	→	385
1₂(853)	→	854
1₂(876)	→	877
1₂(385)	→	386
1₂(342)	→	343
1₂(395)	→	396
1₂(917)	→	918
1₂(500)	→	501
1₂(874)	→	875
1₂(301)	→	302
1₂(863)	→	864
1₂(890)	→	891
1₂(394)	→	395
1₂(877)	→	878
1₂(353)	→	354
1₂(351)	→	352
1₂(396)	→	397
1₂(852)	→	853
1₂(548)	→	549
1₂(350)	→	351
1₂(432)	→	433
5₀(7)	→	7
0₂(333)	→	334
0₂(295)	→	296
0₂(805)	→	806
0₂(549)	→	550
0₂(389)	→	390
0₂(356)	→	357
0₂(935)	→	936
0₂(808)	→	809
0₂(934)	→	935
0₂(550)	→	551
0₂(819)	→	820
0₂(321)	→	322
0₂(837)	→	838
0₂(400)	→	401
0₂(888)	→	889
0₂(840)	→	841
0₂(889)	→	890
0₂(429)	→	430
0₂(816)	→	817
0₂(502)	→	503
0₂(430)	→	431
0₂(880)	→	881
0₂(902)	→	903
0₂(713)	→	714
0₂(867)	→	868
0₂(499)	→	500
0₂(292)	→	293
0₂(470)	→	471
0₂(336)	→	337
0₂(318)	→	319
0₂(856)	→	857

The automaton is closed under rewriting as it is compatible.