Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4106)

The rewrite relation of the following TRS is considered.

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

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(2(x1))	→	3(1(0(0(1(4(0(0(4(2(x1))))))))))	(30)
5(2(x1))	→	3(4(1(2(2(2(0(3(4(2(x1))))))))))	(31)
0(5(1(x1)))	→	1(1(0(4(0(4(4(4(4(1(x1))))))))))	(32)
5(3(2(x1)))	→	1(2(2(1(5(1(0(0(4(2(x1))))))))))	(33)
5(5(2(x1)))	→	4(3(3(3(0(4(0(3(0(2(x1))))))))))	(34)
4(5(4(x1)))	→	4(2(5(4(1(2(1(1(1(4(x1))))))))))	(35)
4(0(3(2(x1))))	→	4(4(2(0(3(1(1(0(0(2(x1))))))))))	(36)
0(1(5(5(x1))))	→	4(0(4(3(1(5(0(2(2(3(x1))))))))))	(37)
5(2(5(1(3(x1)))))	→	2(5(0(0(2(1(4(2(0(3(x1))))))))))	(38)
2(3(4(5(2(0(x1))))))	→	2(1(2(1(0(2(5(1(2(0(x1))))))))))	(39)
4(3(2(5(0(1(x1))))))	→	3(0(1(4(0(3(1(0(0(1(x1))))))))))	(40)
3(2(0(5(1(1(x1))))))	→	3(2(2(1(1(1(5(4(0(0(x1))))))))))	(41)
2(3(0(0(1(2(x1))))))	→	2(3(0(3(0(0(3(4(1(2(x1))))))))))	(42)
5(5(5(0(5(2(x1))))))	→	5(5(3(5(0(4(2(1(0(2(x1))))))))))	(43)
1(2(0(3(5(2(x1))))))	→	1(2(5(2(1(2(5(4(1(2(x1))))))))))	(44)
5(5(4(0(5(3(x1))))))	→	3(3(0(2(5(4(3(0(4(3(x1))))))))))	(45)
2(4(3(2(0(4(x1))))))	→	2(2(0(3(4(1(3(0(0(4(x1))))))))))	(46)
0(1(5(5(2(5(x1))))))	→	4(1(0(2(4(0(4(4(5(5(x1))))))))))	(47)
5(0(3(2(4(5(x1))))))	→	1(3(1(4(3(4(5(4(5(5(x1))))))))))	(48)
5(1(1(1(5(5(x1))))))	→	1(4(1(0(1(1(0(1(0(5(x1))))))))))	(49)
0(5(5(2(5(5(x1))))))	→	0(1(4(4(3(5(2(5(4(3(x1))))))))))	(50)
4(5(5(4(5(5(x1))))))	→	4(0(4(3(4(5(5(2(2(2(x1))))))))))	(51)
5(2(5(5(5(5(x1))))))	→	5(4(2(3(4(1(1(3(2(2(x1))))))))))	(52)
5(0(5(5(0(4(1(x1)))))))	→	3(3(5(1(4(0(3(3(4(1(x1))))))))))	(53)
5(2(1(5(3(2(2(x1)))))))	→	5(2(3(3(0(4(2(1(2(2(x1))))))))))	(54)
5(5(3(3(2(4(3(x1)))))))	→	5(0(4(4(2(0(4(2(3(5(x1))))))))))	(55)
5(5(4(3(5(2(4(x1)))))))	→	0(1(1(4(0(5(2(5(1(5(x1))))))))))	(56)
4(2(4(5(5(2(4(x1)))))))	→	0(3(0(1(2(0(2(3(5(5(x1))))))))))	(57)
2(3(2(4(5(5(4(x1)))))))	→	2(4(2(1(5(3(5(1(1(4(x1))))))))))	(58)

1.1 Bounds

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

final states:

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

transitions:

503	→	471
1906	→	1894
730	→	604
1067	→	1834
1659	→	1598
223	→	822
871	→	858
871	→	1849
1602	→	1662
1151	→	375
1151	→	2013
867	→	748
867	→	671
867	→	665
867	→	654
867	→	1793
867	→	1991
867	→	1971
1895	→	2044
221	→	625
221	→	1030
221	→	1452
376	→	857
376	→	1368
457	→	427
457	→	524
1231	→	1543
1231	→	1879
1940	→	699
633	→	435
1459	→	9
1257	→	1250
2046	→	2067
202	→	1490
1057	→	801
1057	→	681
1057	→	771
1057	→	653
1057	→	795
1057	→	663
87	→	1293
1117	→	1758
715	→	700
715	→	731
1109	→	671
1109	→	1164
1109	→	813
1109	→	654
1109	→	1741
1109	→	2009
1109	→	1888
1109	→	2010
1109	→	785
1109	→	1991
1109	→	1527
1109	→	2007
1109	→	1506
1109	→	2288
1109	→	1516
794	→	1
794	→	813
794	→	801
794	→	681
794	→	748
794	→	653
794	→	799
794	→	671
794	→	654
794	→	2009
794	→	785
794	→	1991
2181	→	1510
1475	→	739
229	→	1515
229	→	1737
1989	→	786
1288	→	1280
10	→	85
1163	→	222
2297	→	1894
273	→	221
1261	→	463
1557	→	2114
2394	→	1137
915	→	997
1688	→	1033
2240	→	1737
2240	→	1988
2240	→	229
2240	→	1888
1367	→	628
1864	→	598
2427	→	690
571	→	1
571	→	813
571	→	801
571	→	681
571	→	748
571	→	653
571	→	799
571	→	671
571	→	654
571	→	665
571	→	2009
571	→	1737
571	→	1988
571	→	2010
571	→	229
571	→	1888
571	→	785
571	→	1991
571	→	739
571	→	1971
1393	→	1600
1046	→	1033
1578	→	1644
578	→	1032
578	→	1279
1473	→	739
1769	→	1144
438	→	427
438	→	502
438	→	1110
1544	→	914
326	→	300
326	→	422
326	→	610
2396	→	1136
2239	→	2401
1784	→	83
1784	→	1889
1993	→	785
1993	→	2011
655	→	674
655	→	625
655	→	6
655	→	221
655	→	253
2133	→	2006
543	→	471
543	→	1177
543	→	1366
1195	→	1180
84	→	9
84	→	708
84	→	2
84	→	301
84	→	1082
84	→	858
84	→	1894
84	→	1953
84	→	1906
84	→	1847
84	→	1568
167	→	112
167	→	1152
956	→	789
436	→	2
436	→	84
436	→	1955
436	→	1908
119	→	1291
145	→	112
145	→	1146
1792	→	368
1792	→	1863
1575	→	739
1575	→	1473
122	→	1670
122	→	1815
2242	→	2233
668	→	1907
668	→	1954
1953	→	699
2054	→	1897
18	→	1
18	→	681
18	→	801
18	→	665
18	→	813
18	→	748
18	→	799
18	→	671
18	→	654
18	→	739
18	→	785
18	→	667
18	→	1971
18	→	2009
18	→	1991
624	→	598
624	→	690
1230	→	2304
1230	→	2312
469	→	6
469	→	690
469	→	232
469	→	598
469	→	624
469	→	1890
2402	→	570
1118	→	671
41	→	9
41	→	699
1577	→	1713
39	→	9
120	→	1043
120	→	1287
3	→	83
3	→	146
3	→	231
3	→	325
3	→	458
3	→	662
1506	→	1527
652	→	1937
652	→	1962
653	→	681
653	→	773
653	→	801
653	→	2296
653	→	2308
772	→	740
1254	→	1984
691	→	898
1634	→	1574
1888	→	229
1888	→	1988
626	→	1358
1294	→	549
2313	→	699
1858	→	598
2012	→	813
347	→	300
347	→	368
347	→	597
347	→	1448
347	→	1865
861	→	1691
298	→	229
1359	→	600
9	→	195
9	→	544
9	→	714
1714	→	1704
914	→	1100
5	→	61
5	→	144
5	→	220
5	→	346
5	→	452
5	→	666
774	→	740
147	→	112
671	→	653
671	→	748
671	→	799
1738	→	1165
1932	→	1894
698	→	5
698	→	427
698	→	682
1969	→	739
2289	→	674
275	→	221
275	→	995
1027	→	1821
1048	→	1770
2429	→	1894
1618	→	1554
255	→	221
255	→	1021
255	→	1305
1991	→	785
1991	→	2009
1134	→	703
1866	→	629
2311	→	699
749	→	740
193	→	1045
193	→	1289
1965	→	739
1031	→	114
397	→	369
1890	→	690
1068	→	1687
1068	→	1819
713	→	700
62	→	9
62	→	712
2354	→	144
1833	→	301
700	→	716
700	→	846
1599	→	1428
1	→	38
1	→	168
1	→	252
1	→	366
1	→	426
1	→	670
123	→	112
123	→	4
123	→	429
123	→	1033
123	→	1671
1308	→	548
826	→	1587
1902	→	1144
2291	→	1894
1591	→	1652
1957	→	699
654	→	813
654	→	1164
654	→	1887
922	→	1791
922	→	1964
1489	→	739
2423	→	83
2423	→	2426
1081	→	10
2074	→	2053
667	→	653
667	→	739
667	→	785
1004	→	922
570	→	1194
570	→	1389
570	→	1438
570	→	1903
1626	→	1565
1318	→	83
1318	→	1873
477	→	1047
1317	→	2298
1317	→	2310
1922	→	1894
1938	→	1894
60	→	9
60	→	710
1426	→	1446
1426	→	1589
505	→	471
428	→	1225
689	→	193
747	→	570
723	→	570
723	→	1162
2288	→	2397
1029	→	427
609	→	598
1522	→	785
1522	→	1539
751	→	740
1547	→	1611
796	→	786
423	→	369
1161	→	223
1514	→	1432
297	→	2395
1232	→	801
1232	→	681
1232	→	1
1232	→	653
1232	→	665
1232	→	1971
253	→	221
253	→	993
253	→	668
253	→	348
253	→	166
253	→	8
253	→	272
253	→	456
253	→	6
253	→	1165
309	→	5
309	→	451
309	→	461
1669	→	1609
662	→	1905
662	→	1952
2238	→	2403
2238	→	2407
1971	→	739
349	→	300
349	→	398
349	→	608
1212	→	461
994	→	86
2305	→	1894
552	→	435
1176	→	291
1453	→	725
976	→	855
1310	→	565
121	→	5
121	→	427
121	→	682
1610	→	1395
6	→	8
6	→	166
6	→	272
6	→	348
6	→	456
6	→	668
627	→	909
627	→	1063
468	→	1488
1051	→	1569
1882	→	229
1042	→	682
577	→	1855
377	→	1
377	→	801
377	→	681
377	→	653
377	→	665
377	→	1971
1397	→	688
308	→	1521
2031	→	2005
2031	→	1987
2031	→	2399
1818	→	470
1234	→	427
1292	→	1280
2431	→	699
230	→	6
230	→	253
230	→	674
230	→	655
2400	→	1794
1566	→	1318
1987	→	785
1987	→	2005
1101	→	2232
900	→	985
2010	→	813
665	→	653
665	→	1
1180	→	1391
204	→	1
204	→	813
204	→	671
204	→	654
204	→	2009
204	→	785
204	→	1991
525	→	471
923	→	1
923	→	571
923	→	1807
923	→	1991
569	→	1179
569	→	1202
569	→	1424
569	→	1893
1516	→	1506
1516	→	2007
1516	→	2288
1188	→	1992
859	→	977
2	→	59
2	→	122
2	→	274
2	→	327
2	→	437
2	→	664
2008	→	814
787	→	946
1540	→	813
11	→	1456
4	→	40
4	→	111
4	→	254
4	→	299
4	→	450
4	→	652
232	→	221
1178	→	293
1178	→	1256
1174	→	676
1069	→	801
1069	→	681
1069	→	771
1069	→	1
1069	→	653
1069	→	795
1069	→	663
1848	→	1825
827	→	1505
827	→	1994
1786	→	368
1786	→	1857
2151	→	1137
1761	→	144
1761	→	1871
1538	→	813
478	→	1080
478	→	1175
478	→	1454
478	→	1472
479	→	3
479	→	623
479	→	300
479	→	328
479	→	1889
479	→	1784
252	→	1990
300	→	424
300	→	623
425	→	369
1108	→	2353
802	→	786
2341	→	144
1390	→	682
1491	→	739
1872	→	426
1692	→	1052
800	→	786
800	→	2355
2006	→	813
1012	→	933
1536	→	85
1536	→	625
1536	→	6
1536	→	221
1536	→	275
1536	→	10
1369	→	654
1369	→	1881
1555	→	1510
738	→	570
738	→	1121
738	→	1311
1835	→	1824
1145	→	253
1145	→	674
1145	→	655
1145	→	1165
1145	→	2023
1145	→	2059
1145	→	230
1145	→	1738
1145	→	2289
1145	→	2398
1586	→	1506
1586	→	1516
1586	→	1995
1586	→	2172
12	→	188
1963	→	699
1856	→	1824
169	→	112
169	→	1160
112	→	460
2004	→	85
2004	→	10
1771	→	1762
1455	→	732
1091	→	813
1091	→	654
1091	→	671
1091	→	2009
1091	→	1888
1091	→	2010
1091	→	785
1091	→	1991
1091	→	2150
1044	→	1033
1020	→	955
663	→	653
663	→	771
663	→	795
1712	→	1528
1712	→	1996
1255	→	690
1255	→	232
1255	→	668
1255	→	348
1255	→	166
1255	→	8
1255	→	272
1255	→	456
1255	→	6
1255	→	598
1255	→	624
1049	→	1627
934	→	577
1686	→	1033
113	→	724
113	→	1319
1122	→	196
2299	→	1894
1816	→	470
2045	→	2087
1316	→	1556
579	→	4
579	→	123
579	→	545
453	→	427
453	→	504
453	→	1248
709	→	700
856	→	702
847	→	1125
948	→	1013
1083	→	1762
1083	→	2241
1090	→	2340
828	→	435
707	→	229
1447	→	717
908	→	693
2408	→	699
83	→	1567
821	→	6
821	→	85
821	→	625
821	→	221
821	→	275
821	→	10
2014	→	222
17	→	1474
17	→	1809
683	→	1309
1822	→	470
1286	→	632
926	→	1005
1433	→	654
1433	→	801
1433	→	681
1433	→	748
1433	→	1
1433	→	653
1433	→	799
1433	→	671
1433	→	2009
1433	→	785
1433	→	1991
1439	→	1425
1144	→	1760
1144	→	1986
1144	→	2124
2401	→	2422
2401	→	2424
2401	→	2428
2401	→	2430
1874	→	229
2404	→	1894
666	→	1921
666	→	1956
1508	→	1545
664	→	1783
664	→	1929
664	→	1939
858	→	1082
1153	→	1147
203	→	1519
203	→	1743
1457	→	327
1368	→	2290
1368	→	2306
866	→	1785
866	→	1968
2307	→	699
2309	→	699
722	→	1135
1904	→	1894
523	→	471
1742	→	1137
1290	→	1280
848	→	969
670	→	1923
670	→	1958
1120	→	197
1959	→	699
711	→	700
92	→	17
1028	→	1685
1028	→	1817
451	→	427
451	→	470
1955	→	699
399	→	369
375	→	1931
375	→	1960
1651	→	1585
1520	→	785
1520	→	1537
575	→	924
1985	→	739
1306	→	86
2123	→	1874
2123	→	2393
328	→	300
328	→	662
328	→	325
328	→	146
328	→	83
328	→	231
328	→	458
328	→	3
1320	→	573
910	→	13
367	→	300
367	→	396
367	→	606
546	→	572
1908	→	1894
611	→	598
1759	→	1136
680	→	193
680	→	1233
1241	→	83
1930	→	1894
1568	→	858
1568	→	1847
669	→	653
669	→	750
1449	→	726
194	→	1
194	→	801
194	→	681
194	→	771
194	→	653
194	→	795
194	→	663
194	→	739
194	→	785
194	→	667
1558	→	1619
1671	→	1033
605	→	17
2066	→	2030
2398	→	1165
1924	→	1894
1961	→	699
725	→	1307
427	→	542
427	→	1119
427	→	1260
427	→	5
737	→	913
984	→	866
992	→	907
1850	→	1825
1588	→	1577
1588	→	1703
1590	→	1719
1810	→	1793
996	→	86
2096	→	1898
1802	→	789
1880	→	229
2356	→	822
1147	→	1541
192	→	1823
2425	→	1203
661	→	308
327	→	1970
607	→	598
228	→	1576
1189	→	451
1189	→	5
1189	→	461
1744	→	1136
1542	→	823
1820	→	470
459	→	427
459	→	522
196	→	291
196	→	563
1808	→	1794
545	→	1235
545	→	1458
435	→	870
1728	→	1429
5₁(1515)	→	1516
5₁(2005)	→	2006
5₁(1984)	→	1985
5₁(576)	→	577
5₁(1488)	→	1489
5₁(674)	→	675
5₁(692)	→	693
5₁(1490)	→	1491
5₁(1392)	→	1393
5₁(569)	→	570
5₁(1313)	→	1314
5₁(1541)	→	1542
5₁(1230)	→	1231
5₁(1319)	→	1320
5₁(1472)	→	1473
5₁(2009)	→	2010
5₁(664)	→	665
5₁(1879)	→	1880
5₁(670)	→	671
5₁(1507)	→	1508
5₁(702)	→	703
5₁(1427)	→	1428
5₁(666)	→	667
5₁(1519)	→	1520
5₁(1368)	→	1369
5₁(1873)	→	1874
5₁(786)	→	787
5₁(1317)	→	1318
5₁(1509)	→	1510
5₁(1964)	→	1965
5₁(822)	→	823
5₁(303)	→	304
5₁(1992)	→	1993
5₁(1474)	→	1475
5₁(1968)	→	1969
5₁(652)	→	653
5₁(690)	→	691
5₁(1986)	→	1987
5₁(1064)	→	1065
5₁(729)	→	730
5₁(1970)	→	1971
5₁(1183)	→	1184
5₁(601)	→	602
5₁(788)	→	789
5₁(1539)	→	1540
5₁(1521)	→	1522
5₁(2011)	→	2012
5₁(1887)	→	1888
5₁(668)	→	669
5₁(1282)	→	1283
5₁(472)	→	473
5₁(1505)	→	1506
5₁(429)	→	430
5₁(1428)	→	1429
5₁(662)	→	663
5₁(1235)	→	1236
5₁(1527)	→	1528
5₁(701)	→	702
5₁(189)	→	190
5₁(2401)	→	2402
5₁(1394)	→	1395
5₁(572)	→	573
5₁(824)	→	825
5₁(567)	→	568
5₁(653)	→	654
5₁(570)	→	571
5₁(1990)	→	1991
5₁(1881)	→	1882
5₁(375)	→	376
5₁(1537)	→	1538
5₁(227)	→	228
5₂(2236)	→	2237
5₂(1897)	→	1898
5₂(2238)	→	2239
5₂(1994)	→	1995
5₂(1052)	→	1053
5₂(1171)	→	1172
5₂(2179)	→	2180
5₂(1995)	→	1996
5₂(1206)	→	1207
5₂(1800)	→	1801
5₂(1896)	→	1897
5₂(2239)	→	2240
5₂(1142)	→	1143
4₂(2234)	→	2235
4₂(1650)	→	1651
4₂(1711)	→	1712
4₂(1209)	→	1210
4₂(1898)	→	1899
4₂(1557)	→	1558
4₂(1706)	→	1707
4₂(1048)	→	1049
4₂(2025)	→	2026
4₂(1569)	→	1570
4₂(1658)	→	1659
4₂(1011)	→	1012
4₂(1668)	→	1669
4₂(1825)	→	1826
4₂(1743)	→	1744
4₂(1633)	→	1634
4₂(2065)	→	2066
4₂(1128)	→	1129
4₂(1003)	→	1004
4₂(899)	→	900
4₂(1768)	→	1769
4₂(917)	→	918
4₂(991)	→	992
4₂(1577)	→	1578
4₂(1133)	→	1134
4₂(1590)	→	1591
4₂(1019)	→	1020
4₂(858)	→	859
4₂(861)	→	862
4₂(902)	→	903
4₂(2132)	→	2133
4₂(1593)	→	1594
4₂(1722)	→	1723
4₂(1141)	→	1142
4₂(925)	→	926
4₂(1033)	→	1034
4₂(2127)	→	2128
4₂(847)	→	848
4₂(947)	→	948
4₂(1795)	→	1796
4₂(1580)	→	1581
4₂(1085)	→	1086
4₂(1625)	→	1626
4₂(1560)	→	1561
4₂(1604)	→	1605
4₂(850)	→	851
4₂(2122)	→	2123
4₂(975)	→	976
4₂(1737)	→	1738
4₂(1211)	→	1212
4₂(1170)	→	1171
4₂(1164)	→	1165
4₂(950)	→	951
4₂(1601)	→	1602
4₂(2395)	→	2396
4₂(1135)	→	1136
4₂(1617)	→	1618
4₂(1549)	→	1550
4₂(1758)	→	1759
4₂(928)	→	929
4₂(1035)	→	1036
4₂(1038)	→	1039
4₂(1546)	→	1547
4₂(1727)	→	1728
4₂(1900)	→	1901
4₂(2174)	→	2175
4₂(914)	→	915
4₂(1036)	→	1037
4₂(1034)	→	1035
4₂(983)	→	984
4₂(2397)	→	2398
4₂(1144)	→	1145
4₂(2117)	→	2118
4₂(1103)	→	1104
4₂(1108)	→	1109
4₂(1173)	→	1174
4₂(1090)	→	1091
0₂(1606)	→	1607
0₂(2001)	→	2002
0₂(1551)	→	1552
0₂(970)	→	971
0₂(1628)	→	1629
0₂(1603)	→	1604
0₂(926)	→	927
0₂(1125)	→	1126
0₂(1592)	→	1593
0₂(1037)	→	1038
0₂(1205)	→	1206
0₂(915)	→	916
0₂(901)	→	902
0₂(1770)	→	1771
0₂(1086)	→	1087
0₂(848)	→	849
0₂(1602)	→	1603
0₂(2399)	→	2400
0₂(948)	→	949
0₂(904)	→	905
0₂(1082)	→	1083
0₂(986)	→	987
0₂(1572)	→	1573
0₂(2177)	→	2178
0₂(2023)	→	2024
0₂(1707)	→	1708
0₂(1100)	→	1101
0₂(927)	→	928
0₂(1582)	→	1583
0₂(2027)	→	2028
0₂(1703)	→	1704
0₂(1102)	→	1103
0₂(2118)	→	2119
0₂(2178)	→	2179
0₂(930)	→	931
0₂(1104)	→	1105
0₂(1127)	→	1128
0₂(1793)	→	1794
0₂(859)	→	860
0₂(2114)	→	2115
0₂(1006)	→	1007
0₂(916)	→	917
0₂(919)	→	920
0₂(2126)	→	2127
0₂(1050)	→	1051
0₂(1014)	→	1015
0₂(864)	→	865
0₂(1901)	→	1902
0₂(1129)	→	1130
0₂(2028)	→	2029
0₂(1084)	→	1085
0₂(931)	→	932
0₂(2003)	→	2004
0₂(952)	→	953
0₂(2235)	→	2236
0₂(905)	→	906
0₂(978)	→	979
0₂(1998)	→	1999
0₂(1721)	→	1722
0₂(1583)	→	1584
0₂(1563)	→	1564
0₂(1723)	→	1724
0₂(2124)	→	2125
0₂(2060)	→	2061
0₂(1607)	→	1608
0₂(1571)	→	1572
0₂(1558)	→	1559
0₂(1830)	→	1831
0₂(2024)	→	2025
0₂(900)	→	901
0₂(1595)	→	1596
0₂(1578)	→	1579
0₂(1705)	→	1706
0₂(1798)	→	1799
0₂(1807)	→	1808
0₂(1049)	→	1050
0₂(860)	→	861
0₂(2172)	→	2173
0₂(1559)	→	1560
0₂(1547)	→	1548
0₂(1663)	→	1664
0₂(852)	→	853
0₂(1591)	→	1592
0₂(1713)	→	1714
0₂(1210)	→	1211
0₂(1653)	→	1654
0₂(1612)	→	1613
0₂(1562)	→	1563
0₂(2128)	→	2129
0₂(1552)	→	1553
0₂(1762)	→	1763
0₂(953)	→	954
0₂(1596)	→	1597
0₂(1579)	→	1580
0₂(920)	→	921
0₂(998)	→	999
0₂(2116)	→	2117
0₂(1799)	→	1800
0₂(849)	→	850
0₂(863)	→	864
0₂(1827)	→	1828
0₂(1766)	→	1767
0₂(1620)	→	1621
0₂(1719)	→	1720
0₂(853)	→	854
0₂(1039)	→	1040
0₂(1645)	→	1646
0₂(1828)	→	1829
0₂(1548)	→	1549
0₂(949)	→	950
2₃(2069)	→	2070
2₃(2071)	→	2072
2₃(2070)	→	2071
2₃(2044)	→	2045
0₁(373)	→	374
0₁(452)	→	453
0₁(659)	→	660
0₁(431)	→	432
0₁(1279)	→	1280
0₁(467)	→	468
0₁(548)	→	549
0₁(1389)	→	1390
0₁(746)	→	747
0₁(295)	→	296
0₁(1293)	→	1294
0₁(195)	→	196
0₁(818)	→	819
0₁(396)	→	397
0₁(734)	→	735
0₁(547)	→	548
0₁(1817)	→	1818
0₁(706)	→	707
0₁(820)	→	821
0₁(603)	→	604
0₁(1187)	→	1188
0₁(11)	→	12
0₁(1121)	→	1122
0₁(625)	→	626
0₁(1111)	→	1112
0₁(1026)	→	1027
0₁(1819)	→	1820
0₁(1871)	→	1872
0₁(598)	→	599
0₁(14)	→	15
0₁(291)	→	292
0₁(726)	→	727
0₁(368)	→	369
0₁(1432)	→	1433
0₁(1307)	→	1308
0₁(426)	→	427
0₁(793)	→	794
0₁(697)	→	698
0₁(398)	→	399
0₁(374)	→	375
0₁(686)	→	687
0₁(524)	→	525
0₁(566)	→	567
0₁(1510)	→	1511
0₁(450)	→	451
0₁(460)	→	461
0₁(470)	→	471
0₁(1253)	→	1254
0₁(86)	→	87
0₁(542)	→	543
0₁(464)	→	465
0₁(1175)	→	1176
0₁(456)	→	457
0₁(197)	→	198
0₁(437)	→	438
0₁(1533)	→	1534
0₁(10)	→	11
0₁(424)	→	425
0₁(1233)	→	1234
0₁(550)	→	551
0₁(1250)	→	1251
0₁(742)	→	743
0₁(118)	→	119
0₁(1815)	→	1816
0₁(1228)	→	1229
0₁(631)	→	632
0₁(461)	→	462
0₁(1287)	→	1288
0₁(302)	→	303
0₁(1182)	→	1183
0₁(15)	→	16
0₁(1530)	→	1531
0₁(1024)	→	1025
0₁(1229)	→	1230
0₁(502)	→	503
0₁(1821)	→	1822
0₁(199)	→	200
0₁(1280)	→	1281
0₁(683)	→	684
0₁(626)	→	627
0₁(458)	→	459
0₁(656)	→	657
0₁(1113)	→	1114
0₁(681)	→	682
0₁(116)	→	117
0₁(815)	→	816
0₁(504)	→	505
0₁(522)	→	523
0₁(422)	→	423
0₁(1535)	→	1536
0₁(1289)	→	1290
0₁(1291)	→	1292
0₁(307)	→	308
0₁(789)	→	790
0₁(1237)	→	1238
0₀(3)	→	5
0₀(6)	→	5
0₀(5)	→	5
0₀(4)	→	5
0₀(2)	→	5
0₀(1)	→	5
0₃(2046)	→	2047
0₃(2051)	→	2052
0₃(2068)	→	2069
0₃(2089)	→	2090
0₃(2091)	→	2092
0₃(2047)	→	2048
0₃(2087)	→	2088
0₃(2050)	→	2051
1₃(2072)	→	2073
1₃(2049)	→	2050
1₃(2052)	→	2053
4₀(2)	→	6
4₀(6)	→	6
4₀(4)	→	6
4₀(1)	→	6
4₀(3)	→	6
4₀(5)	→	6
2₂(1615)	→	1616
2₂(1647)	→	1648
2₂(1907)	→	1908
2₂(2290)	→	2291
2₂(2298)	→	2299
2₂(2296)	→	2297
2₂(1905)	→	1906
2₂(1545)	→	1546
2₂(1015)	→	1016
2₂(924)	→	925
2₂(2062)	→	2063
2₂(1656)	→	1657
2₂(2173)	→	2174
2₂(999)	→	1000
2₂(2233)	→	2234
2₂(1621)	→	1622
2₂(989)	→	990
2₂(1999)	→	2000
2₂(987)	→	988
2₂(1543)	→	1544
2₂(1587)	→	1588
2₂(898)	→	899
2₂(1047)	→	1048
2₂(1666)	→	1667
2₂(1895)	→	1896
2₂(971)	→	972
2₂(2180)	→	2181
2₂(2176)	→	2177
2₂(1929)	→	1930
2₂(946)	→	947
2₂(2063)	→	2064
2₂(1832)	→	1833
2₂(1623)	→	1624
2₂(1614)	→	1615
2₂(1629)	→	1630
2₂(1801)	→	1802
2₂(2061)	→	2062
2₂(1001)	→	1002
2₂(1834)	→	1835
2₂(846)	→	847
2₂(857)	→	858
2₂(1855)	→	1856
2₂(973)	→	974
2₂(1665)	→	1666
2₂(1054)	→	1055
2₂(1894)	→	1895
2₂(1937)	→	1938
2₂(1017)	→	1018
2₂(1622)	→	1623
2₂(1921)	→	1922
2₂(1997)	→	1998
2₂(1646)	→	1647
2₂(1055)	→	1056
2₂(1654)	→	1655
2₂(1923)	→	1924
2₂(988)	→	989
2₂(1143)	→	1144
2₂(1000)	→	1001
2₂(1007)	→	1008
2₂(1203)	→	1204
2₂(1794)	→	1795
2₂(1204)	→	1205
2₂(1823)	→	1824
2₂(1016)	→	1017
2₂(2304)	→	2305
2₂(1797)	→	1798
2₂(1168)	→	1169
2₂(979)	→	980
2₂(1893)	→	1894
2₂(1931)	→	1932
2₂(1009)	→	1010
2₂(1576)	→	1577
2₂(1589)	→	1590
2₂(972)	→	973
2₂(1008)	→	1009
2₂(1613)	→	1614
2₂(2403)	→	2404
2₂(1172)	→	1173
2₂(1655)	→	1656
2₂(1903)	→	1904
2₂(1556)	→	1557
2₂(1600)	→	1601
2₂(1767)	→	1768
2₂(1630)	→	1631
2₂(2428)	→	2429
2₂(980)	→	981
2₂(981)	→	982
2₂(1567)	→	1568
2₂(1139)	→	1140
2₂(1664)	→	1665
2₂(913)	→	914
2₂(1648)	→	1649
2₂(870)	→	871
2₂(1631)	→	1632
3₃(2053)	→	2054
3₃(2067)	→	2068
3₃(2093)	→	2094
3₃(2088)	→	2089
3₃(2094)	→	2095
3₃(2092)	→	2093
1₀(1)	→	4
1₀(6)	→	4
1₀(3)	→	4
1₀(5)	→	4
1₀(2)	→	4
1₀(4)	→	4
2₁(1529)	→	1530
2₁(699)	→	700
2₁(87)	→	88
2₁(1239)	→	1240
2₁(1952)	→	1953
2₁(301)	→	302
2₁(2430)	→	2431
2₁(573)	→	574
2₁(191)	→	192
2₁(8)	→	9
2₁(1309)	→	1310
2₁(296)	→	297
2₁(1458)	→	1459
2₁(427)	→	428
2₁(192)	→	193
2₁(1316)	→	1317
2₁(740)	→	741
2₁(1939)	→	1940
2₁(430)	→	431
2₁(1180)	→	1181
2₁(372)	→	373
2₁(714)	→	715
2₁(476)	→	477
2₁(61)	→	62
2₁(88)	→	89
2₁(826)	→	827
2₁(2306)	→	2307
2₁(1067)	→	1068
2₁(369)	→	370
2₁(59)	→	60
2₁(564)	→	565
2₁(1314)	→	1315
2₁(575)	→	576
2₁(1424)	→	1425
2₁(700)	→	701
2₁(602)	→	603
2₁(433)	→	434
2₁(1958)	→	1959
2₁(2312)	→	2313
2₁(2407)	→	2408
2₁(1962)	→	1963
2₁(376)	→	377
2₁(708)	→	709
2₁(2310)	→	2311
2₁(658)	→	659
2₁(89)	→	90
2₁(83)	→	84
2₁(1954)	→	1955
2₁(1148)	→	1149
2₁(814)	→	815
2₁(40)	→	41
2₁(1393)	→	1394
2₁(721)	→	722
2₁(1236)	→	1237
2₁(1508)	→	1509
2₁(1956)	→	1957
2₁(577)	→	578
2₁(1227)	→	1228
2₁(224)	→	225
2₁(712)	→	713
2₁(1181)	→	1182
2₁(737)	→	738
2₁(1438)	→	1439
2₁(787)	→	788
2₁(691)	→	692
2₁(38)	→	39
2₁(300)	→	301
2₁(228)	→	229
2₁(1960)	→	1961
2₁(1425)	→	1426
2₁(1426)	→	1427
2₁(743)	→	744
2₁(1531)	→	1532
2₁(1066)	→	1067
2₁(435)	→	436
2₁(732)	→	733
2₁(632)	→	633
2₁(477)	→	478
2₁(710)	→	711
2₁(2308)	→	2309
2₁(1231)	→	1232
2₁(816)	→	817
4₁(608)	→	609
4₁(1396)	→	1397
4₁(274)	→	275
4₁(695)	→	696
4₁(606)	→	607
4₁(677)	→	678
4₁(229)	→	230
4₁(565)	→	566
4₁(827)	→	828
4₁(629)	→	630
4₁(297)	→	298
4₁(198)	→	199
4₁(705)	→	706
4₁(2340)	→	2341
4₁(370)	→	371
4₁(12)	→	13
4₁(744)	→	745
4₁(1281)	→	1282
4₁(2426)	→	2427
4₁(1312)	→	1313
4₁(465)	→	466
4₁(610)	→	611
4₁(91)	→	92
4₁(655)	→	656
4₁(741)	→	742
4₁(9)	→	10
4₁(114)	→	115
4₁(2353)	→	2354
4₁(1511)	→	1512
4₁(1025)	→	1026
4₁(1117)	→	1118
4₁(252)	→	253
4₁(308)	→	309
4₁(306)	→	307
4₁(694)	→	695
4₁(745)	→	746
4₁(790)	→	791
4₁(117)	→	118
4₁(727)	→	728
4₁(1889)	→	1890
4₁(722)	→	723
4₁(719)	→	720
4₁(1391)	→	1392
4₁(113)	→	114
4₁(1080)	→	1081
4₁(657)	→	658
4₁(545)	→	546
4₁(1857)	→	1858
4₁(1112)	→	1113
4₁(1863)	→	1864
4₁(1022)	→	1023
4₁(231)	→	232
4₁(623)	→	624
4₁(471)	→	472
4₁(909)	→	910
4₁(1021)	→	1022
4₁(600)	→	601
4₁(1188)	→	1189
4₁(115)	→	116
4₁(272)	→	273
4₁(654)	→	655
4₁(1251)	→	1252
4₁(1429)	→	1430
4₁(226)	→	227
4₁(1030)	→	1031
4₁(1225)	→	1226
4₁(733)	→	734
4₁(688)	→	689
4₁(1186)	→	1187
4₁(1150)	→	1151
4₁(703)	→	704
4₁(675)	→	676
4₁(254)	→	255
4₁(1023)	→	1024
4₁(1431)	→	1432
4₁(597)	→	598
4₁(1760)	→	1761
4₁(203)	→	204
4₁(2288)	→	2289
4₁(112)	→	113
4₁(220)	→	221
2₀(3)	→	2
2₀(5)	→	2
2₀(2)	→	2
2₀(4)	→	2
2₀(1)	→	2
2₀(6)	→	2
3₀(2)	→	3
3₀(4)	→	3
3₀(3)	→	3
3₀(6)	→	3
3₀(1)	→	3
3₀(5)	→	3
3₁(627)	→	628
3₁(1114)	→	1115
3₁(463)	→	464
3₁(346)	→	347
3₁(748)	→	749
3₁(1783)	→	1784
3₁(17)	→	18
3₁(993)	→	994
3₁(568)	→	569
3₁(1534)	→	1535
3₁(771)	→	772
3₁(1446)	→	1447
3₁(823)	→	824
3₁(720)	→	721
3₁(348)	→	349
3₁(716)	→	717
3₁(1179)	→	1180
3₁(1256)	→	1257
3₁(305)	→	306
3₁(1791)	→	1792
3₁(704)	→	705
3₁(1430)	→	1431
3₁(1448)	→	1449
3₁(630)	→	631
3₁(676)	→	677
3₁(85)	→	86
3₁(750)	→	751
3₁(366)	→	367
3₁(1254)	→	1255
3₁(325)	→	326
3₁(549)	→	550
3₁(200)	→	201
3₁(735)	→	736
3₁(1305)	→	1306
3₁(2422)	→	2423
3₁(1395)	→	1396
3₁(1456)	→	1457
3₁(1528)	→	1529
3₁(294)	→	295
3₁(2007)	→	2008
3₁(1185)	→	1186
3₁(196)	→	197
3₁(813)	→	814
3₁(202)	→	203
3₁(299)	→	300
3₁(1115)	→	1116
3₁(478)	→	479
3₁(725)	→	726
3₁(1249)	→	1250
3₁(819)	→	820
3₁(327)	→	328
3₁(1452)	→	1453
3₁(1119)	→	1120
3₁(1116)	→	1117
3₁(1110)	→	1111
3₁(1785)	→	1786
3₁(468)	→	469
3₁(736)	→	737
3₁(773)	→	774
3₁(724)	→	725
3₁(1366)	→	1367
3₁(995)	→	996
3₁(599)	→	600
3₁(679)	→	680
3₁(551)	→	552
3₁(1358)	→	1359
3₁(693)	→	694
3₁(739)	→	740
3₁(1194)	→	1195
3₁(546)	→	547
3₁(604)	→	605
3₁(201)	→	202
4₃(2073)	→	2074
4₃(2090)	→	2091
4₃(2045)	→	2046
4₃(2048)	→	2049
4₃(2095)	→	2096
1₁(1226)	→	1227
1₁(1152)	→	1153
1₁(1506)	→	1507
1₁(685)	→	686
1₁(1311)	→	1312
1₁(687)	→	688
1₁(795)	→	796
1₁(1248)	→	1249
1₁(434)	→	435
1₁(190)	→	191
1₁(428)	→	429
1₁(16)	→	17
1₁(696)	→	697
1₁(574)	→	575
1₁(1512)	→	1513
1₁(1147)	→	1148
1₁(188)	→	189
1₁(371)	→	372
1₁(1027)	→	1028
1₁(223)	→	224
1₁(791)	→	792
1₁(466)	→	467
1₁(1865)	→	1866
1₁(111)	→	112
1₁(718)	→	719
1₁(1315)	→	1316
1₁(293)	→	294
1₁(1283)	→	1284
1₁(731)	→	732
1₁(222)	→	223
1₁(144)	→	145
1₁(122)	→	123
1₁(1240)	→	1241
1₁(1454)	→	1455
1₁(682)	→	683
1₁(785)	→	786
1₁(13)	→	14
1₁(1284)	→	1285
1₁(225)	→	226
1₁(801)	→	802
1₁(817)	→	818
1₁(1532)	→	1533
1₁(799)	→	800
1₁(1285)	→	1286
1₁(1146)	→	1147
1₁(90)	→	91
1₁(678)	→	679
1₁(193)	→	194
1₁(563)	→	564
1₁(1260)	→	1261
1₁(1162)	→	1163
1₁(292)	→	293
1₁(1238)	→	1239
1₁(1068)	→	1069
1₁(221)	→	222
1₁(1063)	→	1064
1₁(120)	→	121
1₁(168)	→	169
1₁(2013)	→	2014
1₁(1160)	→	1161
1₁(544)	→	545
1₁(304)	→	305
1₁(1028)	→	1029
1₁(432)	→	433
1₁(475)	→	476
1₁(166)	→	167
1₁(1252)	→	1253
1₁(146)	→	147
1₁(660)	→	661
1₁(1184)	→	1185
1₁(2355)	→	2356
1₁(1149)	→	1150
1₁(473)	→	474
1₁(628)	→	629
1₁(792)	→	793
1₁(684)	→	685
1₁(1177)	→	1178
1₁(1513)	→	1514
1₁(825)	→	826
1₁(1065)	→	1066
1₁(578)	→	579
1₁(717)	→	718
1₁(728)	→	729
1₁(462)	→	463
1₁(474)	→	475
1₁(1988)	→	1989
1₁(119)	→	120
1₂(1051)	→	1052
1₂(2029)	→	2030
1₂(1824)	→	1825
1₂(932)	→	933
1₂(2150)	→	2151
1₂(1207)	→	1208
1₂(1169)	→	1170
1₂(1764)	→	1765
1₂(2064)	→	2065
1₂(1018)	→	1019
1₂(851)	→	852
1₂(1040)	→	1041
1₂(862)	→	863
1₂(1136)	→	1137
1₂(1550)	→	1551
1₂(2241)	→	2242
1₂(1167)	→	1168
1₂(1166)	→	1167
1₂(1624)	→	1625
1₂(1741)	→	1742
1₂(921)	→	922
1₂(951)	→	952
1₂(1570)	→	1571
1₂(854)	→	855
1₂(929)	→	930
1₂(1165)	→	1166
1₂(1010)	→	1011
1₂(906)	→	907
1₂(1002)	→	1003
1₂(1685)	→	1686
1₂(1616)	→	1617
1₂(1632)	→	1633
1₂(954)	→	955
1₂(1847)	→	1848
1₂(1138)	→	1139
1₂(1032)	→	1033
1₂(918)	→	919
1₂(1056)	→	1057
1₂(2232)	→	2233
1₂(1045)	→	1046
1₂(865)	→	866
1₂(982)	→	983
1₂(1849)	→	1850
1₂(1597)	→	1598
1₂(1687)	→	1688
1₂(1041)	→	1042
1₂(1573)	→	1574
1₂(1691)	→	1692
1₂(1667)	→	1668
1₂(1657)	→	1658
1₂(2026)	→	2027
1₂(1796)	→	1797
1₂(2175)	→	2176
1₂(1649)	→	1650
1₂(1608)	→	1609
1₂(1553)	→	1554
1₂(2000)	→	2001
1₂(974)	→	975
1₂(1763)	→	1764
1₂(1605)	→	1606
1₂(990)	→	991
1₂(1053)	→	1054
1₂(1594)	→	1595
1₂(1564)	→	1565
1₂(1561)	→	1562
1₂(1581)	→	1582
1₂(1584)	→	1585
1₂(1043)	→	1044
1₂(903)	→	904
1₂(1140)	→	1141
1₂(1670)	→	1671
1₂(2393)	→	2394
1₂(1137)	→	1138
5₀(1)	→	1
5₀(6)	→	1
5₀(5)	→	1
5₀(2)	→	1
5₀(3)	→	1
5₀(4)	→	1
3₂(2237)	→	2238
3₂(2121)	→	2122
3₂(1554)	→	1555
3₂(1662)	→	1663
3₂(922)	→	923
3₂(855)	→	856
3₂(1013)	→	1014
3₂(1005)	→	1006
3₂(2119)	→	2120
3₂(1565)	→	1566
3₂(955)	→	956
3₂(2030)	→	2031
3₂(997)	→	998
3₂(907)	→	908
3₂(1202)	→	1203
3₂(2002)	→	2003
3₂(2125)	→	2126
3₂(1089)	→	1090
3₂(1574)	→	1575
3₂(1132)	→	1133
3₂(1899)	→	1900
3₂(969)	→	970
3₂(1106)	→	1107
3₂(1652)	→	1653
3₂(1644)	→	1645
3₂(1725)	→	1726
3₂(1726)	→	1727
3₂(1831)	→	1832
3₂(1720)	→	1721
3₂(1105)	→	1106
3₂(1619)	→	1620
3₂(1809)	→	1810
3₂(2059)	→	2060
3₂(1829)	→	1830
3₂(1710)	→	1711
3₂(2115)	→	2116
3₂(1609)	→	1610
3₂(1996)	→	1997
3₂(1083)	→	1084
3₂(1126)	→	1127
3₂(977)	→	978
3₂(1709)	→	1710
3₂(2424)	→	2425
3₂(1611)	→	1612
3₂(1826)	→	1827
3₂(985)	→	986
3₂(1585)	→	1586
3₂(1765)	→	1766
3₂(866)	→	867
3₂(1724)	→	1725
3₂(1131)	→	1132
3₂(2131)	→	2132
3₂(1704)	→	1705
3₂(1087)	→	1088
3₂(1101)	→	1102
3₂(2129)	→	2130
3₂(1708)	→	1709
3₂(1627)	→	1628
3₂(2130)	→	2131
3₂(1088)	→	1089
3₂(1208)	→	1209
3₂(1107)	→	1108
3₂(1598)	→	1599
3₂(2120)	→	2121
3₂(933)	→	934
3₂(1130)	→	1131

The automaton is closed under rewriting as it is compatible.