Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3817)

The rewrite relation of the following TRS is considered.

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

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(0(0(x1))))	→	5(2(2(1(0(2(2(0(3(1(x1))))))))))	(50)
2(4(1(2(x1))))	→	2(3(3(2(1(4(0(1(2(3(x1))))))))))	(51)
0(4(3(2(x1))))	→	4(4(2(3(1(4(3(1(4(2(x1))))))))))	(52)
0(4(2(5(x1))))	→	0(0(1(4(0(3(3(1(1(5(x1))))))))))	(53)
3(2(0(0(0(x1)))))	→	1(1(1(2(2(0(3(3(1(2(x1))))))))))	(54)
2(0(5(1(0(x1)))))	→	2(2(0(1(0(1(5(4(5(0(x1))))))))))	(55)
4(1(1(2(0(x1)))))	→	4(0(1(3(0(3(2(2(0(1(x1))))))))))	(56)
4(4(3(1(1(x1)))))	→	4(0(3(1(4(3(4(5(4(2(x1))))))))))	(57)
4(4(4(1(1(x1)))))	→	4(5(3(3(3(2(1(2(1(2(x1))))))))))	(58)
2(4(2(4(1(x1)))))	→	2(0(3(1(3(2(5(5(2(1(x1))))))))))	(59)
4(4(3(1(5(x1)))))	→	4(3(4(2(2(0(1(1(0(1(x1))))))))))	(60)
0(4(3(2(5(x1)))))	→	0(2(2(0(3(0(1(2(1(5(x1))))))))))	(61)
0(4(1(5(5(x1)))))	→	5(4(3(3(4(1(4(0(1(2(x1))))))))))	(62)
1(4(1(1(0(0(x1))))))	→	1(4(2(2(5(0(3(0(1(2(x1))))))))))	(63)
3(0(5(1(0(0(x1))))))	→	3(0(3(3(2(2(1(0(1(2(x1))))))))))	(64)
2(4(3(2(0(0(x1))))))	→	3(0(1(4(3(5(2(3(1(2(x1))))))))))	(65)
0(0(4(3(0(0(x1))))))	→	4(2(2(2(4(2(1(3(0(1(x1))))))))))	(66)
1(0(2(2(4(1(x1))))))	→	1(0(4(5(4(5(1(4(0(1(x1))))))))))	(67)
2(0(4(3(3(2(x1))))))	→	0(2(3(3(4(0(3(5(5(2(x1))))))))))	(68)
0(0(4(1(1(3(x1))))))	→	4(5(5(0(2(0(1(1(0(3(x1))))))))))	(69)
4(1(5(5(4(3(x1))))))	→	4(2(1(4(5(1(2(2(1(4(x1))))))))))	(70)
1(1(5(0(0(5(x1))))))	→	2(3(1(4(2(0(3(3(5(2(x1))))))))))	(71)
0(5(5(5(0(5(x1))))))	→	0(3(4(0(1(4(5(4(0(5(x1))))))))))	(72)
2(0(0(2(0(0(0(x1)))))))	→	2(1(3(5(5(2(1(3(1(2(x1))))))))))	(73)
3(4(1(3(0(0(0(x1)))))))	→	4(5(5(4(4(2(0(0(1(1(x1))))))))))	(74)
3(5(0(4(2(0(0(x1)))))))	→	5(1(4(0(5(2(3(5(3(0(x1))))))))))	(75)
5(5(4(5(3(0(0(x1)))))))	→	5(0(3(4(2(2(1(0(1(2(x1))))))))))	(76)
3(4(4(1(5(1(0(x1)))))))	→	1(0(3(4(0(4(1(4(5(3(x1))))))))))	(77)
2(0(0(5(0(2(0(x1)))))))	→	0(3(0(5(2(3(0(2(3(0(x1))))))))))	(78)
0(4(2(4(2(5(0(x1)))))))	→	0(0(1(2(3(3(2(4(5(2(x1))))))))))	(79)
5(5(5(5(1(3(1(x1)))))))	→	3(1(4(5(4(0(5(1(2(1(x1))))))))))	(80)
2(0(4(3(2(0(2(x1)))))))	→	5(2(4(3(5(0(4(0(1(2(x1))))))))))	(81)
5(0(0(4(2(0(2(x1)))))))	→	5(1(2(1(2(3(0(1(0(2(x1))))))))))	(82)
5(0(2(2(4(1(2(x1)))))))	→	5(1(2(1(4(2(0(2(0(1(x1))))))))))	(83)
1(5(2(5(4(1(2(x1)))))))	→	1(3(1(2(1(3(4(5(4(0(x1))))))))))	(84)
3(3(5(3(5(3(2(x1)))))))	→	3(5(2(0(1(4(0(1(0(2(x1))))))))))	(85)
4(4(1(4(5(3(2(x1)))))))	→	4(3(4(3(1(2(1(1(1(3(x1))))))))))	(86)
0(4(1(1(4(1(3(x1)))))))	→	0(0(2(1(3(0(2(1(4(0(x1))))))))))	(87)
2(4(5(3(4(1(3(x1)))))))	→	2(4(0(2(2(0(1(0(1(1(x1))))))))))	(88)
5(0(4(3(3(2(3(x1)))))))	→	5(0(1(4(5(5(0(0(1(0(x1))))))))))	(89)
3(2(0(5(2(4(3(x1)))))))	→	4(3(1(4(2(2(3(3(5(3(x1))))))))))	(90)
0(4(3(4(3(4(3(x1)))))))	→	0(2(1(3(3(1(4(0(3(0(x1))))))))))	(91)
0(4(2(5(3(4(3(x1)))))))	→	0(5(0(4(1(4(0(3(3(3(x1))))))))))	(92)
1(5(0(0(4(4(3(x1)))))))	→	3(5(4(5(1(2(0(1(0(3(x1))))))))))	(93)
1(5(3(3(5(0(5(x1)))))))	→	1(2(1(4(2(0(1(1(3(5(x1))))))))))	(94)
2(2(4(4(4(1(5(x1)))))))	→	0(1(5(3(1(4(5(3(3(1(x1))))))))))	(95)
1(5(5(4(4(1(5(x1)))))))	→	3(3(4(0(0(1(1(0(1(4(x1))))))))))	(96)
1(3(4(5(1(5(5(x1)))))))	→	1(2(0(1(1(4(2(2(1(1(x1))))))))))	(97)
0(0(4(1(5(5(5(x1)))))))	→	4(5(1(0(5(0(3(0(1(1(x1))))))))))	(98)

1.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:

2207	→	2399
2207	→	2409
1303	→	773
1793	→	9
279	→	230
2073	→	882
239	→	3
239	→	870
239	→	715
239	→	341
239	→	795
239	→	366
239	→	351
239	→	2346
366	→	341
366	→	795
871	→	859
871	→	68
871	→	4
871	→	784
871	→	867
871	→	2126
871	→	2080
871	→	1832
1268	→	525
2042	→	859
867	→	859
846	→	826
1627	→	859
1652	→	872
899	→	890
2119	→	951
2119	→	2134
869	→	859
102	→	1017
102	→	1533
102	→	1549
1191	→	1013
486	→	1259
486	→	1678
1751	→	931
1138	→	1127
789	→	2199
589	→	1443
589	→	2183
2381	→	94
1056	→	344
967	→	623
2268	→	1233
1117	→	398
1117	→	1750
1117	→	1778
715	→	1916
715	→	2019
715	→	2029
2246	→	441
103	→	2
103	→	606
103	→	164
103	→	228
103	→	1818
103	→	1922
103	→	1820
103	→	1870
103	→	1099
794	→	787
1787	→	962
1624	→	1966
1624	→	2193
2141	→	962
897	→	238
1475	→	760
2349	→	2401
2349	→	2407
809	→	796
809	→	832
10	→	931
1691	→	882
2208	→	2380
2208	→	2382
2208	→	2411
2208	→	2417
1487	→	922
1487	→	230
1487	→	660
1487	→	296
1487	→	120
1487	→	41
1487	→	189
1487	→	350
1487	→	1
1487	→	297
1487	→	1250
487	→	406
487	→	1651
487	→	1707
487	→	1725
1864	→	326
1864	→	1930
640	→	617
2135	→	962
1250	→	608
2105	→	525
781	→	2
781	→	782
781	→	326
781	→	164
781	→	228
781	→	1922
781	→	1820
781	→	1870
1121	→	398
1121	→	1758
1121	→	1776
1473	→	17
96	→	1488
1642	→	859
383	→	341
383	→	806
383	→	868
2211	→	2200
608	→	1114
1544	→	1536
2396	→	795
2396	→	2346
1593	→	804
1593	→	2351
2133	→	951
2133	→	2148
1363	→	910
1363	→	750
1363	→	889
1363	→	616
1363	→	923
1363	→	674
1363	→	276
1363	→	143
1363	→	8
1363	→	209
1363	→	340
1363	→	5
1363	→	94
1363	→	748
1363	→	121
1363	→	1657
1363	→	1959
1363	→	609
728	→	17
811	→	796
811	→	847
2040	→	859
956	→	1061
1909	→	525
706	→	951
706	→	1026
511	→	519
511	→	542
1625	→	525
1625	→	1815
1923	→	680
299	→	1875
878	→	1257
878	→	1676
878	→	2253
1870	→	326
1870	→	1922
1532	→	398
1724	→	488
1724	→	705
1724	→	398
1724	→	4
1724	→	9
1724	→	42
1724	→	231
1724	→	1793
1953	→	739
2097	→	525
2054	→	2191
2054	→	2320
18	→	1
18	→	922
18	→	230
18	→	760
18	→	680
18	→	607
18	→	259
18	→	297
18	→	342
18	→	257
624	→	172
2402	→	398
1098	→	2162
1098	→	2332
1098	→	2345
365	→	1952
41	→	1821
3	→	67
3	→	161
3	→	227
3	→	256
3	→	367
3	→	678
2335	→	795
1362	→	1853
1362	→	1863
1362	→	2112
1362	→	2269
2063	→	882
988	→	969
988	→	1077
382	→	1944
772	→	2210
1254	→	623
817	→	548
1789	→	962
1812	→	298
1812	→	1972
2149	→	962
1119	→	398
1119	→	1752
1119	→	1780
805	→	796
805	→	825
1258	→	525
646	→	617
1840	→	398
1840	→	2088
1840	→	2120
2252	→	441
919	→	4
919	→	488
919	→	705
919	→	398
919	→	9
919	→	42
919	→	231
919	→	1793
1467	→	739
9	→	398
9	→	463
9	→	705
1706	→	890
1714	→	892
1931	→	680
1931	→	2245
5	→	8
5	→	143
5	→	209
5	→	276
5	→	340
5	→	674
774	→	1
774	→	922
774	→	230
774	→	297
774	→	1250
1629	→	859
341	→	715
341	→	810
341	→	870
2002	→	795
2030	→	344
584	→	1523
95	→	1470
515	→	1255
515	→	1906
515	→	2355
642	→	617
671	→	661
671	→	676
671	→	278
671	→	93
671	→	43
671	→	163
671	→	365
671	→	6
671	→	673
1524	→	1515
1076	→	1063
1076	→	1513
2103	→	525
1027	→	233
1681	→	882
2215	→	2200
1664	→	608
618	→	912
1252	→	617
765	→	236
325	→	299
1806	→	2349
2358	→	608
749	→	740
749	→	872
1965	→	739
673	→	661
1031	→	1198
1031	→	1325
445	→	1069
446	→	102
495	→	238
1890	→	607
1068	→	937
2018	→	804
2018	→	2041
2018	→	2062
2354	→	608
1668	→	548
938	→	614
1601	→	804
1601	→	1641
1601	→	1690
1599	→	804
1599	→	1628
1599	→	1688
1530	→	398
2057	→	608
1	→	41
1	→	120
1	→	189
1	→	296
1	→	350
1	→	660
123	→	94
123	→	641
123	→	902
1471	→	754
1791	→	962
1726	→	1716
826	→	2267
2406	→	326
1907	→	1892
1078	→	1063
1078	→	1521
1591	→	819
1040	→	1029
1040	→	1474
2055	→	525
2055	→	2166
877	→	2229
1009	→	1468
1957	→	739
2244	→	17
305	→	1112
2113	→	525
716	→	752
716	→	882
716	→	162
716	→	5
549	→	5
549	→	882
549	→	162
549	→	752
549	→	716
549	→	144
549	→	890
549	→	911
549	→	874
549	→	1660
549	→	1947
549	→	1955
165	→	408
1489	→	768
833	→	826
1994	→	398
2418	→	795
969	→	1226
969	→	1327
1838	→	398
1838	→	2086
1838	→	2132
101	→	1624
778	→	1665
1185	→	1189
2228	→	2200
1753	→	931
688	→	4
688	→	706
688	→	70
688	→	232
688	→	1996
2424	→	705
2024	→	344
548	→	1261
548	→	1606
548	→	1620
747	→	306
747	→	1057
590	→	525
590	→	1053
44	→	9
44	→	4
1283	→	1271
1283	→	2251
1278	→	1794
1278	→	1993
1278	→	2001
723	→	1118
723	→	1149
723	→	1770
723	→	2271
2331	→	398
677	→	661
1996	→	398
609	→	1657
1607	→	804
1607	→	1643
1607	→	1680
1522	→	1514
751	→	740
751	→	880
2044	→	859
1683	→	882
687	→	1015
687	→	1531
687	→	1543
881	→	873
881	→	1368
1070	→	1062
1807	→	2160
1807	→	2164
1807	→	2330
1807	→	2334
297	→	230
675	→	661
1030	→	1184
556	→	1267
556	→	1600
556	→	1618
2243	→	2403
2243	→	2421
662	→	943
662	→	1024
1099	→	164
1099	→	670
1099	→	258
1099	→	141
1099	→	91
1099	→	207
1099	→	384
1099	→	2
1099	→	1818
518	→	3
518	→	870
518	→	715
518	→	341
518	→	795
518	→	366
512	→	775
2238	→	17
2333	→	398
208	→	164
349	→	102
385	→	341
385	→	808
385	→	866
2087	→	931
890	→	1713
1127	→	1290
1917	→	525
1723	→	1920
1723	→	2015
1723	→	2023
1277	→	2054
614	→	989
614	→	1041
614	→	1454
614	→	2158
407	→	6
407	→	661
407	→	673
407	→	677
1528	→	787
526	→	4
526	→	705
526	→	398
526	→	662
526	→	9
526	→	44
526	→	871
526	→	488
526	→	42
526	→	231
526	→	819
526	→	344
526	→	2030
526	→	1793
824	→	485
1921	→	525
2155	→	992
257	→	230
257	→	660
257	→	296
257	→	120
257	→	41
257	→	189
257	→	350
257	→	1
257	→	297
257	→	1250
173	→	3
173	→	870
173	→	715
173	→	341
173	→	795
173	→	366
173	→	368
173	→	2020
1830	→	398
1830	→	2078
1830	→	2118
918	→	1265
918	→	1598
918	→	1616
911	→	890
788	→	1809
788	→	2326
679	→	661
121	→	94
121	→	616
121	→	748
121	→	889
277	→	230
648	→	617
1477	→	760
2071	→	882
6	→	43
6	→	93
6	→	163
6	→	278
6	→	365
6	→	676
773	→	1263
773	→	1490
773	→	1608
773	→	1622
1256	→	525
792	→	1253
1336	→	910
1336	→	750
1336	→	5
1336	→	647
1336	→	818
1336	→	94
1336	→	1953
1042	→	1029
1042	→	1476
2081	→	931
1356	→	1456
2213	→	2200
823	→	1667
384	→	1956
1037	→	1823
1818	→	164
1824	→	164
2065	→	882
1234	→	436
2111	→	525
2200	→	2275
1205	→	782
1205	→	326
1205	→	670
1205	→	258
1205	→	141
1205	→	91
1205	→	207
1205	→	384
1205	→	2
1205	→	606
1205	→	164
1205	→	1818
237	→	968
237	→	991
237	→	1028
1585	→	819
1279	→	706
1279	→	70
1279	→	4
1279	→	232
1279	→	1996
2412	→	398
230	→	689
230	→	922
230	→	1249
230	→	2273
2153	→	992
2400	→	398
615	→	2
615	→	782
615	→	326
615	→	164
615	→	228
615	→	208
615	→	1922
615	→	1820
615	→	1870
615	→	1924
615	→	1872
368	→	341
1101	→	164
1355	→	1742
2010	→	804
2010	→	2039
2010	→	2070
2274	→	436
831	→	237
350	→	1792
350	→	1811
350	→	1958
350	→	2154
2022	→	344
437	→	406
525	→	1098
923	→	1659
1188	→	348
803	→	525
803	→	1251
1014	→	949
1014	→	1421
1014	→	1889
1036	→	1825
2	→	91
2	→	141
2	→	207
2	→	258
2	→	384
2	→	670
2329	→	398
2161	→	94
2165	→	164
686	→	1649
1679	→	548
4	→	69
4	→	122
4	→	191
4	→	229
4	→	382
4	→	672
1291	→	680
1018	→	1008
1018	→	1584
1150	→	1127
1150	→	1282
1945	→	739
400	→	791
400	→	1727
582	→	172
1650	→	525
1650	→	1813
1621	→	705
1779	→	951
1779	→	1786
258	→	1837
258	→	1871
258	→	2104
557	→	2
557	→	782
557	→	326
557	→	606
557	→	164
557	→	1818
1761	→	931
520	→	1527
1666	→	608
1001	→	760
1001	→	680
1001	→	607
1001	→	1923
300	→	550
300	→	698
1550	→	1536
1854	→	398
1854	→	2094
1854	→	2124
1814	→	342
802	→	1478
802	→	1592
802	→	1614
820	→	1744
2147	→	962
2209	→	1818
2209	→	2104
2209	→	1837
2209	→	670
2209	→	258
2209	→	141
2209	→	91
2209	→	207
2209	→	384
2209	→	2
2209	→	1099
704	→	102
2184	→	398
2254	→	17
1773	→	525
2230	→	2200
1491	→	95
1491	→	2237
2346	→	795
1872	→	326
1872	→	1924
1915	→	525
306	→	1100
1125	→	491
1925	→	680
1369	→	719
1743	→	924
2350	→	525
2350	→	2397
1856	→	326
1856	→	1932
1901	→	1055
1901	→	661
1901	→	673
759	→	614
2038	→	859
2004	→	795
2327	→	398
1771	→	525
1455	→	739
1517	→	2056
1832	→	398
1832	→	2080
1832	→	2126
697	→	238
746	→	1466
2352	→	859
1013	→	2386
1939	→	680
1623	→	705
1878	→	543
2192	→	398
2237	→	2405
2237	→	2423
724	→	5
724	→	910
724	→	750
724	→	889
724	→	616
724	→	923
724	→	94
724	→	748
724	→	121
724	→	1657
724	→	1959
724	→	609
1204	→	1914
1204	→	2017
1204	→	2025
1326	→	699
1038	→	910
1038	→	750
1038	→	898
1038	→	94
1038	→	674
1038	→	276
1038	→	143
1038	→	8
1038	→	209
1038	→	340
1038	→	5
1038	→	639
1038	→	142
1038	→	739
1038	→	1957
42	→	9
42	→	4
42	→	992
42	→	2155
2163	→	94
957	→	929
1816	→	342
1133	→	1891
1133	→	1908
1133	→	2357
2079	→	931
162	→	94
950	→	918
950	→	2353
1795	→	94
1541	→	1798
1541	→	2328
2186	→	398
1745	→	926
231	→	488
2127	→	951
2127	→	2146
990	→	969
990	→	1075
2270	→	804
707	→	851
707	→	962
256	→	1831
256	→	1869
256	→	2102
2408	→	739
1975	→	95
1975	→	2243
2194	→	398
414	→	405
2139	→	962
905	→	890
1025	→	167
17	→	1122
17	→	1151
17	→	1774
1644	→	859
1822	→	164
727	→	1472
1609	→	804
1609	→	1626
1609	→	1682
190	→	164
190	→	324
714	→	5
714	→	910
714	→	750
714	→	647
714	→	818
714	→	94
714	→	898
714	→	639
714	→	142
714	→	1953
714	→	1957
896	→	1269
1486	→	1918
1486	→	1974
1486	→	2009
1486	→	2021
164	→	326
164	→	606
164	→	782
1136	→	870
1136	→	715
1136	→	341
1136	→	678
1136	→	256
1136	→	161
1136	→	67
1136	→	227
1136	→	367
1136	→	3
1136	→	795
1136	→	366
1361	→	2214
1260	→	525
68	→	9
870	→	1819
2404	→	326
1933	→	680
462	→	439
1919	→	525
464	→	439
2383	→	164
517	→	1120
517	→	1126
517	→	1772
1862	→	326
1862	→	1938
2026	→	344
2095	→	931
1266	→	525
1469	→	754
1457	→	741
865	→	727
1677	→	548
1054	→	342
1422	→	696
722	→	2227
340	→	1954
142	→	94
142	→	639
142	→	898
1058	→	342
1227	→	575
1708	→	890
1619	→	705
1264	→	525
259	→	230
259	→	760
259	→	1
259	→	680
259	→	607
259	→	1923
848	→	826
848	→	1232
1649	→	1964
1649	→	2185
1959	→	739
1660	→	874
92	→	9
92	→	461
1285	→	1271
1285	→	2235
790	→	17
790	→	2265
1955	→	739
2422	→	705
399	→	480
399	→	575
399	→	583
2272	→	804
1444	→	739
807	→	796
807	→	845
1520	→	782
1520	→	326
1520	→	2
1520	→	164
1520	→	228
1520	→	1922
1520	→	1820
1520	→	1870
1947	→	739
903	→	890
1113	→	164
2125	→	951
2125	→	2140
351	→	341
351	→	804
351	→	858
351	→	678
351	→	256
351	→	161
351	→	67
351	→	227
351	→	367
351	→	3
351	→	690
1775	→	525
1016	→	1008
1016	→	1590
367	→	1946
2410	→	93
144	→	94
144	→	645
144	→	739
144	→	904
2159	→	992
43	→	1817
1759	→	931
1783	→	951
1783	→	1790
1785	→	962
1967	→	739
1876	→	519
1876	→	1877
1777	→	951
1777	→	1784
210	→	164
210	→	298
669	→	406
1781	→	951
1781	→	1788
785	→	812
1152	→	1127
1152	→	1284
888	→	494
1826	→	164
1973	→	760
2398	→	342
1689	→	882
767	→	1124
70	→	9
70	→	438
1615	→	705
930	→	525
1797	→	94
1658	→	874
929	→	1007
929	→	1529
929	→	1535
576	→	739
576	→	1947
2020	→	804
2020	→	2043
2020	→	2064
798	→	1300
439	→	766
975	→	348
2284	→	784
2016	→	804
2016	→	2037
2016	→	2072
1485	→	2212
1123	→	398
1123	→	1760
1123	→	1782
1810	→	1799
94	→	647
94	→	750
94	→	818
94	→	910
2356	→	608
191	→	1796
191	→	1995
191	→	2003
192	→	164
192	→	91
192	→	207
192	→	384
192	→	670
192	→	258
192	→	141
192	→	2
192	→	1818
780	→	1116
780	→	1137
780	→	1766
2121	→	951
2121	→	2138
1617	→	705
661	→	1055
2236	→	441
327	→	299
327	→	430
327	→	510
2167	→	342
607	→	680
607	→	760
228	→	164
1262	→	525
238	→	987
238	→	1039
238	→	1354
238	→	2152
1135	→	1829
1135	→	1855
1135	→	2096
2266	→	810
1542	→	772
1820	→	164
879	→	713
879	→	1663
879	→	1705
879	→	1715
1534	→	398
2321	→	739
857	→	102
1808	→	164
1808	→	1099
545	→	725
1115	→	442
2089	→	931
1728	→	915
1767	→	525
307	→	5
307	→	910
307	→	750
307	→	898
307	→	94
307	→	639
307	→	142
307	→	739
307	→	1957
307	→	1953
1519	→	1839
1519	→	1861
1519	→	2110
0₁(614)	→	615
0₁(727)	→	728
0₁(1328)	→	1329
0₁(482)	→	483
0₁(350)	→	351
0₁(694)	→	695
0₁(384)	→	385
0₁(1624)	→	1625
0₁(1543)	→	1544
0₁(2138)	→	2139
0₁(1470)	→	1471
0₁(753)	→	754
0₁(2017)	→	2018
0₁(965)	→	966
0₁(547)	→	548
0₁(2019)	→	2020
0₁(234)	→	235
0₁(891)	→	892
0₁(520)	→	521
0₁(1875)	→	1876
0₁(2265)	→	2266
0₁(10)	→	11
0₁(639)	→	640
0₁(912)	→	913
0₁(445)	→	446
0₁(689)	→	690
0₁(963)	→	964
0₁(895)	→	896
0₁(1251)	→	1252
0₁(1184)	→	1185
0₁(1273)	→	1274
0₁(947)	→	948
0₁(2009)	→	2010
0₁(1359)	→	1360
0₁(2001)	→	2002
0₁(555)	→	556
0₁(1600)	→	1601
0₁(2269)	→	2270
0₁(1717)	→	1718
0₁(1124)	→	1125
0₁(1608)	→	1609
0₁(398)	→	399
0₁(238)	→	239
0₁(859)	→	860
0₁(682)	→	683
0₁(490)	→	491
0₁(1523)	→	1524
0₁(1744)	→	1745
0₁(791)	→	792
0₁(2054)	→	2055
0₁(1784)	→	1785
0₁(2334)	→	2335
0₁(1592)	→	1593
0₁(1676)	→	1677
0₁(2015)	→	2016
0₁(1075)	→	1076
0₁(2140)	→	2141
0₁(405)	→	406
0₁(1481)	→	1482
0₁(645)	→	646
0₁(647)	→	648
0₁(616)	→	617
0₁(1010)	→	1011
0₁(946)	→	947
0₁(1786)	→	1787
0₁(943)	→	944
0₁(1062)	→	1063
0₁(814)	→	815
0₁(510)	→	511
0₁(882)	→	883
0₁(743)	→	744
0₁(1678)	→	1679
0₁(1598)	→	1599
0₁(860)	→	861
0₁(340)	→	341
0₁(96)	→	97
0₁(1203)	→	1204
0₁(365)	→	366
0₁(609)	→	610
0₁(1649)	→	1650
0₁(589)	→	590
0₁(301)	→	302
0₁(970)	→	971
0₁(2134)	→	2135
0₁(1715)	→	1716
0₁(2146)	→	2147
0₁(852)	→	853
0₁(2345)	→	2346
0₁(720)	→	721
0₁(775)	→	776
0₁(2349)	→	2350
0₁(1226)	→	1227
0₁(367)	→	368
0₁(1066)	→	1067
0₁(768)	→	769
0₁(1713)	→	1714
0₁(13)	→	14
0₁(402)	→	403
0₁(1329)	→	1330
0₁(347)	→	348
0₁(827)	→	828
0₁(2148)	→	2149
0₁(1606)	→	1607
0₁(1468)	→	1469
0₁(925)	→	926
0₁(746)	→	747
0₁(757)	→	758
0₁(382)	→	383
0₁(621)	→	622
0₁(855)	→	856
0₁(784)	→	785
0₁(1128)	→	1129
0₁(2417)	→	2418
0₁(1535)	→	1536
0₁(619)	→	620
0₁(706)	→	707
0₁(1032)	→	1033
0₁(1077)	→	1078
0₁(2003)	→	2004
0₁(1725)	→	1726
0₁(782)	→	783
0₁(2271)	→	2272
0₁(707)	→	708
0₁(1790)	→	1791
0₁(1788)	→	1789
0₁(641)	→	642
0₁(2409)	→	2410
0₁(973)	→	974
0₁(1301)	→	1302
0₁(956)	→	957
0₁(345)	→	346
0₁(1186)	→	1187
0₁(1549)	→	1550
0₁(237)	→	238
0₁(1514)	→	1515
0₁(1667)	→	1668
0₁(492)	→	493
3₂(1798)	→	1799
3₂(1806)	→	1807
3₂(1809)	→	1810
3₂(2389)	→	2390
3₂(992)	→	993
3₂(2204)	→	2205
3₂(2392)	→	2393
3₂(1805)	→	1806
3₂(2206)	→	2207
2₂(1894)	→	1895
2₂(2208)	→	2209
2₂(1899)	→	1900
2₂(1893)	→	1894
2₂(2386)	→	2387
2₂(994)	→	995
2₂(995)	→	996
2₂(1807)	→	1808
2₂(999)	→	1000
2₂(1804)	→	1805
2₂(2200)	→	2201
2₂(2393)	→	2394
2₂(998)	→	999
2₂(2203)	→	2204
2₂(1799)	→	1800
5₂(2201)	→	2202
5₂(2202)	→	2203
5₂(2278)	→	2279
5₂(1000)	→	1001
5₂(2280)	→	2281
5₂(1896)	→	1897
2₁(1151)	→	1152
2₁(1490)	→	1491
2₁(1368)	→	1369
2₁(463)	→	464
2₁(926)	→	927
2₁(1811)	→	1812
2₁(348)	→	349
2₁(913)	→	914
2₁(1198)	→	1199
2₁(303)	→	304
2₁(1126)	→	1127
2₁(163)	→	164
2₁(1861)	→	1862
2₁(438)	→	439
2₁(399)	→	400
2₁(1039)	→	1040
2₁(494)	→	495
2₁(663)	→	664
2₁(874)	→	875
2₁(102)	→	103
2₁(1114)	→	1115
2₁(2403)	→	2404
2₁(708)	→	709
2₁(662)	→	663
2₁(1817)	→	1818
2₁(1863)	→	1864
2₁(1330)	→	1331
2₁(2164)	→	2165
2₁(483)	→	484
2₁(1518)	→	1519
2₁(1718)	→	1719
2₁(1269)	→	1270
2₁(761)	→	762
2₁(11)	→	12
2₁(792)	→	793
2₁(853)	→	854
2₁(227)	→	228
2₁(613)	→	614
2₁(821)	→	822
2₁(1149)	→	1150
2₁(207)	→	208
2₁(1819)	→	1820
2₁(1871)	→	1872
2₁(1823)	→	1824
2₁(1112)	→	1113
2₁(854)	→	855
2₁(752)	→	753
2₁(826)	→	827
2₁(779)	→	780
2₁(951)	→	952
2₁(620)	→	621
2₁(191)	→	192
2₁(580)	→	581
2₁(1825)	→	1826
2₁(952)	→	953
2₁(687)	→	688
2₁(523)	→	524
2₁(1041)	→	1042
2₁(170)	→	171
2₁(484)	→	485
2₁(1033)	→	1034
2₁(1064)	→	1065
2₁(441)	→	442
2₁(94)	→	95
2₁(2382)	→	2383
2₁(800)	→	801
2₁(12)	→	13
2₁(755)	→	756
2₁(1013)	→	1014
2₁(1478)	→	1479
2₁(718)	→	719
2₁(400)	→	401
2₁(1034)	→	1035
2₁(488)	→	489
2₁(929)	→	930
2₁(2253)	→	2254
2₁(550)	→	551
2₁(1190)	→	1191
2₁(1100)	→	1101
2₁(972)	→	973
2₁(430)	→	431
2₁(1028)	→	1029
2₁(1357)	→	1358
2₁(1137)	→	1138
2₁(1974)	→	1975
2₁(788)	→	789
2₁(581)	→	582
2₁(668)	→	669
2₁(1008)	→	1009
2₁(543)	→	544
2₁(1278)	→	1279
2₁(432)	→	433
2₁(461)	→	462
2₁(577)	→	578
2₁(302)	→	303
2₁(764)	→	765
2₁(15)	→	16
2₁(1274)	→	1275
2₁(209)	→	210
2₁(786)	→	787
2₁(189)	→	190
2₁(1855)	→	1856
2₁(99)	→	100
2₁(1527)	→	1528
2₁(971)	→	972
2₁(1821)	→	1822
2₁(875)	→	876
2₁(2405)	→	2406
2₁(683)	→	684
2₁(579)	→	580
2₁(1541)	→	1542
2₁(815)	→	816
2₁(1472)	→	1473
2₁(493)	→	494
2₁(1098)	→	1099
2₁(522)	→	523
2₁(544)	→	545
2₁(830)	→	831
2₁(1063)	→	1064
2₁(1869)	→	1870
2₁(699)	→	700
2₁(16)	→	17
3₀(3)	→	5
3₀(6)	→	5
3₀(5)	→	5
3₀(4)	→	5
3₀(2)	→	5
3₀(1)	→	5
4₀(2)	→	6
4₀(6)	→	6
4₀(4)	→	6
4₀(1)	→	6
4₀(3)	→	6
4₀(5)	→	6
4₂(2394)	→	2395
4₂(2276)	→	2277
4₂(1906)	→	1907
4₂(2281)	→	2282
4₂(2279)	→	2280
4₂(1900)	→	1901
4₂(1802)	→	1803
4₂(2395)	→	2396
4₂(2390)	→	2391
4₂(1897)	→	1898
4₂(1891)	→	1892
4₂(2387)	→	2388
1₀(1)	→	4
1₀(6)	→	4
1₀(3)	→	4
1₀(5)	→	4
1₀(2)	→	4
1₀(4)	→	4
4₁(933)	→	934
4₁(2102)	→	2103
4₁(797)	→	798
4₁(690)	→	691
4₁(1261)	→	1262
4₁(892)	→	893
4₁(812)	→	813
4₁(876)	→	877
4₁(1233)	→	1234
4₁(1908)	→	1909
4₁(1721)	→	1722
4₁(666)	→	667
4₁(1513)	→	1514
4₁(1360)	→	1361
4₁(1482)	→	1483
4₁(856)	→	857
4₁(1201)	→	1202
4₁(524)	→	525
4₁(2104)	→	2105
4₁(695)	→	696
4₁(171)	→	172
4₁(406)	→	407
4₁(97)	→	98
4₁(1916)	→	1917
4₁(948)	→	949
4₁(553)	→	554
4₁(692)	→	693
4₁(740)	→	741
4₁(342)	→	343
4₁(164)	→	165
4₁(771)	→	772
4₁(1766)	→	1767
4₁(172)	→	173
4₁(1332)	→	1333
4₁(513)	→	514
4₁(1772)	→	1773
4₁(578)	→	579
4₁(744)	→	745
4₁(810)	→	811
4₁(1331)	→	1332
4₁(511)	→	512
4₁(1536)	→	1537
4₁(586)	→	587
4₁(1257)	→	1258
4₁(1255)	→	1256
4₁(1275)	→	1276
4₁(1259)	→	1260
4₁(411)	→	412
4₁(709)	→	710
4₁(2096)	→	2097
4₁(793)	→	794
4₁(583)	→	584
4₁(1265)	→	1266
4₁(1129)	→	1130
4₁(167)	→	168
4₁(660)	→	661
4₁(953)	→	954
4₁(516)	→	517
4₁(1770)	→	1771
4₁(235)	→	236
4₁(894)	→	895
4₁(2112)	→	2113
4₁(760)	→	761
4₁(721)	→	722
4₁(2110)	→	2111
4₁(1918)	→	1919
4₁(769)	→	770
4₁(1335)	→	1336
4₁(806)	→	807
4₁(1538)	→	1539
4₁(588)	→	589
4₁(1263)	→	1264
4₁(678)	→	679
4₁(808)	→	809
4₁(1517)	→	1518
4₁(672)	→	673
4₁(670)	→	671
4₁(916)	→	917
4₁(1134)	→	1135
4₁(927)	→	928
4₁(1456)	→	1457
4₁(610)	→	611
4₁(863)	→	864
4₁(713)	→	714
4₁(883)	→	884
4₁(778)	→	779
4₁(676)	→	677
4₁(725)	→	726
4₁(1484)	→	1485
4₁(409)	→	410
4₁(1302)	→	1303
4₁(1914)	→	1915
4₁(485)	→	486
4₁(684)	→	685
4₁(1421)	→	1422
4₁(674)	→	675
4₁(1131)	→	1132
4₁(1920)	→	1921
4₁(710)	→	711
4₁(1521)	→	1522
4₁(1011)	→	1012
4₁(1774)	→	1775
4₁(795)	→	796
4₁(2273)	→	2274
4₁(804)	→	805
4₁(1267)	→	1268
4₁(742)	→	743
5₁(1055)	→	1056
5₁(517)	→	518
5₁(1930)	→	1931
5₁(936)	→	937
5₁(1199)	→	1200
5₁(1972)	→	1973
5₁(1813)	→	1814
5₁(606)	→	607
5₁(1053)	→	1054
5₁(750)	→	751
5₁(1282)	→	1283
5₁(1483)	→	1484
5₁(1187)	→	1188
5₁(1519)	→	1520
5₁(1537)	→	1538
5₁(229)	→	230
5₁(748)	→	749
5₁(2251)	→	2252
5₁(1057)	→	1058
5₁(1362)	→	1363
5₁(1932)	→	1933
5₁(2357)	→	2358
5₁(780)	→	781
5₁(756)	→	757
5₁(278)	→	279
5₁(701)	→	702
5₁(1815)	→	1816
5₁(1333)	→	1334
5₁(862)	→	863
5₁(1476)	→	1477
5₁(796)	→	797
5₁(2056)	→	2057
5₁(1358)	→	1359
5₁(2237)	→	2238
5₁(341)	→	342
5₁(258)	→	259
5₁(691)	→	692
5₁(716)	→	717
5₁(1722)	→	1723
5₁(1663)	→	1664
5₁(896)	→	897
5₁(816)	→	817
5₁(2355)	→	2356
5₁(1135)	→	1136
5₁(1334)	→	1335
5₁(2243)	→	2244
5₁(2353)	→	2354
5₁(776)	→	777
5₁(964)	→	965
5₁(1284)	→	1285
5₁(1480)	→	1481
5₁(1651)	→	1652
5₁(915)	→	916
5₁(2245)	→	2246
5₁(2166)	→	2167
5₁(436)	→	437
5₁(1889)	→	1890
5₁(1720)	→	1721
5₁(1474)	→	1475
5₁(2235)	→	2236
5₁(719)	→	720
5₁(711)	→	712
5₁(256)	→	257
5₁(1938)	→	1939
5₁(2397)	→	2398
5₁(1249)	→	1250
5₁(1515)	→	1516
5₁(770)	→	771
5₁(861)	→	862
5₁(521)	→	522
5₁(723)	→	724
5₁(587)	→	588
5₁(1488)	→	1489
5₁(1355)	→	1356
5₁(623)	→	624
5₁(932)	→	933
5₁(700)	→	701
5₁(622)	→	623
5₁(739)	→	740
5₁(296)	→	297
5₁(1665)	→	1666
5₁(1290)	→	1291
5₁(343)	→	344
5₁(917)	→	918
5₁(276)	→	277
5₁(2267)	→	2268
5₁(1270)	→	1271
5₁(439)	→	440
5₁(1253)	→	1254
5₁(767)	→	768
5₁(1232)	→	1233
5₁(585)	→	586
5₁(17)	→	18
5₁(712)	→	713
5₁(665)	→	666
5₁(551)	→	552
5₁(1922)	→	1923
5₁(607)	→	608
5₁(440)	→	441
5₁(1924)	→	1925
5₁(408)	→	409
2₀(3)	→	2
2₀(5)	→	2
2₀(2)	→	2
2₀(4)	→	2
2₀(1)	→	2
2₀(6)	→	2
0₀(2)	→	3
0₀(4)	→	3
0₀(3)	→	3
0₀(6)	→	3
0₀(1)	→	3
0₀(5)	→	3
3₁(1705)	→	1706
3₁(101)	→	102
3₁(1015)	→	1016
3₁(2088)	→	2089
3₁(434)	→	435
3₁(2094)	→	2095
3₁(1682)	→	1683
3₁(745)	→	746
3₁(918)	→	919
3₁(758)	→	759
3₁(949)	→	950
3₁(166)	→	167
3₁(300)	→	301
3₁(1794)	→	1795
3₁(1030)	→	1031
3₁(885)	→	886
3₁(1958)	→	1959
3₁(442)	→	443
3₁(2160)	→	2161
3₁(823)	→	824
3₁(9)	→	10
3₁(232)	→	233
3₁(2072)	→	2073
3₁(696)	→	697
3₁(1454)	→	1455
3₁(1752)	→	1753
3₁(726)	→	727
3₁(2086)	→	2087
3₁(1200)	→	1201
3₁(161)	→	162
3₁(413)	→	414
3₁(902)	→	903
3₁(1277)	→	1278
3₁(969)	→	970
3₁(1443)	→	1444
3₁(1031)	→	1032
3₁(890)	→	891
3₁(100)	→	101
3₁(410)	→	411
3₁(169)	→	170
3₁(828)	→	829
3₁(491)	→	492
3₁(2078)	→	2079
3₁(880)	→	881
3₁(798)	→	799
3₁(1758)	→	1759
3₁(1680)	→	1681
3₁(433)	→	434
3₁(681)	→	682
3₁(1657)	→	1658
3₁(878)	→	879
3₁(680)	→	681
3₁(1026)	→	1027
3₁(935)	→	936
3₁(1760)	→	1761
3₁(2080)	→	2081
3₁(1659)	→	1660
3₁(1133)	→	1134
3₁(1516)	→	1517
3₁(2070)	→	2071
3₁(1065)	→	1066
3₁(1486)	→	1487
3₁(898)	→	899
3₁(1271)	→	1272
3₁(612)	→	613
3₁(403)	→	404
3₁(1952)	→	1953
3₁(922)	→	923
3₁(1185)	→	1186
3₁(514)	→	515
3₁(1272)	→	1273
3₁(1944)	→	1945
3₁(904)	→	905
3₁(611)	→	612
3₁(299)	→	300
3₁(1690)	→	1691
3₁(785)	→	786
3₁(686)	→	687
3₁(1966)	→	1967
3₁(763)	→	764
3₁(1017)	→	1018
3₁(1954)	→	1955
3₁(435)	→	436
3₁(1539)	→	1540
3₁(1132)	→	1133
3₁(401)	→	402
3₁(548)	→	549
3₁(2380)	→	2381
3₁(1723)	→	1724
3₁(1750)	→	1751
3₁(2320)	→	2321
3₁(962)	→	963
3₁(910)	→	911
3₁(93)	→	94
3₁(1964)	→	1965
3₁(519)	→	520
3₁(545)	→	546
3₁(556)	→	557
3₁(552)	→	553
3₁(702)	→	703
3₁(122)	→	123
3₁(143)	→	144
3₁(2162)	→	2163
3₁(1956)	→	1957
3₁(515)	→	516
3₁(802)	→	803
3₁(1356)	→	1357
3₁(1466)	→	1467
3₁(575)	→	576
3₁(754)	→	755
3₁(715)	→	716
3₁(1024)	→	1025
3₁(777)	→	778
3₁(233)	→	234
3₁(773)	→	774
3₁(2407)	→	2408
3₁(762)	→	763
3₁(1007)	→	1008
3₁(1067)	→	1068
3₁(1204)	→	1205
3₁(873)	→	874
3₁(931)	→	932
3₁(444)	→	445
3₁(2062)	→	2063
3₁(2064)	→	2065
3₁(141)	→	142
3₁(120)	→	121
3₁(872)	→	873
3₁(889)	→	890
3₁(1707)	→	1708
3₁(1946)	→	1947
3₁(1796)	→	1797
3₁(886)	→	887
3₁(486)	→	487
3₁(608)	→	609
3₁(546)	→	547
3₁(717)	→	718
3₁(1688)	→	1689
3₁(1354)	→	1355
1₁(1829)	→	1830
1₁(2183)	→	2184
1₁(974)	→	975
1₁(1614)	→	1615
1₁(685)	→	686
1₁(1837)	→	1838
1₁(165)	→	166
1₁(2421)	→	2422
1₁(818)	→	819
1₁(1877)	→	1878
1₁(667)	→	668
1₁(2330)	→	2331
1₁(305)	→	306
1₁(820)	→	821
1₁(819)	→	820
1₁(1116)	→	1117
1₁(766)	→	767
1₁(98)	→	99
1₁(1009)	→	1010
1₁(512)	→	513
1₁(1628)	→	1629
1₁(1276)	→	1277
1₁(1361)	→	1362
1₁(326)	→	327
1₁(404)	→	405
1₁(41)	→	42
1₁(1300)	→	1301
1₁(1035)	→	1036
1₁(324)	→	325
1₁(1202)	→	1203
1₁(955)	→	956
1₁(2126)	→	2127
1₁(1479)	→	1480
1₁(1831)	→	1832
1₁(344)	→	345
1₁(2399)	→	2400
1₁(813)	→	814
1₁(822)	→	823
1₁(2401)	→	2402
1₁(1776)	→	1777
1₁(1130)	→	1131
1₁(703)	→	704
1₁(954)	→	955
1₁(1626)	→	1627
1₁(1118)	→	1119
1₁(2043)	→	2044
1₁(966)	→	967
1₁(937)	→	938
1₁(1325)	→	1326
1₁(868)	→	869
1₁(772)	→	773
1₁(236)	→	237
1₁(1189)	→	1190
1₁(306)	→	307
1₁(1127)	→	1128
1₁(783)	→	784
1₁(1029)	→	1030
1₁(1327)	→	1328
1₁(1780)	→	1781
1₁(914)	→	915
1₁(845)	→	846
1₁(664)	→	665
1₁(2191)	→	2192
1₁(2351)	→	2352
1₁(1037)	→	1038
1₁(1839)	→	1840
1₁(69)	→	70
1₁(722)	→	723
1₁(945)	→	946
1₁(1782)	→	1783
1₁(1792)	→	1793
1₁(877)	→	878
1₁(1584)	→	1585
1₁(858)	→	859
1₁(1122)	→	1123
1₁(2132)	→	2133
1₁(542)	→	543
1₁(1616)	→	1617
1₁(525)	→	526
1₁(2326)	→	2327
1₁(1727)	→	1728
1₁(829)	→	830
1₁(1719)	→	1720
1₁(1620)	→	1621
1₁(847)	→	848
1₁(67)	→	68
1₁(968)	→	969
1₁(801)	→	802
1₁(924)	→	925
1₁(2423)	→	2424
1₁(705)	→	706
1₁(887)	→	888
1₁(443)	→	444
1₁(799)	→	800
1₁(2185)	→	2186
1₁(618)	→	619
1₁(14)	→	15
1₁(431)	→	432
1₁(944)	→	945
1₁(480)	→	481
1₁(870)	→	871
1₁(1742)	→	1743
1₁(851)	→	852
1₁(489)	→	490
1₁(1061)	→	1062
1₁(576)	→	577
1₁(987)	→	988
1₁(866)	→	867
1₁(1641)	→	1642
1₁(1120)	→	1121
1₁(1529)	→	1530
1₁(91)	→	92
1₁(661)	→	662
1₁(168)	→	169
1₁(1643)	→	1644
1₁(934)	→	935
1₁(2025)	→	2026
1₁(1778)	→	1779
1₁(412)	→	413
1₁(893)	→	894
1₁(304)	→	305
1₁(2193)	→	2194
1₁(864)	→	865
1₁(1618)	→	1619
1₁(1853)	→	1854
1₁(2124)	→	2125
1₁(923)	→	924
1₁(1622)	→	1623
1₁(741)	→	742
1₁(2120)	→	2121
1₁(1533)	→	1534
1₁(928)	→	929
1₁(2039)	→	2040
1₁(2332)	→	2333
1₁(789)	→	790
1₁(1716)	→	1717
1₁(346)	→	347
1₁(2021)	→	2022
1₁(1069)	→	1070
1₁(554)	→	555
1₁(832)	→	833
1₁(1012)	→	1013
1₁(2041)	→	2042
1₁(2037)	→	2038
1₁(1036)	→	1037
1₁(2328)	→	2329
1₁(298)	→	299
1₁(1485)	→	1486
1₁(989)	→	990
1₁(2029)	→	2030
1₁(2118)	→	2119
1₁(1995)	→	1996
1₁(230)	→	231
1₁(698)	→	699
1₁(1590)	→	1591
1₁(43)	→	44
1₁(617)	→	618
1₁(1540)	→	1541
1₁(1993)	→	1994
1₁(787)	→	788
1₁(2411)	→	2412
1₁(95)	→	96
1₁(825)	→	826
1₁(584)	→	585
1₁(2023)	→	2024
1₁(693)	→	694
1₁(884)	→	885
1₁(481)	→	482
1₁(231)	→	232
1₁(8)	→	9
1₁(1531)	→	1532
0₂(2275)	→	2276
0₂(993)	→	994
0₂(1801)	→	1802
0₂(996)	→	997
0₂(2282)	→	2283
0₂(2207)	→	2208
5₀(1)	→	1
5₀(6)	→	1
5₀(5)	→	1
5₀(2)	→	1
5₀(3)	→	1
5₀(4)	→	1
1₂(2214)	→	2215
1₂(1898)	→	1899
1₂(2158)	→	2159
1₂(2199)	→	2200
1₂(2277)	→	2278
1₂(997)	→	998
1₂(1803)	→	1804
1₂(991)	→	992
1₂(2229)	→	2230
1₂(2388)	→	2389
1₂(2205)	→	2206
1₂(2154)	→	2155
1₂(1892)	→	1893
1₂(1800)	→	1801
1₂(2227)	→	2228
1₂(2212)	→	2213
1₂(2283)	→	2284
1₂(2391)	→	2392
1₂(2210)	→	2211
1₂(2152)	→	2153
1₂(1895)	→	1896

The automaton is closed under rewriting as it is compatible.