Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3450)

The rewrite relation of the following TRS is considered.

0(5(3(x1)))	→	3(0(4(3(0(4(1(4(4(4(x1))))))))))	(1)
1(3(4(x1)))	→	0(4(3(5(5(1(0(3(4(4(x1))))))))))	(2)
4(5(3(x1)))	→	3(4(3(2(2(3(0(3(3(4(x1))))))))))	(3)
1(5(3(1(x1))))	→	2(1(0(1(1(1(5(1(1(2(x1))))))))))	(4)
3(0(0(5(x1))))	→	4(2(0(2(1(2(4(0(3(5(x1))))))))))	(5)
4(1(3(5(x1))))	→	3(0(3(4(4(2(5(5(2(2(x1))))))))))	(6)
0(0(4(5(1(x1)))))	→	0(3(5(2(2(0(0(3(2(1(x1))))))))))	(7)
0(1(0(2(5(x1)))))	→	1(0(3(0(2(3(1(1(5(2(x1))))))))))	(8)
0(1(4(5(4(x1)))))	→	1(0(3(3(1(0(2(3(1(4(x1))))))))))	(9)
1(0(5(4(0(x1)))))	→	1(1(2(0(4(0(0(3(1(0(x1))))))))))	(10)
1(5(3(5(4(x1)))))	→	2(0(2(1(4(4(1(0(1(4(x1))))))))))	(11)
3(5(0(5(3(x1)))))	→	3(2(2(2(0(0(2(2(0(4(x1))))))))))	(12)
4(5(3(1(3(x1)))))	→	2(0(3(5(5(5(0(2(4(3(x1))))))))))	(13)
4(5(3(3(5(x1)))))	→	3(3(4(1(0(1(5(2(5(5(x1))))))))))	(14)
4(5(4(5(3(x1)))))	→	2(3(0(3(3(4(1(5(2(1(x1))))))))))	(15)
5(3(3(5(3(x1)))))	→	5(4(4(5(4(0(2(0(3(3(x1))))))))))	(16)
0(0(1(4(5(3(x1))))))	→	1(1(1(4(4(3(1(1(5(4(x1))))))))))	(17)
0(0(5(1(3(3(x1))))))	→	0(2(0(1(4(4(5(5(4(4(x1))))))))))	(18)
0(1(3(5(0(1(x1))))))	→	1(5(0(4(3(3(5(2(3(5(x1))))))))))	(19)
0(5(3(0(2(3(x1))))))	→	0(0(3(2(3(5(5(0(4(3(x1))))))))))	(20)
1(0(0(5(5(1(x1))))))	→	0(3(1(1(1(4(4(4(0(1(x1))))))))))	(21)
1(3(4(5(4(5(x1))))))	→	1(4(5(0(4(3(3(3(1(5(x1))))))))))	(22)
1(4(0(5(4(0(x1))))))	→	1(0(2(5(5(0(3(0(4(0(x1))))))))))	(23)
2(5(4(0(5(3(x1))))))	→	5(3(4(3(2(4(3(2(5(2(x1))))))))))	(24)
4(0(1(3(4(5(x1))))))	→	3(0(5(0(4(4(4(3(3(5(x1))))))))))	(25)
4(1(0(5(3(1(x1))))))	→	2(0(3(4(1(5(0(2(5(1(x1))))))))))	(26)
4(5(4(5(3(2(x1))))))	→	0(3(5(3(4(4(4(2(1(2(x1))))))))))	(27)
5(1(2(4(5(3(x1))))))	→	0(2(1(1(1(0(1(1(5(4(x1))))))))))	(28)
5(1(3(4(5(1(x1))))))	→	2(0(2(4(4(3(0(1(1(1(x1))))))))))	(29)
0(0(1(1(3(5(3(x1)))))))	→	1(2(1(5(1(3(0(3(5(3(x1))))))))))	(30)
0(1(4(0(5(2(4(x1)))))))	→	1(1(0(1(0(3(2(5(1(4(x1))))))))))	(31)
1(3(4(0(0(0(0(x1)))))))	→	0(1(0(2(3(2(4(3(3(3(x1))))))))))	(32)
1(4(0(0(5(3(5(x1)))))))	→	0(0(1(3(1(4(4(2(2(5(x1))))))))))	(33)
1(4(0(5(4(2(1(x1)))))))	→	0(0(1(5(4(3(3(3(3(5(x1))))))))))	(34)
1(5(1(5(0(5(1(x1)))))))	→	2(2(2(1(1(5(4(5(5(1(x1))))))))))	(35)
2(5(4(5(4(0(1(x1)))))))	→	5(3(0(4(5(0(4(4(3(1(x1))))))))))	(36)
3(1(0(5(3(5(3(x1)))))))	→	4(4(0(3(4(5(3(4(2(3(x1))))))))))	(37)
4(1(5(3(3(5(3(x1)))))))	→	3(1(3(1(1(5(4(3(4(2(x1))))))))))	(38)
4(5(3(5(1(2(5(x1)))))))	→	3(3(2(1(1(5(1(5(5(5(x1))))))))))	(39)
4(5(3(5(5(0(1(x1)))))))	→	4(3(2(2(0(2(2(4(5(1(x1))))))))))	(40)
5(0(0(0(0(0(5(x1)))))))	→	1(5(1(1(4(4(2(0(2(5(x1))))))))))	(41)
5(1(3(2(5(3(0(x1)))))))	→	5(0(4(3(5(1(3(3(1(0(x1))))))))))	(42)
5(1(4(2(4(5(3(x1)))))))	→	0(1(0(2(3(2(1(0(0(3(x1))))))))))	(43)
5(1(4(5(2(4(2(x1)))))))	→	2(5(0(1(5(1(5(2(0(2(x1))))))))))	(44)

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:

{6, 5, 4, 3, 2, 1}

transitions:

272	→	1425
1374	→	845
1374	→	252
1374	→	584
1374	→	326
1374	→	155
1374	→	86
1374	→	249
1374	→	457
1374	→	2
1374	→	783
1374	→	711
1374	→	755
1374	→	1968
1760	→	87
1206	→	1182
1243	→	201
279	→	125
871	→	1016
871	→	1234
871	→	1392
329	→	300
429	→	677
429	→	1597
869	→	613
733	→	1415
1940	→	201
818	→	809
917	→	9
917	→	1916
685	→	437
1459	→	785
128	→	297
128	→	387
128	→	817
128	→	901
128	→	1059
2046	→	16
202	→	632
202	→	703
589	→	838
589	→	1458
589	→	1496
1333	→	2007
1418	→	605
1418	→	1466
87	→	9
87	→	411
1697	→	1901
1156	→	752
855	→	1322
809	→	1328
809	→	1776
10	→	88
10	→	624
10	→	1205
1261	→	674
2062	→	128
734	→	2
734	→	845
734	→	252
734	→	783
734	→	711
734	→	755
734	→	1968
1694	→	2067
1694	→	2081
1966	→	201
915	→	9
1284	→	1492
1393	→	749
1431	→	2015
1237	→	9
886	→	1083
96	→	5
96	→	735
96	→	648
96	→	300
96	→	360
96	→	430
96	→	754
96	→	390
96	→	329
96	→	414
438	→	5
438	→	300
438	→	430
438	→	360
438	→	754
438	→	390
438	→	329
438	→	414
1209	→	1832
1209	→	1957
129	→	717
326	→	1840
326	→	1965
1841	→	128
1253	→	654
701	→	1033
701	→	1227
701	→	1599
2056	→	935
1849	→	128
2040	→	588
956	→	1717
1923	→	606
595	→	1236
595	→	1924
1249	→	640
299	→	1811
299	→	1945
878	→	733
878	→	1518
2082	→	605
585	→	531
676	→	437
2054	→	935
18	→	1
18	→	429
18	→	458
1395	→	749
815	→	980
815	→	1005
815	→	1180
3	→	63
3	→	198
3	→	269
3	→	359
3	→	439
3	→	558
583	→	531
1483	→	801
988	→	2023
1628	→	1614
1634	→	1751
1888	→	361
2080	→	506
460	→	429
460	→	1368
460	→	1631
1495	→	838
1812	→	128
1226	→	300
646	→	1411
347	→	300
861	→	1003
861	→	1238
298	→	272
919	→	9
1424	→	605
1467	→	793
9	→	117
9	→	413
9	→	506
9	→	615
1706	→	92
1706	→	1556
1706	→	865
647	→	308
5	→	8
5	→	176
5	→	251
5	→	344
5	→	459
5	→	530
209	→	1612
209	→	1711
95	→	1417
515	→	3
515	→	703
515	→	585
515	→	632
515	→	202
199	→	128
199	→	899
618	→	728
947	→	90
1295	→	1284
1082	→	460
1082	→	499
1082	→	649
1110	→	1085
1866	→	501
1866	→	615
1866	→	413
1866	→	117
1866	→	506
1866	→	9
1866	→	1175
1890	→	362
2018	→	605
942	→	1903
942	→	2009
1833	→	128
700	→	903
700	→	920
700	→	1225
700	→	1298
1416	→	605
1416	→	1464
1034	→	271
1034	→	1107
1034	→	1482
631	→	308
1493	→	809
1	→	39
1	→	127
1	→	229
1	→	299
1	→	481
1	→	541
1936	→	201
40	→	9
40	→	1203
1430	→	2017
1902	→	1129
542	→	531
877	→	1244
1884	→	271
1299	→	387
1299	→	1490
716	→	537
1489	→	803
1022	→	1696
1022	→	2047
2074	→	201
1112	→	361
1004	→	981
1267	→	1885
1267	→	1895
1626	→	1615
770	→	854
770	→	1207
777	→	95
1412	→	605
1323	→	714
1938	→	201
2024	→	201
505	→	136
1645	→	1737
390	→	498
390	→	754
1934	→	299
1934	→	1598
1213	→	1817
1213	→	1951
480	→	429
135	→	1456
1996	→	605
1208	→	591
606	→	761
606	→	1314
606	→	1555
1064	→	1856
1064	→	1883
179	→	128
179	→	271
179	→	361
612	→	1127
125	→	916
125	→	1211
125	→	1294
1137	→	499
1598	→	299
881	→	1540
816	→	125
816	→	1320
1643	→	1627
1643	→	429
1643	→	458
269	→	1873
1414	→	605
309	→	1
309	→	677
309	→	429
309	→	482
309	→	458
309	→	1598
1654	→	880
1654	→	429
1654	→	1322
1654	→	855
1654	→	480
1654	→	902
1982	→	201
1212	→	300
760	→	622
994	→	981
201	→	588
201	→	668
201	→	769
177	→	128
177	→	808
177	→	879
1799	→	128
1896	→	361
1917	→	533
702	→	6
702	→	854
702	→	901
702	→	387
702	→	128
702	→	156
702	→	770
702	→	1841
614	→	2
614	→	201
614	→	270
614	→	746
614	→	845
614	→	252
614	→	783
614	→	711
614	→	1940
614	→	1968
1214	→	300
251	→	1877
540	→	4
540	→	615
540	→	413
540	→	411
540	→	9
540	→	87
540	→	501
540	→	1175
1944	→	201
532	→	640
532	→	1480
844	→	595
346	→	1798
346	→	1941
1921	→	300
810	→	1488
1855	→	128
1984	→	506
639	→	369
6	→	41
6	→	178
6	→	200
6	→	346
6	→	479
6	→	556
302	→	1595
1235	→	1230
792	→	1138
792	→	1152
921	→	9
345	→	300
1397	→	757
308	→	1423
1818	→	128
1092	→	1854
1092	→	1937
431	→	863
1292	→	1871
1292	→	1922
1292	→	2045
124	→	933
1293	→	854
1293	→	901
1293	→	387
1293	→	128
1293	→	556
1293	→	346
1293	→	178
1293	→	41
1293	→	200
1293	→	479
1293	→	6
1293	→	156
1293	→	770
230	→	201
230	→	1516
613	→	1057
613	→	1146
1297	→	1284
270	→	201
270	→	86
270	→	249
270	→	457
270	→	584
270	→	326
270	→	155
270	→	2
776	→	1398
900	→	880
1146	→	1834
1146	→	1959
2010	→	605
437	→	991
437	→	1240
1596	→	876
853	→	4
853	→	615
853	→	413
853	→	411
853	→	9
853	→	87
301	→	597
2	→	86
2	→	155
2	→	249
2	→	326
2	→	457
2	→	584
1746	→	809
1746	→	42
1746	→	818
1175	→	501
2008	→	605
1950	→	201
979	→	804
4	→	65
4	→	157
4	→	231
4	→	328
4	→	428
4	→	582
232	→	201
1291	→	1644
1291	→	1659
1291	→	1920
1291	→	1989
118	→	946
344	→	1842
344	→	1967
604	→	539
604	→	1248
557	→	531
801	→	969
904	→	948
252	→	201
252	→	584
252	→	326
252	→	155
252	→	86
252	→	249
252	→	457
252	→	2
300	→	648
300	→	710
300	→	735
300	→	791
300	→	530
300	→	344
300	→	176
300	→	8
300	→	251
300	→	459
300	→	5
369	→	993
369	→	1242
1892	→	362
440	→	429
1108	→	1085
508	→	1625
1015	→	669
1015	→	617
66	→	9
66	→	389
359	→	1796
359	→	1939
704	→	778
1843	→	128
2048	→	507
862	→	2
862	→	769
862	→	588
862	→	201
862	→	230
862	→	1946
913	→	429
913	→	480
913	→	880
913	→	1322
913	→	855
913	→	902
481	→	1995
887	→	743
887	→	1494
1334	→	615
1334	→	413
1334	→	411
1334	→	4
1334	→	9
1334	→	87
1491	→	809
1872	→	271
1872	→	1889
1872	→	2025
623	→	369
1600	→	16
1835	→	128
1145	→	499
1145	→	677
1145	→	1
1145	→	429
1145	→	460
1145	→	649
12	→	1252
559	→	531
2038	→	809
596	→	125
514	→	914
514	→	1213
514	→	1296
514	→	1633
1315	→	705
1771	→	846
1771	→	1517
1517	→	846
1432	→	754
1432	→	390
1432	→	791
1432	→	710
1432	→	300
1432	→	329
1432	→	414
1497	→	840
1556	→	92
753	→	369
1247	→	201
1878	→	271
1878	→	1893
1632	→	1614
1712	→	1697
1958	→	201
370	→	1
370	→	460
370	→	649
370	→	499
370	→	482
370	→	1598
1399	→	605
1255	→	10
678	→	1254
1204	→	1182
724	→	1413
126	→	4
126	→	87
126	→	40
126	→	678
126	→	650
902	→	880
1239	→	201
42	→	9
137	→	5
137	→	327
137	→	669
64	→	9
64	→	411
64	→	4
64	→	87
957	→	117
957	→	506
957	→	42
957	→	809
957	→	818
1816	→	128
1321	→	711
709	→	278
1541	→	857
158	→	128
1745	→	2055
458	→	429
458	→	1627
1718	→	935
990	→	327
990	→	5
990	→	669
531	→	605
531	→	745
531	→	799
531	→	870
763	→	1260
414	→	390
1886	→	1073
17	→	918
17	→	1209
17	→	1283
17	→	1761
1952	→	201
1894	→	362
360	→	300
712	→	1396
250	→	201
250	→	1498
1523	→	845
1502	→	512
2068	→	299
2068	→	2079
1144	→	1848
1144	→	1935
1874	→	271
1874	→	1891
1245	→	201
1919	→	589
768	→	95
768	→	1522
1847	→	128
1990	→	387
1990	→	2037
203	→	1394
2026	→	801
1457	→	201
1695	→	1212
1904	→	299
1904	→	1983
1093	→	460
1093	→	541
1093	→	299
1093	→	127
1093	→	39
1093	→	229
1093	→	481
1093	→	1
1093	→	649
482	→	429
482	→	1
1058	→	271
1058	→	1109
388	→	362
388	→	694
744	→	2
744	→	711
744	→	769
744	→	588
744	→	201
744	→	252
744	→	755
744	→	1968
1619	→	1887
782	→	775
1620	→	1373
1620	→	2039
1660	→	9
711	→	783
711	→	845
1225	→	1809
1225	→	1943
790	→	136
1210	→	300
807	→	209
943	→	329
943	→	754
943	→	390
943	→	412
943	→	414
412	→	390
1233	→	806
1251	→	642
328	→	1846
328	→	1981
1942	→	201
1065	→	17
1065	→	1918
594	→	1685
1481	→	794
1759	→	2053
1241	→	201
1269	→	868
1777	→	970
210	→	3
210	→	870
210	→	745
210	→	531
210	→	542
210	→	863
210	→	431
210	→	792
210	→	1996
507	→	1250
507	→	1264
1211	→	1815
1211	→	1949
767	→	1246
1797	→	128
725	→	4
725	→	615
725	→	413
725	→	411
725	→	9
725	→	87
1023	→	870
1023	→	745
1023	→	531
1023	→	558
1023	→	359
1023	→	198
1023	→	63
1023	→	269
1023	→	439
1023	→	3
1023	→	542
1023	→	1996
682	→	1072
682	→	1111
798	→	700
1920	→	2061
1920	→	2073
992	→	981
2016	→	605
1810	→	128
1465	→	793
395	→	367
1147	→	390
1147	→	791
1147	→	710
1147	→	300
1147	→	329
1147	→	414
656	→	95
430	→	1174
1968	→	201
327	→	300
156	→	128
1189	→	615
1189	→	413
1189	→	411
1189	→	4
1189	→	9
1189	→	87
1946	→	201
1960	→	201
1519	→	845
1₁(1092)	→	1093
1₁(982)	→	983
1₁(622)	→	623
1₁(1615)	→	1616
1₁(411)	→	412
1₁(328)	→	329
1₁(749)	→	750
1₁(842)	→	843
1₁(1252)	→	1253
1₁(344)	→	345
1₁(1085)	→	1086
1₁(815)	→	816
1₁(326)	→	327
1₁(362)	→	363
1₁(654)	→	655
1₁(735)	→	736
1₁(859)	→	860
1₁(1427)	→	1428
1₁(872)	→	873
1₁(1555)	→	1556
1₁(786)	→	787
1₁(1146)	→	1147
1₁(981)	→	982
1₁(1209)	→	1210
1₁(730)	→	731
1₁(598)	→	599
1₁(985)	→	986
1₁(787)	→	788
1₁(369)	→	370
1₁(205)	→	206
1₁(616)	→	617
1₁(1617)	→	1618
1₁(129)	→	130
1₁(767)	→	768
1₁(882)	→	883
1₁(841)	→	842
1₁(839)	→	840
1₁(731)	→	732
1₁(751)	→	752
1₁(1213)	→	1214
1₁(1429)	→	1430
1₁(652)	→	653
1₁(1496)	→	1497
1₁(1211)	→	1212
1₁(812)	→	813
1₁(729)	→	730
1₁(1018)	→	1019
1₁(1920)	→	1921
1₁(1140)	→	1141
1₁(299)	→	300
1₁(499)	→	500
1₁(986)	→	987
1₁(1144)	→	1145
1₁(593)	→	594
1₁(775)	→	776
1₁(90)	→	91
1₁(502)	→	503
1₁(758)	→	759
1₁(131)	→	132
1₁(858)	→	859
1₁(668)	→	669
1₁(1225)	→	1226
1₁(135)	→	136
1₁(128)	→	129
1₁(429)	→	430
1₁(736)	→	737
1₁(11)	→	12
1₁(617)	→	618
1₁(773)	→	774
1₁(884)	→	885
1₁(1086)	→	1087
1₁(813)	→	814
1₁(436)	→	437
1₁(864)	→	865
1₁(628)	→	629
1₁(984)	→	985
1₁(861)	→	862
1₁(621)	→	622
1₁(877)	→	878
1₁(346)	→	347
1₁(437)	→	438
1₁(133)	→	134
1₁(363)	→	364
1₁(132)	→	133
1₁(389)	→	390
1₁(359)	→	360
1₁(653)	→	654
1₁(413)	→	414
1₁(591)	→	592
1₁(714)	→	715
1₁(988)	→	989
1₁(393)	→	394
4₂(905)	→	906
4₂(933)	→	934
4₂(910)	→	911
4₂(1861)	→	1862
4₂(1925)	→	1926
4₂(903)	→	904
4₂(907)	→	908
4₂(1928)	→	1929
4₂(977)	→	978
4₂(1711)	→	1712
4₂(904)	→	905
4₂(2053)	→	2054
4₂(1697)	→	1698
4₂(1862)	→	1863
4₂(1648)	→	1649
4₂(1704)	→	1705
4₂(1645)	→	1646
4₂(955)	→	956
4₂(1769)	→	1770
4₂(1685)	→	1686
4₂(1717)	→	1718
4₂(969)	→	970
4₂(1696)	→	1697
4₂(1637)	→	1638
4₂(1651)	→	1652
4₂(1635)	→	1636
4₂(934)	→	935
4₂(1640)	→	1641
4₂(2055)	→	2056
4₂(1924)	→	1925
4₂(1127)	→	1128
4₂(1686)	→	1687
4₂(1761)	→	1762
4₂(1646)	→	1647
4₂(1758)	→	1759
4₂(1633)	→	1634
4₂(1693)	→	1694
4₂(1744)	→	1745
4₂(1644)	→	1645
4₂(1929)	→	1930
4₂(941)	→	942
4₂(1634)	→	1635
4₂(1776)	→	1777
1₂(1011)	→	1012
1₂(1128)	→	1129
1₂(1689)	→	1690
1₂(1132)	→	1133
1₂(1136)	→	1137
1₂(1074)	→	1075
1₂(1700)	→	1701
1₂(1006)	→	1007
1₂(1647)	→	1648
1₂(1081)	→	1082
1₂(1930)	→	1931
1₂(1636)	→	1637
1₂(1013)	→	1014
1₂(937)	→	938
1₂(1901)	→	1902
1₂(1010)	→	1011
1₂(906)	→	907
1₂(1007)	→	1008
1₂(1009)	→	1010
1₂(1075)	→	1076
0₂(1135)	→	1136
0₂(1933)	→	1934
0₂(1078)	→	1079
0₂(1864)	→	1865
0₂(911)	→	912
0₂(972)	→	973
0₂(1753)	→	1754
0₂(1739)	→	1740
0₂(1652)	→	1653
0₂(942)	→	943
0₂(1688)	→	1689
0₂(1764)	→	1765
0₂(1705)	→	1706
0₂(950)	→	951
0₂(1012)	→	1013
0₂(1131)	→	1132
0₂(908)	→	909
0₂(1699)	→	1700
0₂(1080)	→	1081
0₂(1638)	→	1639
0₂(936)	→	937
0₂(1649)	→	1650
0₂(1931)	→	1932
0₂(1641)	→	1642
0₂(1694)	→	1695
4₁(803)	→	804
4₁(1236)	→	1237
4₁(1490)	→	1491
4₁(2079)	→	2080
4₁(65)	→	66
4₁(675)	→	676
4₁(1425)	→	1426
4₁(1983)	→	1984
4₁(2025)	→	2026
4₁(918)	→	919
4₁(433)	→	434
4₁(677)	→	678
4₁(1016)	→	1017
4₁(867)	→	868
4₁(1370)	→	1371
4₁(650)	→	651
4₁(808)	→	809
4₁(810)	→	811
4₁(696)	→	697
4₁(856)	→	857
4₁(9)	→	10
4₁(1458)	→	1459
4₁(772)	→	773
4₁(276)	→	277
4₁(594)	→	595
4₁(706)	→	707
4₁(1314)	→	1315
4₁(1498)	→	1499
4₁(41)	→	42
4₁(1290)	→	1291
4₁(1482)	→	1483
4₁(275)	→	276
4₁(792)	→	793
4₁(715)	→	716
4₁(1516)	→	1517
4₁(612)	→	613
4₁(2037)	→	2038
4₁(620)	→	621
4₁(793)	→	794
4₁(1180)	→	1181
4₁(672)	→	673
4₁(1659)	→	1660
4₁(914)	→	915
4₁(124)	→	125
4₁(8)	→	9
4₁(63)	→	64
4₁(599)	→	600
4₁(1466)	→	1467
4₁(771)	→	772
4₁(1369)	→	1370
4₁(94)	→	95
4₁(1329)	→	1330
4₁(800)	→	801
4₁(12)	→	13
4₁(719)	→	720
4₁(86)	→	87
4₁(1426)	→	1427
4₁(619)	→	620
4₁(611)	→	612
4₁(705)	→	706
4₁(718)	→	719
4₁(10)	→	11
4₁(39)	→	40
4₁(780)	→	781
4₁(1492)	→	1493
4₁(704)	→	705
4₁(920)	→	921
4₁(649)	→	650
4₁(720)	→	721
4₁(531)	→	532
4₁(806)	→	807
4₁(857)	→	858
4₁(740)	→	741
4₁(1287)	→	1288
4₁(1231)	→	1232
4₁(636)	→	637
4₁(500)	→	501
4₁(1328)	→	1329
4₁(1464)	→	1465
4₁(15)	→	16
4₁(1248)	→	1249
4₁(209)	→	210
4₁(1540)	→	1541
4₁(916)	→	917
4₁(784)	→	785
4₁(1174)	→	1175
4₁(845)	→	846
4₁(627)	→	628
4₁(817)	→	818
4₁(762)	→	763
4₁(796)	→	797
4₁(626)	→	627
4₁(1154)	→	1155
4₁(1480)	→	1481
4₁(203)	→	204
4₁(609)	→	610
4₁(501)	→	502
4₁(1022)	→	1023
4₁(852)	→	853
4₁(651)	→	652
4₁(1254)	→	1255
4₁(739)	→	740
4₁(699)	→	700
1₀(3)	→	5
1₀(6)	→	5
1₀(5)	→	5
1₀(4)	→	5
1₀(2)	→	5
1₀(1)	→	5
2₀(2)	→	6
2₀(6)	→	6
2₀(4)	→	6
2₀(1)	→	6
2₀(3)	→	6
2₀(5)	→	6
5₂(1859)	→	1860
5₂(1691)	→	1692
5₂(1690)	→	1691
5₂(1927)	→	1928
5₂(1926)	→	1927
5₂(1702)	→	1703
5₂(1073)	→	1074
5₂(1701)	→	1702
5₂(1008)	→	1009
5₂(939)	→	940
5₂(1858)	→	1859
5₂(938)	→	939
4₀(1)	→	4
4₀(6)	→	4
4₀(3)	→	4
4₀(5)	→	4
4₀(2)	→	4
4₀(4)	→	4
2₁(644)	→	645
2₁(843)	→	844
2₁(849)	→	850
2₁(846)	→	847
2₁(1288)	→	1289
2₁(1499)	→	1500
2₁(694)	→	695
2₁(1057)	→	1058
2₁(512)	→	513
2₁(1895)	→	1896
2₁(1989)	→	1990
2₁(1840)	→	1841
2₁(1203)	→	1204
2₁(1916)	→	1917
2₁(1883)	→	1884
2₁(1063)	→	1064
2₁(717)	→	718
2₁(1877)	→	1878
2₁(1613)	→	1614
2₁(391)	→	392
2₁(1815)	→	1816
2₁(873)	→	874
2₁(122)	→	123
2₁(1832)	→	1833
2₁(507)	→	508
2₁(589)	→	590
2₁(697)	→	698
2₁(1083)	→	1084
2₁(208)	→	209
2₁(1285)	→	1286
2₁(1848)	→	1849
2₁(850)	→	851
2₁(136)	→	137
2₁(1842)	→	1843
2₁(1205)	→	1206
2₁(297)	→	298
2₁(513)	→	514
2₁(741)	→	742
2₁(763)	→	764
2₁(1234)	→	1235
2₁(1268)	→	1269
2₁(304)	→	305
2₁(770)	→	771
2₁(1188)	→	1189
2₁(157)	→	158
2₁(198)	→	199
2₁(511)	→	512
2₁(711)	→	712
2₁(365)	→	366
2₁(789)	→	790
2₁(980)	→	981
2₁(539)	→	540
2₁(991)	→	992
2₁(1871)	→	1872
2₁(532)	→	533
2₁(305)	→	306
2₁(1017)	→	1018
2₁(847)	→	848
2₁(155)	→	156
2₁(1887)	→	1888
2₁(1873)	→	1874
2₁(630)	→	631
2₁(1229)	→	1230
2₁(993)	→	994
2₁(1111)	→	1112
2₁(271)	→	272
2₁(788)	→	789
2₁(769)	→	770
2₁(1373)	→	1374
2₁(1019)	→	1020
2₁(755)	→	756
2₁(206)	→	207
2₁(1595)	→	1596
2₁(274)	→	275
2₁(765)	→	766
2₁(799)	→	800
2₁(1181)	→	1182
2₁(875)	→	876
2₁(1627)	→	1628
2₁(176)	→	177
2₁(1003)	→	1004
2₁(1033)	→	1034
2₁(752)	→	753
2₁(1809)	→	1810
2₁(121)	→	122
2₁(1298)	→	1299
2₁(503)	→	504
2₁(607)	→	608
2₁(1817)	→	1818
2₁(1846)	→	1847
2₁(300)	→	301
2₁(989)	→	990
2₁(880)	→	881
2₁(1021)	→	1022
2₁(1371)	→	1372
2₁(1296)	→	1297
2₁(2061)	→	2062
2₁(1500)	→	1501
2₁(1798)	→	1799
2₁(1834)	→	1835
2₁(1088)	→	1089
2₁(1854)	→	1855
2₁(743)	→	744
2₁(127)	→	128
2₁(1294)	→	1295
2₁(204)	→	205
2₁(1631)	→	1632
2₁(435)	→	436
2₁(855)	→	856
2₁(1283)	→	1284
2₁(732)	→	733
2₁(1062)	→	1063
2₁(1811)	→	1812
2₁(178)	→	179
2₁(632)	→	633
2₁(1138)	→	1139
2₁(508)	→	509
2₁(1796)	→	1797
2₁(683)	→	684
5₁(1244)	→	1245
5₁(1518)	→	1519
5₁(881)	→	882
5₁(674)	→	675
5₁(1945)	→	1946
5₁(1331)	→	1332
5₁(588)	→	589
5₁(781)	→	782
5₁(1951)	→	1952
5₁(1185)	→	1186
5₁(838)	→	839
5₁(750)	→	751
5₁(1937)	→	1938
5₁(1183)	→	1184
5₁(860)	→	861
5₁(1064)	→	1065
5₁(229)	→	230
5₁(1981)	→	1982
5₁(2023)	→	2024
5₁(625)	→	626
5₁(1949)	→	1950
5₁(1267)	→	1268
5₁(200)	→	201
5₁(273)	→	274
5₁(681)	→	682
5₁(615)	→	616
5₁(883)	→	884
5₁(1322)	→	1323
5₁(701)	→	702
5₁(1935)	→	1936
5₁(802)	→	803
5₁(361)	→	362
5₁(534)	→	535
5₁(1456)	→	1457
5₁(130)	→	131
5₁(92)	→	93
5₁(1242)	→	1243
5₁(1614)	→	1615
5₁(610)	→	611
5₁(1109)	→	1110
5₁(91)	→	92
5₁(1266)	→	1267
5₁(983)	→	984
5₁(1959)	→	1960
5₁(1965)	→	1966
5₁(840)	→	841
5₁(1240)	→	1241
5₁(2039)	→	2040
5₁(251)	→	252
5₁(590)	→	591
5₁(811)	→	812
5₁(269)	→	270
5₁(1284)	→	1285
5₁(1084)	→	1085
5₁(624)	→	625
5₁(1918)	→	1919
5₁(642)	→	643
5₁(306)	→	307
5₁(745)	→	746
5₁(536)	→	537
5₁(1889)	→	1890
5₁(613)	→	614
5₁(387)	→	388
5₁(722)	→	723
5₁(708)	→	709
5₁(713)	→	714
5₁(710)	→	711
5₁(783)	→	784
5₁(1625)	→	1626
5₁(1107)	→	1108
5₁(2073)	→	2074
5₁(865)	→	866
5₁(1292)	→	1293
5₁(1893)	→	1894
5₁(795)	→	796
5₁(886)	→	887
5₁(1488)	→	1489
5₁(231)	→	232
5₁(1494)	→	1495
5₁(1967)	→	1968
5₁(1943)	→	1944
5₁(535)	→	536
5₁(1957)	→	1958
5₁(1250)	→	1251
5₁(1522)	→	1523
5₁(1320)	→	1321
5₁(1619)	→	1620
5₁(1184)	→	1185
5₁(754)	→	755
5₁(785)	→	786
5₁(1616)	→	1617
5₁(272)	→	273
5₁(1232)	→	1233
5₁(1891)	→	1892
5₁(1207)	→	1208
5₁(1939)	→	1940
5₁(641)	→	642
5₁(633)	→	634
5₁(597)	→	598
5₁(638)	→	639
5₁(1238)	→	1239
5₁(682)	→	683
5₁(1941)	→	1942
5₁(249)	→	250
5₁(1246)	→	1247
5₀(3)	→	2
5₀(5)	→	2
5₀(2)	→	2
5₀(4)	→	2
5₀(1)	→	2
5₀(6)	→	2
3₀(2)	→	3
3₀(4)	→	3
3₀(3)	→	3
3₀(6)	→	3
3₀(1)	→	3
3₀(5)	→	3
3₁(584)	→	585
3₁(1413)	→	1414
3₁(748)	→	749
3₁(17)	→	18
3₁(1330)	→	1331
3₁(801)	→	802
3₁(2015)	→	2016
3₁(774)	→	775
3₁(430)	→	431
3₁(814)	→	815
3₁(530)	→	531
3₁(1291)	→	1292
3₁(595)	→	596
3₁(670)	→	671
3₁(364)	→	365
3₁(1227)	→	1228
3₁(1995)	→	1996
3₁(1428)	→	1429
3₁(541)	→	542
3₁(779)	→	780
3₁(277)	→	278
3₁(791)	→	792
3₁(618)	→	619
3₁(645)	→	646
3₁(117)	→	118
3₁(1394)	→	1395
3₁(394)	→	395
3₁(1396)	→	1397
3₁(1398)	→	1399
3₁(761)	→	762
3₁(1286)	→	1287
3₁(1922)	→	1923
3₁(695)	→	696
3₁(88)	→	89
3₁(809)	→	810
3₁(2009)	→	2010
3₁(390)	→	391
3₁(874)	→	875
3₁(1368)	→	1369
3₁(721)	→	722
3₁(2081)	→	2082
3₁(367)	→	368
3₁(582)	→	583
3₁(851)	→	852
3₁(671)	→	672
3₁(863)	→	864
3₁(655)	→	656
3₁(2017)	→	2018
3₁(698)	→	699
3₁(537)	→	538
3₁(1264)	→	1265
3₁(2007)	→	2008
3₁(600)	→	601
3₁(643)	→	644
3₁(514)	→	515
3₁(1417)	→	1418
3₁(1289)	→	1290
3₁(14)	→	15
3₁(1141)	→	1142
3₁(866)	→	867
3₁(778)	→	779
3₁(601)	→	602
3₁(804)	→	805
3₁(746)	→	747
3₁(603)	→	604
3₁(723)	→	724
3₁(605)	→	606
3₁(1090)	→	1091
3₁(756)	→	757
3₁(93)	→	94
3₁(634)	→	635
3₁(1059)	→	1060
3₁(556)	→	557
3₁(1423)	→	1424
3₁(125)	→	126
3₁(1087)	→	1088
3₁(700)	→	701
3₁(703)	→	704
3₁(764)	→	765
3₁(123)	→	124
3₁(1142)	→	1143
3₁(1411)	→	1412
3₁(738)	→	739
3₁(1415)	→	1416
3₁(635)	→	636
3₁(679)	→	680
3₁(1392)	→	1393
3₁(120)	→	121
3₁(1186)	→	1187
3₁(558)	→	559
3₁(1332)	→	1333
3₁(669)	→	670
3₁(301)	→	302
3₁(201)	→	202
3₁(118)	→	119
3₁(307)	→	308
0₁(1152)	→	1153
0₁(646)	→	647
0₁(848)	→	849
0₁(1060)	→	1061
0₁(592)	→	593
0₁(366)	→	367
0₁(308)	→	309
0₁(1089)	→	1090
0₁(134)	→	135
0₁(207)	→	208
0₁(2045)	→	2046
0₁(1612)	→	1613
0₁(766)	→	767
0₁(876)	→	877
0₁(434)	→	435
0₁(538)	→	539
0₁(879)	→	880
0₁(1153)	→	1154
0₁(428)	→	429
0₁(459)	→	460
0₁(16)	→	17
0₁(392)	→	393
0₁(498)	→	499
0₁(89)	→	90
0₁(759)	→	760
0₁(368)	→	369
0₁(510)	→	511
0₁(868)	→	869
0₁(1155)	→	1156
0₁(854)	→	855
0₁(439)	→	440
0₁(1430)	→	1431
0₁(1265)	→	1266
0₁(640)	→	641
0₁(1091)	→	1092
0₁(608)	→	609
0₁(1372)	→	1373
0₁(479)	→	480
0₁(1020)	→	1021
0₁(506)	→	507
0₁(1501)	→	1502
0₁(13)	→	14
0₁(504)	→	505
0₁(680)	→	681
0₁(629)	→	630
0₁(724)	→	725
0₁(871)	→	872
0₁(2067)	→	2068
0₁(431)	→	432
0₁(870)	→	871
0₁(678)	→	679
0₁(712)	→	713
0₁(885)	→	886
0₁(1061)	→	1062
0₁(1260)	→	1261
0₁(987)	→	988
0₁(602)	→	603
0₁(278)	→	279
0₁(733)	→	734
0₁(747)	→	748
0₁(901)	→	902
0₁(1333)	→	1334
0₁(606)	→	607
0₁(757)	→	758
0₁(1139)	→	1140
0₁(742)	→	743
0₁(648)	→	649
0₁(1599)	→	1600
0₁(707)	→	708
0₁(533)	→	534
0₁(1903)	→	1904
0₁(432)	→	433
0₁(457)	→	458
0₁(1618)	→	1619
0₁(1230)	→	1231
0₁(637)	→	638
0₁(797)	→	798
0₁(1597)	→	1598
0₁(1187)	→	1188
0₁(805)	→	806
0₁(302)	→	303
0₁(673)	→	674
0₁(684)	→	685
0₁(202)	→	203
0₁(1431)	→	1432
0₁(899)	→	900
0₁(509)	→	510
0₁(794)	→	795
0₁(737)	→	738
0₁(303)	→	304
0₁(776)	→	777
0₁(946)	→	947
0₁(95)	→	96
0₁(2047)	→	2048
0₁(1143)	→	1144
0₁(1182)	→	1183
0₁(481)	→	482
0₁(728)	→	729
0₁(119)	→	120
0₁(1228)	→	1229
2₂(1014)	→	1015
2₂(1857)	→	1858
2₂(1856)	→	1857
2₂(1766)	→	1767
2₂(975)	→	976
2₂(1741)	→	1742
2₂(1860)	→	1861
2₂(953)	→	954
2₂(1755)	→	1756
2₂(1077)	→	1078
2₂(1130)	→	1131
2₂(1072)	→	1073
2₂(1742)	→	1743
2₂(974)	→	975
2₂(1756)	→	1757
2₂(1767)	→	1768
2₂(952)	→	953
2₂(1005)	→	1006
2₂(1885)	→	1886
2₂(1932)	→	1933
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
3₂(1698)	→	1699
3₂(1752)	→	1753
3₂(909)	→	910
3₂(948)	→	949
3₂(1687)	→	1688
3₂(1076)	→	1077
3₂(1692)	→	1693
3₂(956)	→	957
3₂(1642)	→	1643
3₂(951)	→	952
3₂(970)	→	971
3₂(976)	→	977
3₂(935)	→	936
3₂(1762)	→	1763
3₂(1134)	→	1135
3₂(978)	→	979
3₂(940)	→	941
3₂(1763)	→	1764
3₂(1743)	→	1744
3₂(1740)	→	1741
3₂(1737)	→	1738
3₂(1757)	→	1758
3₂(1759)	→	1760
3₂(1738)	→	1739
3₂(949)	→	950
3₂(1650)	→	1651
3₂(1751)	→	1752
3₂(1765)	→	1766
3₂(1745)	→	1746
3₂(1079)	→	1080
3₂(1133)	→	1134
3₂(954)	→	955
3₂(1754)	→	1755
3₂(1653)	→	1654
3₂(971)	→	972
3₂(1768)	→	1769
3₂(1863)	→	1864
3₂(1129)	→	1130
3₂(1639)	→	1640
3₂(973)	→	974
3₂(1703)	→	1704
3₂(1865)	→	1866
3₂(1770)	→	1771
3₂(912)	→	913

The automaton is closed under rewriting as it is compatible.