Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/88156)

The rewrite relation of the following TRS is considered.

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

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

1(1(0(2(1(0(3(0(2(1(1(0(0(x1)))))))))))))	→	0(1(0(0(0(1(0(0(2(2(0(2(0(0(3(0(0(x1)))))))))))))))))	(31)
1(2(0(1(1(2(2(0(1(3(0(1(0(x1)))))))))))))	→	2(1(0(3(0(1(0(1(0(0(0(0(3(2(2(0(0(x1)))))))))))))))))	(32)
2(1(3(0(2(1(3(1(0(0(1(1(0(x1)))))))))))))	→	0(2(2(1(0(0(0(0(2(0(3(1(0(2(0(2(0(x1)))))))))))))))))	(33)
1(1(1(1(0(0(3(0(1(2(3(1(0(x1)))))))))))))	→	0(1(0(0(3(0(3(0(2(3(0(0(1(3(1(3(0(x1)))))))))))))))))	(34)
1(3(1(1(3(2(3(2(0(2(0(2(0(x1)))))))))))))	→	0(1(2(2(0(0(3(2(3(0(3(0(0(3(1(0(0(x1)))))))))))))))))	(35)
3(0(2(3(0(2(1(2(2(3(2(2(0(x1)))))))))))))	→	0(3(0(0(1(2(0(1(0(0(3(2(0(1(2(3(0(x1)))))))))))))))))	(36)
3(2(1(1(2(2(3(2(2(0(3(2(0(x1)))))))))))))	→	2(1(1(0(2(0(3(1(0(2(0(2(3(2(0(0(1(x1)))))))))))))))))	(37)
2(3(1(2(0(0(2(0(1(1(3(2(0(x1)))))))))))))	→	0(2(2(0(0(2(2(1(0(2(2(3(0(0(2(2(0(x1)))))))))))))))))	(38)
3(1(3(0(2(0(1(3(2(2(3(2(0(x1)))))))))))))	→	3(2(2(0(2(0(2(2(0(0(1(1(2(0(3(0(0(x1)))))))))))))))))	(39)
1(1(2(2(1(0(1(0(2(3(0(0(1(x1)))))))))))))	→	2(1(0(0(1(0(2(0(2(0(0(0(1(3(3(0(0(x1)))))))))))))))))	(40)
2(2(1(1(1(0(1(1(2(0(3(0(1(x1)))))))))))))	→	3(3(3(3(3(0(0(0(3(0(0(2(0(0(2(3(0(x1)))))))))))))))))	(41)
2(3(2(3(1(0(0(2(2(0(2(1(1(x1)))))))))))))	→	1(0(0(2(3(0(0(1(0(3(2(1(0(0(0(0(2(x1)))))))))))))))))	(42)
1(0(2(2(1(0(0(2(2(1(2(2(1(x1)))))))))))))	→	3(0(1(0(2(0(2(3(0(2(2(1(0(0(3(0(0(x1)))))))))))))))))	(43)
0(1(1(1(0(0(1(2(0(1(3(2(1(x1)))))))))))))	→	0(3(1(0(1(0(0(0(3(0(2(1(0(1(0(3(0(x1)))))))))))))))))	(44)
3(2(0(1(2(2(2(2(3(0(0(3(1(x1)))))))))))))	→	0(0(2(1(3(2(0(3(0(2(3(0(2(2(0(0(3(x1)))))))))))))))))	(45)
0(1(3(1(0(2(1(3(1(0(1(3(1(x1)))))))))))))	→	0(0(0(0(3(0(1(3(3(0(0(3(1(3(0(2(1(x1)))))))))))))))))	(46)
0(3(2(0(0(1(0(0(3(1(1(3(1(x1)))))))))))))	→	0(3(1(1(0(2(0(0(0(0(2(3(0(2(0(1(2(x1)))))))))))))))))	(47)
1(0(0(3(1(0(2(0(1(3(1(3(1(x1)))))))))))))	→	1(0(3(3(3(1(0(0(2(0(0(1(0(0(0(2(2(x1)))))))))))))))))	(48)
0(0(3(1(0(3(0(1(0(1(2(3(1(x1)))))))))))))	→	0(0(1(0(1(2(3(2(0(0(3(0(0(0(1(3(0(x1)))))))))))))))))	(49)
1(1(0(0(2(3(0(3(2(0(3(3(1(x1)))))))))))))	→	1(3(2(0(1(0(0(0(2(0(0(3(0(3(0(2(3(x1)))))))))))))))))	(50)
0(3(2(0(2(2(3(2(2(2(3(3(1(x1)))))))))))))	→	0(0(2(1(3(2(2(0(1(2(2(0(2(2(3(0(3(x1)))))))))))))))))	(51)
0(1(2(2(2(2(3(2(2(1(2(0(2(x1)))))))))))))	→	0(3(2(0(0(1(3(0(2(0(0(1(0(0(0(0(1(x1)))))))))))))))))	(52)
2(1(1(0(2(3(2(2(1(2(2(0(2(x1)))))))))))))	→	0(1(2(2(1(0(0(0(0(0(0(1(3(1(3(2(0(x1)))))))))))))))))	(53)
1(0(1(2(0(0(2(2(1(3(3(0(2(x1)))))))))))))	→	2(0(1(2(0(0(0(1(3(0(2(0(0(1(0(2(3(x1)))))))))))))))))	(54)
3(1(3(0(0(2(1(2(3(0(1(1(2(x1)))))))))))))	→	3(3(1(2(2(0(0(2(2(0(0(0(0(1(0(2(2(x1)))))))))))))))))	(55)
3(2(1(2(3(3(0(1(0(1(0(2(2(x1)))))))))))))	→	0(0(0(1(2(1(2(2(0(2(1(0(2(1(0(3(0(x1)))))))))))))))))	(56)
3(0(3(0(2(3(3(2(0(0(0(3(2(x1)))))))))))))	→	0(2(3(0(2(0(3(0(0(0(2(1(0(0(0(2(2(x1)))))))))))))))))	(57)
3(2(3(2(3(0(2(0(2(2(0(3(2(x1)))))))))))))	→	2(0(0(2(0(0(3(0(0(3(3(0(2(3(0(0(1(x1)))))))))))))))))	(58)
3(3(3(0(2(0(2(1(3(1(0(0(3(x1)))))))))))))	→	3(1(0(0(2(2(2(0(3(0(0(2(1(0(1(0(0(x1)))))))))))))))))	(59)
0(3(3(2(2(0(3(1(0(2(2(2(3(x1)))))))))))))	→	0(0(1(0(0(1(1(2(1(0(3(0(0(1(0(1(1(x1)))))))))))))))))	(60)

1.1 Bounds

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

final states:

{4, 3, 2, 1}

transitions:

272	→	254
1182	→	1156
1906	→	553
1659	→	1783
1659	→	1827
1206	→	336
157	→	745
23	→	1
23	→	914
23	→	915
23	→	667
23	→	254
23	→	306
23	→	745
23	→	159
23	→	157
23	→	1068
23	→	1065
23	→	987
23	→	726
23	→	725
23	→	2032
23	→	1718
1268	→	7
1602	→	833
1868	→	900
1868	→	1602
1868	→	198
1868	→	1080
1868	→	1772
867	→	1553
867	→	1567
867	→	1581
2124	→	7
1652	→	7
1287	→	2278
61	→	7
61	→	1077
1940	→	138
1940	→	1973
2253	→	7
917	→	1083
1674	→	6
1674	→	1725
1674	→	1915
454	→	1623
2046	→	93
2046	→	2147
830	→	1173
789	→	665
1905	→	2117
1492	→	1801
338	→	1475
1762	→	254
967	→	1275
2205	→	6
2110	→	7
715	→	858
2246	→	2250
2246	→	2256
152	→	1559
152	→	1569
152	→	1591
1624	→	858
1630	→	254
1288	→	2264
10	→	348
2277	→	7
1169	→	1845
2100	→	254
2247	→	725
1998	→	155
1638	→	7
537	→	1645
537	→	1667
537	→	1705
1966	→	758
2142	→	7
2116	→	7
1248	→	7
1546	→	776
1546	→	1889
1560	→	254
1794	→	7
1431	→	654
1046	→	156
1867	→	2236
1867	→	2246
1867	→	2248
1409	→	539
2204	→	2266
2239	→	7
1784	→	7
882	→	269
882	→	1085
882	→	1104
1972	→	833
167	→	19
1740	→	758
1008	→	2003
2040	→	725
1909	→	2123
1273	→	1763
502	→	451
2126	→	7
2132	→	7
1792	→	7
1916	→	406
668	→	652
466	→	947
466	→	991
466	→	1018
1584	→	758
1887	→	2242
1172	→	758
1172	→	4
1172	→	582
1172	→	627
1172	→	804
1532	→	758
1532	→	1545
585	→	931
625	→	582
2054	→	141
2235	→	7
1103	→	582
1103	→	156
1103	→	624
1103	→	305
1103	→	60
1103	→	499
1103	→	4
1103	→	761
1103	→	654
1103	→	1538
1103	→	1431
1103	→	1911
1103	→	6
1103	→	1884
1964	→	758
469	→	451
226	→	4
226	→	582
226	→	156
226	→	761
226	→	804
226	→	627
226	→	763
226	→	777
226	→	654
226	→	1538
226	→	1431
226	→	1552
226	→	1911
226	→	6
226	→	1884
2249	→	139
3	→	58
3	→	271
3	→	501
3	→	626
583	→	776
1411	→	540
499	→	1981
2203	→	6
2203	→	2230
988	→	967
988	→	1271
772	→	1205
772	→	2009
2271	→	725
553	→	1181
1574	→	138
1574	→	1609
1888	→	6
1888	→	1913
1289	→	2234
1102	→	1753
817	→	153
1011	→	652
1011	→	710
1011	→	451
1011	→	626
1011	→	271
1011	→	58
1011	→	501
1011	→	3
1011	→	469
1011	→	668
1011	→	803
1011	→	139
1011	→	2189
500	→	451
225	→	1177
980	→	1873
405	→	105
1812	→	8
1226	→	1212
1074	→	157
2012	→	7
347	→	151
108	→	1
108	→	914
108	→	254
108	→	697
108	→	272
108	→	915
108	→	651
108	→	308
108	→	2032
108	→	1772
1359	→	2021
1359	→	2039
1359	→	2059
1340	→	139
2140	→	7
9	→	394
1706	→	139
1714	→	139
1714	→	1907
2030	→	7
2275	→	139
59	→	7
59	→	1079
1778	→	254
1276	→	1412
1276	→	1509
1932	→	138
1076	→	197
1076	→	1211
2281	→	7
598	→	2015
598	→	2031
1918	→	779
1454	→	697
2289	→	7
1764	→	254
997	→	1306
361	→	4
361	→	758
361	→	158
361	→	582
361	→	599
361	→	625
1618	→	336
1646	→	7
756	→	1247
1636	→	254
1082	→	198
1344	→	1408
1900	→	553
1770	→	254
467	→	3
467	→	710
467	→	451
467	→	759
467	→	500
1890	→	584
1068	→	157
2018	→	7
107	→	1561
107	→	1573
107	→	1583
224	→	1637
713	→	1209
713	→	1689
942	→	914
942	→	915
942	→	598
942	→	253
942	→	6
942	→	468
942	→	1
942	→	667
942	→	254
942	→	2032
1800	→	8
1668	→	725
1601	→	1807
1601	→	1837
1601	→	1883
1898	→	696
2118	→	7
1	→	6
1	→	253
1	→	468
1	→	598
1105	→	1088
1471	→	2204
1471	→	2254
1726	→	157
1907	→	2125
1010	→	1755
1078	→	198
8	→	93
8	→	197
8	→	155
8	→	7
8	→	581
8	→	307
8	→	91
8	→	450
8	→	2
8	→	92
8	→	584
8	→	201
8	→	1988
8	→	658
1019	→	139
1019	→	1455
1009	→	1919
1009	→	1931
1009	→	1965
1884	→	6
1884	→	1911
1570	→	138
833	→	914
833	→	651
833	→	1
833	→	254
833	→	308
833	→	1082
1066	→	156
940	→	1681
1838	→	139
1838	→	1899
1223	→	1739
1223	→	1997
1338	→	1307
1338	→	2051
1228	→	1214
1111	→	1090
2052	→	94
2245	→	7
1922	→	254
2037	→	2107
2037	→	2186
416	→	2260
2024	→	7
139	→	335
139	→	803
1934	→	138
1934	→	1979
1376	→	7
1996	→	155
1208	→	339
1616	→	336
1801	→	2101
1700	→	139
1676	→	93
1676	→	1813
1988	→	155
2039	→	2115
2039	→	2192
1772	→	254
881	→	1175
1554	→	254
1592	→	758
816	→	1267
269	→	1563
269	→	1575
269	→	1589
1413	→	540
2243	→	7
1654	→	7
1982	→	155
1971	→	2133
1971	→	2194
1971	→	2202
868	→	225
2283	→	7
760	→	818
268	→	1343
1799	→	2099
21	→	985
1883	→	2240
1170	→	1851
912	→	1045
912	→	1432
912	→	1491
1564	→	254
552	→	1643
540	→	943
540	→	1227
540	→	1551
1176	→	1156
407	→	1537
1926	→	138
844	→	2017
1830	→	139
1084	→	199
597	→	225
1610	→	539
2193	→	139
554	→	2
554	→	155
554	→	255
554	→	916
554	→	138
554	→	7
554	→	776
554	→	583
554	→	61
554	→	8
554	→	698
554	→	746
554	→	160
554	→	1275
554	→	1271
554	→	901
554	→	1996
554	→	2016
554	→	967
554	→	988
554	→	1982
554	→	2110
726	→	1
726	→	900
726	→	914
726	→	651
726	→	254
726	→	308
726	→	198
726	→	915
726	→	1082
726	→	1772
726	→	2032
2285	→	7
1865	→	2045
773	→	725
627	→	582
1667	→	1791
1667	→	1835
1882	→	540
468	→	1995
153	→	1179
1456	→	697
986	→	967
986	→	1265
982	→	914
982	→	254
982	→	1
982	→	697
982	→	272
308	→	254
308	→	651
2031	→	2109
2031	→	2188
22	→	1183
1811	→	2093
2189	→	139
1293	→	1276
1293	→	1410
2158	→	2288
336	→	989
2134	→	7
270	→	4
270	→	758
270	→	582
270	→	627
270	→	804
1101	→	2029
2010	→	7
538	→	1
538	→	914
538	→	651
538	→	833
538	→	254
538	→	308
538	→	900
538	→	1602
538	→	198
538	→	1080
538	→	1772
2287	→	7
831	→	107
831	→	1075
831	→	1112
2022	→	7
1180	→	1156
2263	→	7
1684	→	94
1899	→	2131
999	→	1707
2	→	91
2	→	307
2	→	450
2	→	581
2161	→	2280
2195	→	139
2195	→	2226
1540	→	406
11	→	526
2267	→	7
4	→	60
4	→	305
4	→	499
4	→	624
941	→	1777
1291	→	710
1291	→	451
1291	→	3
1291	→	711
1291	→	502
1291	→	1462
1291	→	1474
1291	→	989
1291	→	336
1178	→	1156
1504	→	465
1174	→	1156
582	→	758
582	→	1067
212	→	406
212	→	1917
1786	→	7
1425	→	652
843	→	1531
843	→	1897
843	→	2139
501	→	1989
419	→	1651
419	→	1665
1821	→	2262
1538	→	761
801	→	1629
1666	→	725
1814	→	211
802	→	552
802	→	1615
359	→	1635
359	→	2232
106	→	1375
1836	→	139
913	→	360
913	→	1424
1224	→	107
535	→	966
2265	→	7
1692	→	93
1692	→	1799
1692	→	1821
981	→	1921
981	→	1933
981	→	1941
306	→	254
800	→	1155
2255	→	7
1698	→	140
1698	→	2065
1221	→	1925
759	→	1110
708	→	1699
708	→	2141
450	→	1987
1604	→	539
2038	→	725
140	→	1337
140	→	1971
140	→	2067
2004	→	155
2241	→	7
944	→	584
1013	→	998
7	→	138
7	→	155
7	→	1771
1712	→	139
2162	→	2258
2162	→	2270
757	→	665
2094	→	254
2233	→	155
1184	→	1156
1980	→	539
2237	→	7
1080	→	198
2202	→	2268
2187	→	139
1846	→	139
417	→	2244
2163	→	1462
2163	→	710
2163	→	451
2163	→	3
2163	→	711
2163	→	502
2163	→	1474
2163	→	989
2163	→	336
2257	→	139
1321	→	710
1321	→	451
1321	→	3
1321	→	759
1321	→	500
453	→	1207
453	→	1683
2251	→	7
1756	→	254
1510	→	1494
1357	→	1675
709	→	551
1910	→	553
2269	→	7
948	→	539
948	→	1073
948	→	1539
1718	→	159
990	→	970
2270	→	2272
2270	→	2274
256	→	790
256	→	869
198	→	900
1720	→	156
1644	→	7
2231	→	406
1272	→	8
1822	→	211
1822	→	1881
1822	→	1909
2160	→	2284
1286	→	2282
360	→	1617
360	→	1653
360	→	1659
712	→	832
712	→	1711
712	→	1719
926	→	755
1433	→	696
1433	→	1461
1433	→	1697
2068	→	156
154	→	3
154	→	652
154	→	710
154	→	451
154	→	469
154	→	668
154	→	759
154	→	500
154	→	1473
154	→	1453
154	→	996
154	→	803
154	→	139
154	→	2189
1874	→	7
666	→	553
1476	→	714
1576	→	138
1576	→	1603
254	→	667
254	→	914
2279	→	7
267	→	1339
2032	→	725
832	→	1809
832	→	1843
832	→	1887
1990	→	155
1474	→	1462
1665	→	1785
1665	→	1829
1419	→	539
1266	→	8
1828	→	139
1682	→	93
1682	→	1811
1682	→	1819
2226	→	2252
1360	→	914
1360	→	651
1360	→	833
1360	→	598
1360	→	253
1360	→	6
1360	→	468
1360	→	1
1360	→	254
1360	→	308
1360	→	900
1360	→	1602
1360	→	198
1360	→	1080
1360	→	1772
142	→	2053
1708	→	141
1271	→	1769
1290	→	2011
1290	→	2037
1472	→	417
1660	→	725
92	→	7
92	→	1081
358	→	1087
451	→	696
451	→	710
2108	→	7
452	→	1012
452	→	1430
452	→	1601
541	→	846
1210	→	339
2102	→	254
1171	→	1923
1171	→	1939
1171	→	1963
1113	→	758
1320	→	1673
1320	→	1691
1320	→	1713
1942	→	758
1908	→	553
2261	→	7
2159	→	2286
418	→	2023
1568	→	138
210	→	21
1552	→	777
1562	→	254
1912	→	406
1265	→	1761
551	→	1418
551	→	1793
2066	→	156
1844	→	139
1844	→	1905
1924	→	254
725	→	987
725	→	995
725	→	1065
1612	→	155
1920	→	254
845	→	360
992	→	138
992	→	1273
992	→	1292
1274	→	8
151	→	1611
2016	→	7
1590	→	758
1810	→	7
1852	→	1879
2060	→	139
599	→	582
599	→	158
599	→	624
599	→	305
599	→	60
599	→	499
599	→	4
599	→	656
996	→	1453
996	→	1473
2273	→	7
1802	→	8
1880	→	539
2259	→	7
1754	→	254
656	→	1717
415	→	2276
156	→	211
156	→	539
1914	→	406
1820	→	211
1086	→	197
1086	→	1225
1673	→	2238
1690	→	94
2227	→	553
857	→	596
1808	→	7
420	→	3
420	→	710
420	→	451
420	→	711
420	→	502
420	→	1462
420	→	1474
420	→	989
420	→	336
1582	→	758
1974	→	539
2₁(851)	→	852
2₁(1205)	→	1206
2₁(211)	→	212
2₁(1350)	→	1351
2₁(785)	→	786
2₁(260)	→	261
2₁(788)	→	789
2₁(2059)	→	2060
2₁(456)	→	457
2₁(1221)	→	1222
2₁(2151)	→	2152
2₁(1349)	→	1350
2₁(1091)	→	1092
2₁(784)	→	785
2₁(11)	→	12
2₁(751)	→	752
2₁(710)	→	711
2₁(1009)	→	1010
2₁(1837)	→	1838
2₁(858)	→	859
2₁(1913)	→	1914
2₁(1310)	→	1311
2₁(209)	→	210
2₁(468)	→	469
2₁(162)	→	163
2₁(867)	→	868
2₁(838)	→	839
2₁(1167)	→	1168
2₁(933)	→	934
2₁(981)	→	982
2₁(870)	→	871
2₁(353)	→	354
2₁(2148)	→	2149
2₁(771)	→	772
2₁(1012)	→	1013
2₁(501)	→	502
2₁(667)	→	668
2₁(828)	→	829
2₁(528)	→	529
2₁(967)	→	968
2₁(359)	→	360
2₁(1008)	→	1009
2₁(1683)	→	1684
2₁(1500)	→	1501
2₁(1707)	→	1708
2₁(335)	→	336
2₁(908)	→	909
2₁(795)	→	796
2₁(354)	→	355
2₁(995)	→	996
2₁(1160)	→	1161
2₁(543)	→	544
2₁(1468)	→	1469
2₁(778)	→	779
2₁(879)	→	880
2₁(1835)	→	1836
2₁(527)	→	528
2₁(592)	→	593
2₁(1002)	→	1003
2₁(93)	→	94
2₁(1223)	→	1224
2₁(1088)	→	1089
2₁(256)	→	257
2₁(1018)	→	1019
2₁(1689)	→	1690
2₁(968)	→	969
2₁(1279)	→	1280
2₁(758)	→	759
2₁(2256)	→	2257
2₁(846)	→	847
2₁(140)	→	141
2₁(2186)	→	2187
2₁(902)	→	903
2₁(356)	→	357
2₁(339)	→	340
2₁(408)	→	409
2₁(821)	→	822
2₁(138)	→	139
2₁(1539)	→	1540
2₁(463)	→	464
2₁(1317)	→	1318
2₁(585)	→	586
2₁(997)	→	998
2₁(842)	→	843
2₁(208)	→	209
2₁(584)	→	585
2₁(1861)	→	1862
2₁(151)	→	152
2₁(2053)	→	2054
2₁(1158)	→	1159
2₁(698)	→	699
2₁(814)	→	815
2₁(1705)	→	1706
2₁(815)	→	816
2₁(399)	→	400
2₁(94)	→	95
2₁(145)	→	146
2₁(1213)	→	1214
2₁(2248)	→	2249
2₁(204)	→	205
2₁(1915)	→	1916
2₁(706)	→	707
2₁(401)	→	402
2₁(588)	→	589
2₁(1219)	→	1220
2₁(1711)	→	1712
2₁(531)	→	532
2₁(344)	→	345
2₁(1424)	→	1425
2₁(1461)	→	1462
2₁(1858)	→	1859
2₁(450)	→	451
2₁(1162)	→	1163
2₁(258)	→	259
2₁(1897)	→	1898
2₁(269)	→	270
2₁(1218)	→	1219
2₁(214)	→	215
2₁(2230)	→	2231
2₁(1843)	→	1844
2₁(13)	→	14
2₁(107)	→	108
2₁(1863)	→	1864
2₁(220)	→	221
2₁(765)	→	766
2₁(1339)	→	1340
2₁(1432)	→	1433
2₁(864)	→	865
2₁(1617)	→	1618
2₁(343)	→	344
2₁(651)	→	652
2₁(14)	→	15
2₁(1827)	→	1828
2₁(922)	→	923
2₁(265)	→	266
2₁(854)	→	855
2₁(777)	→	778
2₁(2194)	→	2195
2₁(717)	→	718
2₁(841)	→	842
2₁(2188)	→	2189
2₁(1276)	→	1277
2₁(753)	→	754
2₁(1355)	→	1356
2₁(340)	→	341
2₁(849)	→	850
2₁(499)	→	500
2₁(358)	→	359
2₁(1615)	→	1616
2₁(348)	→	349
2₁(1845)	→	1846
2₁(932)	→	933
2₁(701)	→	702
2₁(2274)	→	2275
2₁(1171)	→	1172
2₁(1713)	→	1714
2₁(909)	→	910
2₁(2051)	→	2052
2₁(780)	→	781
2₁(781)	→	782
2₁(1917)	→	1918
2₁(1502)	→	1503
2₁(1699)	→	1700
2₁(152)	→	153
2₁(852)	→	853
2₁(907)	→	908
2₁(1911)	→	1912
2₁(837)	→	838
2₁(1473)	→	1474
2₁(1829)	→	1830
2₁(801)	→	802
2₁(1857)	→	1858
2₁(1227)	→	1228
2₁(595)	→	596
2₁(2192)	→	2193
2₁(1353)	→	1354
2₁(1097)	→	1098
2₁(533)	→	534
3₁(1311)	→	1312
3₁(1819)	→	1820
3₁(872)	→	873
3₁(803)	→	804
3₁(1821)	→	1822
3₁(1813)	→	1814
3₁(417)	→	418
3₁(1979)	→	1980
3₁(1282)	→	1283
3₁(1408)	→	1409
3₁(338)	→	339
3₁(95)	→	96
3₁(155)	→	156
3₁(2161)	→	2162
3₁(161)	→	162
3₁(1288)	→	1289
3₁(1207)	→	1208
3₁(1492)	→	1493
3₁(205)	→	206
3₁(462)	→	463
3₁(201)	→	202
3₁(157)	→	158
3₁(1963)	→	1964
3₁(1583)	→	1584
3₁(762)	→	763
3₁(2147)	→	2148
3₁(1887)	→	1888
3₁(2154)	→	2155
3₁(862)	→	863
3₁(552)	→	553
3₁(587)	→	588
3₁(1286)	→	1287
3₁(1879)	→	1880
3₁(1065)	→	1066
3₁(772)	→	773
3₁(1591)	→	1592
3₁(2202)	→	2203
3₁(1165)	→	1166
3₁(776)	→	777
3₁(263)	→	264
3₁(1104)	→	1105
3₁(869)	→	870
3₁(224)	→	225
3₁(905)	→	906
3₁(581)	→	582
3₁(873)	→	874
3₁(598)	→	599
3₁(805)	→	806
3₁(723)	→	724
3₁(1112)	→	1113
3₁(164)	→	165
3₁(1739)	→	1740
3₁(360)	→	361
3₁(198)	→	199
3₁(8)	→	9
3₁(1101)	→	1102
3₁(2065)	→	2066
3₁(659)	→	660
3₁(1289)	→	1290
3₁(1211)	→	1212
3₁(203)	→	204
3₁(1159)	→	1160
3₁(1719)	→	1720
3₁(1883)	→	1884
3₁(797)	→	798
3₁(1965)	→	1966
3₁(457)	→	458
3₁(1209)	→	1210
3₁(1537)	→	1538
3₁(748)	→	749
3₁(416)	→	417
3₁(823)	→	824
3₁(394)	→	395
3₁(876)	→	877
3₁(969)	→	970
3₁(545)	→	546
3₁(1853)	→	1854
3₁(1087)	→	1088
3₁(1589)	→	1590
3₁(1609)	→	1610
3₁(978)	→	979
3₁(722)	→	723
3₁(143)	→	144
3₁(2162)	→	2163
3₁(1418)	→	1419
3₁(1501)	→	1502
3₁(537)	→	538
3₁(1000)	→	1001
3₁(1941)	→	1942
3₁(919)	→	920
3₁(1973)	→	1974
3₁(1603)	→	1604
3₁(760)	→	761
3₁(1275)	→	1276
3₁(1045)	→	1046
3₁(411)	→	412
3₁(590)	→	591
3₁(624)	→	625
3₁(257)	→	258
3₁(721)	→	722
3₁(1292)	→	1293
3₁(658)	→	659
3₁(1430)	→	1431
3₁(418)	→	419
3₁(1225)	→	1226
3₁(1551)	→	1552
3₁(1083)	→	1084
3₁(752)	→	753
3₁(2159)	→	2160
3₁(530)	→	531
3₁(2204)	→	2205
3₁(593)	→	594
3₁(653)	→	654
3₁(1359)	→	1360
3₁(2160)	→	2161
3₁(1316)	→	1317
3₁(786)	→	787
3₁(1497)	→	1498
3₁(1673)	→	1674
3₁(2067)	→	2068
3₁(1867)	→	1868
3₁(989)	→	990
3₁(1345)	→	1346
3₁(1290)	→	1291
3₁(1531)	→	1532
3₁(1860)	→	1861
3₁(166)	→	167
3₁(1352)	→	1353
3₁(655)	→	656
3₁(662)	→	663
3₁(626)	→	627
3₁(866)	→	867
3₁(104)	→	105
3₁(1092)	→	1093
3₁(1287)	→	1288
3₁(415)	→	416
3₁(419)	→	420
3₁(2158)	→	2159
3₁(947)	→	948
3₁(215)	→	216
3₁(700)	→	701
3₁(844)	→	845
3₁(1581)	→	1582
1₁(924)	→	925
1₁(1179)	→	1180
1₁(1471)	→	1472
1₁(106)	→	107
1₁(921)	→	922
1₁(1155)	→	1156
1₁(2039)	→	2040
1₁(1503)	→	1504
1₁(1753)	→	1754
1₁(1089)	→	1090
1₁(100)	→	101
1₁(150)	→	151
1₁(2226)	→	2227
1₁(848)	→	849
1₁(1553)	→	1554
1₁(459)	→	460
1₁(218)	→	219
1₁(540)	→	541
1₁(696)	→	697
1₁(824)	→	825
1₁(1348)	→	1349
1₁(832)	→	833
1₁(843)	→	844
1₁(2093)	→	2094
1₁(2246)	→	2247
1₁(798)	→	799
1₁(1081)	→	1082
1₁(1601)	→	1602
1₁(976)	→	977
1₁(923)	→	924
1₁(1214)	→	1215
1₁(1215)	→	1216
1₁(212)	→	213
1₁(142)	→	143
1₁(156)	→	157
1₁(1771)	→	1772
1₁(901)	→	902
1₁(1623)	→	1624
1₁(526)	→	527
1₁(1629)	→	1630
1₁(804)	→	805
1₁(1164)	→	1165
1₁(720)	→	721
1₁(855)	→	856
1₁(1169)	→	1170
1₁(267)	→	268
1₁(262)	→	263
1₁(350)	→	351
1₁(714)	→	715
1₁(916)	→	917
1₁(1725)	→	1726
1₁(1755)	→	1756
1₁(1761)	→	1762
1₁(912)	→	913
1₁(1453)	→	1454
1₁(782)	→	783
1₁(1110)	→	1111
1₁(466)	→	467
1₁(1007)	→	1008
1₁(1923)	→	1924
1₁(1561)	→	1562
1₁(1563)	→	1564
1₁(1717)	→	1718
1₁(594)	→	595
1₁(1763)	→	1764
1₁(1509)	→	1510
1₁(307)	→	308
1₁(1181)	→	1182
1₁(754)	→	755
1₁(980)	→	981
1₁(1899)	→	1900
1₁(2099)	→	2100
1₁(1357)	→	1358
1₁(342)	→	343
1₁(654)	→	655
1₁(542)	→	543
1₁(1098)	→	1099
1₁(1173)	→	1174
1₁(395)	→	396
1₁(914)	→	915
1₁(403)	→	404
1₁(1635)	→	1636
1₁(158)	→	159
1₁(936)	→	937
1₁(1919)	→	1920
1₁(1865)	→	1866
1₁(2270)	→	2271
1₁(2101)	→	2102
1₁(1559)	→	1560
1₁(1320)	→	1321
1₁(268)	→	269
1₁(787)	→	788
1₁(1971)	→	1972
1₁(197)	→	198
1₁(853)	→	854
1₁(1667)	→	1668
1₁(1921)	→	1922
1₁(829)	→	830
1₁(725)	→	726
1₁(1465)	→	1466
1₁(708)	→	709
1₁(756)	→	757
1₁(1175)	→	1176
1₁(271)	→	272
1₁(1313)	→	1314
1₁(455)	→	456
1₁(551)	→	552
1₁(2031)	→	2032
1₁(1073)	→	1074
1₁(792)	→	793
1₁(660)	→	661
1₁(221)	→	222
1₁(1077)	→	1078
1₁(1455)	→	1456
1₁(1067)	→	1068
1₁(974)	→	975
1₁(1769)	→	1770
1₁(349)	→	350
1₁(1177)	→	1178
1₁(1856)	→	1857
1₁(1907)	→	1908
1₁(816)	→	817
1₁(1095)	→	1096
1₁(1909)	→	1910
1₁(818)	→	819
1₁(940)	→	941
1₁(305)	→	306
1₁(813)	→	814
1₁(102)	→	103
1₁(1777)	→	1778
1₁(253)	→	254
1₁(1905)	→	1906
1₁(549)	→	550
1₁(1309)	→	1310
1₁(535)	→	536
1₁(1170)	→	1171
1₁(769)	→	770
1₁(21)	→	22
1₁(2037)	→	2038
1₁(999)	→	1000
1₁(1493)	→	1494
1₁(1665)	→	1666
1₁(17)	→	18
1₁(1079)	→	1080
1₁(1659)	→	1660
1₁(1183)	→	1184
1₁(806)	→	807
1₀(3)	→	1
1₀(4)	→	1
1₀(1)	→	1
1₀(2)	→	1
0₀(2)	→	2
0₀(4)	→	2
0₀(3)	→	2
0₀(1)	→	2
3₀(3)	→	4
3₀(2)	→	4
3₀(4)	→	4
3₀(1)	→	4
0₁(664)	→	665
0₁(163)	→	164
0₁(337)	→	338
0₁(397)	→	398
0₁(410)	→	411
0₁(971)	→	972
0₁(779)	→	780
0₁(750)	→	751
0₁(812)	→	813
0₁(1344)	→	1345
0₁(18)	→	19
0₁(149)	→	150
0₁(745)	→	746
0₁(1859)	→	1860
0₁(406)	→	407
0₁(1463)	→	1464
0₁(336)	→	337
0₁(464)	→	465
0₁(2133)	→	2134
0₁(935)	→	936
0₁(874)	→	875
0₁(761)	→	762
0₁(2131)	→	2132
0₁(755)	→	756
0₁(1495)	→	1496
0₁(1281)	→	1282
0₁(1939)	→	1940
0₁(91)	→	92
0₁(719)	→	720
0₁(839)	→	840
0₁(1100)	→	1101
0₁(1651)	→	1652
0₁(1004)	→	1005
0₁(2250)	→	2251
0₁(972)	→	973
0₁(1783)	→	1784
0₁(9)	→	10
0₁(697)	→	698
0₁(414)	→	415
0₁(351)	→	352
0₁(1277)	→	1278
0₁(346)	→	347
0₁(657)	→	658
0₁(1351)	→	1352
0₁(996)	→	997
0₁(941)	→	942
0₁(1005)	→	1006
0₁(2155)	→	2156
0₁(10)	→	11
0₁(850)	→	851
0₁(529)	→	530
0₁(2023)	→	2024
0₁(398)	→	399
0₁(146)	→	147
0₁(460)	→	461
0₁(794)	→	795
0₁(105)	→	106
0₁(2029)	→	2030
0₁(1981)	→	1982
0₁(1096)	→	1097
0₁(452)	→	453
0₁(1217)	→	1218
0₁(716)	→	717
0₁(202)	→	203
0₁(915)	→	916
0₁(1003)	→	1004
0₁(98)	→	99
0₁(213)	→	214
0₁(532)	→	533
0₁(920)	→	921
0₁(973)	→	974
0₁(1854)	→	1855
0₁(1090)	→	1091
0₁(586)	→	587
0₁(1166)	→	1167
0₁(99)	→	100
0₁(910)	→	911
0₁(1933)	→	1934
0₁(2157)	→	2158
0₁(550)	→	551
0₁(860)	→	861
0₁(19)	→	20
0₁(834)	→	835
0₁(453)	→	454
0₁(1278)	→	1279
0₁(1569)	→	1570
0₁(1681)	→	1682
0₁(865)	→	866
0₁(1545)	→	1546
0₁(451)	→	452
0₁(225)	→	226
0₁(1573)	→	1574
0₁(255)	→	256
0₁(810)	→	811
0₁(861)	→	862
0₁(1283)	→	1284
0₁(1611)	→	1612
0₁(833)	→	834
0₁(1675)	→	1676
0₁(1807)	→	1808
0₁(2240)	→	2241
0₁(2242)	→	2243
0₁(1247)	→	1248
0₁(1801)	→	1802
0₁(768)	→	769
0₁(355)	→	356
0₁(1358)	→	1359
0₁(724)	→	725
0₁(1491)	→	1492
0₁(2109)	→	2110
0₁(819)	→	820
0₁(217)	→	218
0₁(1855)	→	1856
0₁(791)	→	792
0₁(159)	→	160
0₁(1093)	→	1094
0₁(546)	→	547
0₁(1347)	→	1348
0₁(465)	→	466
0₁(1881)	→	1882
0₁(1163)	→	1164
0₁(1094)	→	1095
0₁(2280)	→	2281
0₁(222)	→	223
0₁(548)	→	549
0₁(1220)	→	1221
0₁(1168)	→	1169
0₁(1809)	→	1810
0₁(402)	→	403
0₁(352)	→	353
0₁(1356)	→	1357
0₁(2139)	→	2140
0₁(254)	→	255
0₁(341)	→	342
0₁(2115)	→	2116
0₁(1793)	→	1794
0₁(1464)	→	1465
0₁(404)	→	405
0₁(96)	→	97
0₁(1995)	→	1996
0₁(223)	→	224
0₁(840)	→	841
0₁(206)	→	207
0₁(1010)	→	1011
0₁(264)	→	265
0₁(715)	→	716
0₁(747)	→	748
0₁(2252)	→	2253
0₁(589)	→	590
0₁(582)	→	583
0₁(880)	→	881
0₁(1862)	→	1863
0₁(147)	→	148
0₁(1469)	→	1470
0₁(6)	→	7
0₁(985)	→	986
0₁(2045)	→	2046
0₁(1462)	→	1463
0₁(2268)	→	2269
0₁(825)	→	826
0₁(461)	→	462
0₁(1216)	→	1217
0₁(141)	→	142
0₁(1466)	→	1467
0₁(544)	→	545
0₁(661)	→	662
0₁(2266)	→	2267
0₁(749)	→	750
0₁(591)	→	592
0₁(1307)	→	1308
0₁(783)	→	784
0₁(2150)	→	2151
0₁(1852)	→	1853
0₁(2258)	→	2259
0₁(931)	→	932
0₁(759)	→	760
0₁(1099)	→	1100
0₁(1212)	→	1213
0₁(1799)	→	1800
0₁(216)	→	217
0₁(534)	→	535
0₁(1337)	→	1338
0₁(770)	→	771
0₁(2264)	→	2265
0₁(711)	→	712
0₁(1811)	→	1812
0₁(1791)	→	1792
0₁(763)	→	764
0₁(718)	→	719
0₁(1987)	→	1988
0₁(2107)	→	2108
0₁(705)	→	706
0₁(2017)	→	2018
0₁(139)	→	140
0₁(934)	→	935
0₁(1889)	→	1890
0₁(2125)	→	2126
0₁(2015)	→	2016
0₁(836)	→	837
0₁(1075)	→	1076
0₁(1285)	→	1286
0₁(1318)	→	1319
0₁(656)	→	657
0₁(2276)	→	2277
0₁(345)	→	346
0₁(1925)	→	1926
0₁(2009)	→	2010
0₁(2117)	→	2118
0₁(977)	→	978
0₁(7)	→	8
0₁(1470)	→	1471
0₁(807)	→	808
0₁(835)	→	836
0₁(1271)	→	1272
0₁(2238)	→	2239
0₁(699)	→	700
0₁(2260)	→	2261
0₁(767)	→	768
0₁(906)	→	907
0₁(2234)	→	2235
0₁(15)	→	16
0₁(407)	→	408
0₁(1653)	→	1654
0₁(826)	→	827
0₁(1785)	→	1786
0₁(1989)	→	1990
0₁(830)	→	831
0₁(165)	→	166
0₁(764)	→	765
0₁(1412)	→	1413
0₁(1997)	→	1998
0₁(881)	→	882
0₁(878)	→	879
0₁(1001)	→	1002
0₁(1851)	→	1852
0₁(1343)	→	1344
0₁(259)	→	260
0₁(101)	→	102
0₁(2278)	→	2279
0₁(707)	→	708
0₁(409)	→	410
0₁(2286)	→	2287
0₁(22)	→	23
0₁(547)	→	548
0₁(2254)	→	2255
0₁(1102)	→	1103
0₁(103)	→	104
0₁(811)	→	812
0₁(809)	→	810
0₁(704)	→	705
0₁(1410)	→	1411
0₁(900)	→	901
0₁(1575)	→	1576
0₁(2141)	→	2142
0₁(918)	→	919
0₁(1931)	→	1932
0₁(1280)	→	1281
0₁(938)	→	939
0₁(799)	→	800
0₁(20)	→	21
0₁(1085)	→	1086
0₁(1864)	→	1865
0₁(875)	→	876
0₁(703)	→	704
0₁(793)	→	794
0₁(820)	→	821
0₁(1637)	→	1638
0₁(1499)	→	1500
0₁(1306)	→	1307
0₁(1496)	→	1497
0₁(2153)	→	2154
0₁(2021)	→	2022
0₁(859)	→	860
0₁(1475)	→	1476
0₁(1567)	→	1568
0₁(2288)	→	2289
0₁(12)	→	13
0₁(863)	→	864
0₁(1157)	→	1158
0₁(665)	→	666
0₁(412)	→	413
0₁(539)	→	540
0₁(2011)	→	2012
0₁(413)	→	414
0₁(796)	→	797
0₁(97)	→	98
0₁(396)	→	397
0₁(1346)	→	1347
0₁(2152)	→	2153
0₁(2156)	→	2157
0₁(652)	→	653
0₁(1312)	→	1313
0₁(2149)	→	2150
0₁(1645)	→	1646
0₁(60)	→	61
0₁(1308)	→	1309
0₁(1315)	→	1316
0₁(702)	→	703
0₁(975)	→	976
0₁(877)	→	878
0₁(713)	→	714
0₁(790)	→	791
0₁(454)	→	455
0₁(2123)	→	2124
0₁(357)	→	358
0₁(583)	→	584
0₁(998)	→	999
0₁(904)	→	905
0₁(2244)	→	2245
0₁(2262)	→	2263
0₁(536)	→	537
0₁(2236)	→	2237
0₁(871)	→	872
0₁(1314)	→	1315
0₁(1222)	→	1223
0₁(1498)	→	1499
0₁(16)	→	17
0₁(917)	→	918
0₁(266)	→	267
0₁(219)	→	220
0₁(822)	→	823
0₁(261)	→	262
0₁(1273)	→	1274
0₁(943)	→	944
0₁(1267)	→	1268
0₁(553)	→	554
0₁(458)	→	459
0₁(939)	→	940
0₁(2282)	→	2283
0₁(1866)	→	1867
0₁(58)	→	59
0₁(979)	→	980
0₁(596)	→	597
0₁(827)	→	828
0₁(1494)	→	1495
0₁(966)	→	967
0₁(1284)	→	1285
0₁(144)	→	145
0₁(766)	→	767
0₁(970)	→	971
0₁(2232)	→	2233
0₁(541)	→	542
0₁(1265)	→	1266
0₁(199)	→	200
0₁(400)	→	401
0₁(663)	→	664
0₁(746)	→	747
0₁(856)	→	857
0₁(1691)	→	1692
0₁(1006)	→	1007
0₁(1467)	→	1468
0₁(200)	→	201
0₁(903)	→	904
0₁(148)	→	149
0₁(1643)	→	1644
0₁(800)	→	801
0₁(847)	→	848
0₁(2272)	→	2273
0₁(1156)	→	1157
0₁(1319)	→	1320
0₁(991)	→	992
0₁(937)	→	938
0₁(2003)	→	2004
0₁(160)	→	161
0₁(207)	→	208
0₁(1873)	→	1874
0₁(1161)	→	1162
0₁(2284)	→	2285
0₁(925)	→	926
0₁(1375)	→	1376
0₁(712)	→	713
0₁(1354)	→	1355
0₁(808)	→	809
0₁(153)	→	154
0₁(1697)	→	1698
0₁(987)	→	988
0₁(911)	→	912
2₀(1)	→	3
2₀(2)	→	3
2₀(3)	→	3
2₀(4)	→	3

The automaton is closed under rewriting as it is compatible.