Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4920)

The rewrite relation of the following TRS is considered.

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

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:

1405	→	213
1405	→	1491
1374	→	705
1839	→	974
854	→	492
1243	→	1705
2073	→	624
2073	→	2176
1151	→	805
1380	→	711
867	→	707
793	→	877
793	→	945
793	→	1255
793	→	1844
429	→	2
429	→	786
429	→	285
429	→	658
429	→	600
591	→	2418
650	→	320
650	→	1119
1627	→	795
587	→	561
587	→	1359
2421	→	2342
1940	→	2271
1940	→	2331
2393	→	8
2393	→	2398
2393	→	2406
633	→	5
633	→	711
633	→	312
633	→	343
633	→	601
633	→	610
633	→	766
633	→	623
633	→	323
633	→	1221
917	→	908
486	→	684
486	→	1166
315	→	1361
2216	→	2203
835	→	100
1459	→	768
2338	→	774
589	→	561
589	→	918
1845	→	974
2340	→	774
1463	→	320
1333	→	1855
1333	→	1872
1333	→	1902
1333	→	1965
860	→	847
860	→	1667
1117	→	1950
1117	→	2186
1089	→	820
1089	→	538
1089	→	92
1089	→	584
1089	→	340
1089	→	142
1089	→	68
1089	→	246
1089	→	419
1089	→	4
1089	→	507
1089	→	118
1089	→	796
794	→	4
794	→	741
794	→	141
794	→	164
794	→	214
794	→	813
794	→	287
794	→	732
794	→	740
794	→	516
794	→	162
794	→	1621
2141	→	642
2181	→	847
214	→	164
214	→	741
897	→	2048
1354	→	485
10	→	485
1163	→	507
1163	→	1280
1163	→	2174
2297	→	2278
1169	→	9
2247	→	2420
1557	→	642
2173	→	786
2198	→	2392
537	→	508
537	→	731
2218	→	2203
915	→	622
915	→	702
915	→	861
915	→	1
915	→	449
294	→	1164
294	→	1421
1794	→	878
2183	→	847
1046	→	1034
1046	→	1381
1867	→	1856
561	→	642
561	→	667
561	→	920
561	→	863
561	→	6
561	→	781
561	→	421
561	→	907
561	→	583
561	→	2157
2105	→	599
1237	→	609
1237	→	1948
886	→	2241
1473	→	784
641	→	625
2185	→	847
933	→	10
1979	→	9
2131	→	213
2131	→	2170
2211	→	2394
608	→	5
608	→	711
608	→	377
608	→	312
608	→	323
608	→	623
608	→	621
2099	→	599
1498	→	2249
2133	→	213
2133	→	2172
1386	→	712
2330	→	213
1977	→	1966
2399	→	287
2242	→	9
668	→	1150
668	→	1367
878	→	2038
491	→	1299
491	→	1377
585	→	561
585	→	916
585	→	6
585	→	1209
585	→	485
585	→	10
585	→	933
2097	→	599
2097	→	2360
18	→	1
18	→	765
18	→	622
18	→	702
18	→	861
18	→	449
1964	→	410
1118	→	682
1118	→	2106
643	→	749
643	→	757
643	→	773
643	→	120
643	→	584
643	→	340
643	→	142
643	→	68
643	→	246
643	→	419
643	→	4
643	→	864
2047	→	711
2047	→	377
2047	→	312
120	→	92
3	→	66
3	→	140
3	→	284
3	→	360
3	→	446
3	→	580
583	→	561
583	→	907
1362	→	685
1506	→	1492
2063	→	320
600	→	658
600	→	786
812	→	793
772	→	320
1254	→	1243
617	→	385
225	→	3
225	→	599
225	→	213
225	→	562
225	→	9
225	→	44
1324	→	1314
1613	→	806
1812	→	92
2149	→	642
626	→	1083
1294	→	711
1294	→	312
1294	→	610
1294	→	5
1294	→	766
1294	→	623
1294	→	323
740	→	732
740	→	813
2012	→	100
919	→	908
919	→	1321
1467	→	775
411	→	1678
2049	→	2039
9	→	213
9	→	387
9	→	599
9	→	1168
9	→	1616
1714	→	245
1714	→	588
1714	→	342
1714	→	161
1714	→	89
1714	→	264
1714	→	448
1714	→	2
1714	→	703
1706	→	1723
914	→	1776
914	→	1813
914	→	2080
1332	→	1904
1332	→	1928
1332	→	2054
1332	→	2190
1332	→	2302
5	→	8
5	→	91
5	→	266
5	→	358
5	→	464
5	→	560
341	→	312
2175	→	642
2107	→	314
515	→	17
642	→	2160
598	→	3
598	→	90
598	→	552
1126	→	847
1124	→	1114
2103	→	599
2289	→	2278
1027	→	287
1027	→	1400
1681	→	831
319	→	2277
361	→	312
891	→	878
1183	→	1177
1252	→	711
1252	→	312
1252	→	560
1252	→	358
1252	→	91
1252	→	8
1252	→	266
1252	→	464
1252	→	5
1252	→	343
1252	→	1221
765	→	828
2179	→	847
2409	→	668
2361	→	806
756	→	385
756	→	1460
1082	→	711
1082	→	312
1082	→	560
1082	→	358
1082	→	91
1082	→	8
1082	→	266
1082	→	464
1082	→	5
1082	→	343
1082	→	1219
1929	→	100
1806	→	92
889	→	878
2311	→	668
90	→	9
90	→	194
90	→	1614
193	→	164
99	→	896
99	→	934
99	→	973
99	→	1242
467	→	420
467	→	609
467	→	636
467	→	857
1159	→	507
1890	→	562
1890	→	1616
1890	→	599
1890	→	213
1890	→	9
1890	→	44
224	→	1154
713	→	2275
942	→	632
2373	→	377
1403	→	213
1403	→	1509
1034	→	1073
2057	→	320
1	→	41
1	→	117
1	→	244
1	→	322
1	→	483
1	→	582
1430	→	750
2295	→	2278
2291	→	2278
287	→	590
1040	→	606
2055	→	320
1730	→	2148
1730	→	2164
690	→	417
1298	→	1285
1298	→	2110
1837	→	974
2423	→	786
1331	→	2298
1081	→	1980
2256	→	100
1004	→	994
895	→	878
1994	→	313
101	→	2
101	→	267
101	→	739
101	→	517
101	→	247
101	→	539
570	→	3
570	→	599
570	→	213
570	→	562
570	→	9
570	→	44
570	→	797
570	→	163
570	→	69
570	→	1558
570	→	750
570	→	1434
570	→	2101
570	→	2330
2357	→	806
1713	→	1793
1713	→	1821
1713	→	2088
2293	→	2278
416	→	1353
1722	→	707
1319	→	2294
1173	→	1406
1173	→	1505
1173	→	1612
1215	→	711
1215	→	5
1215	→	377
1215	→	312
428	→	1464
2212	→	561
2212	→	1209
2212	→	485
2212	→	10
2212	→	933
747	→	1301
747	→	1379
747	→	1880
2334	→	213
44	→	9
1283	→	645
1283	→	1721
2169	→	774
2395	→	8
2395	→	2400
2395	→	2408
748	→	632
748	→	1003
796	→	820
796	→	1327
796	→	538
796	→	92
796	→	584
796	→	340
796	→	142
796	→	68
796	→	246
796	→	419
796	→	4
796	→	507
796	→	118
323	→	312
343	→	312
343	→	1208
1428	→	750
675	→	607
2250	→	878
1654	→	822
1157	→	507
1982	→	2352
385	→	1152
562	→	805
2087	→	624
2087	→	2182
2087	→	2335
2222	→	2203
1881	→	2027
2305	→	668
2214	→	2203
1499	→	1770
1499	→	1805
1499	→	1842
1499	→	2072
1499	→	2247
1214	→	2292
141	→	92
141	→	1007
493	→	2
493	→	267
493	→	245
493	→	703
1944	→	2263
1944	→	2327
983	→	313
1453	→	757
1453	→	2166
2224	→	377
509	→	1373
2155	→	757
2155	→	2339
172	→	1
172	→	765
172	→	622
172	→	702
172	→	861
172	→	449
1322	→	1314
779	→	1398
597	→	894
597	→	951
597	→	1269
1382	→	712
171	→	1125
171	→	1156
171	→	1402
2071	→	320
2199	→	2372
2199	→	2386
2199	→	2404
2199	→	2412
639	→	625
6	→	43
6	→	119
6	→	215
6	→	311
6	→	466
6	→	586
2407	→	668
1235	→	609
1865	→	828
1865	→	765
1256	→	1243
921	→	908
921	→	1323
1042	→	1034
1042	→	1383
2081	→	624
2081	→	2180
1438	→	757
1438	→	2168
1927	→	1905
1302	→	1285
384	→	2005
2065	→	320
394	→	2215
386	→	5
386	→	711
386	→	312
386	→	343
386	→	610
386	→	766
386	→	623
386	→	323
386	→	1219
386	→	1233
1292	→	2288
2111	→	713
484	→	420
484	→	620
484	→	634
484	→	855
288	→	1282
2200	→	1297
2200	→	1043
2200	→	100
2200	→	711
2200	→	312
2200	→	2102
2200	→	1944
2200	→	2025
2200	→	464
2200	→	266
2200	→	8
2200	→	91
2200	→	358
2200	→	560
2200	→	5
2200	→	359
2200	→	1945
2200	→	2203
2200	→	1073
2200	→	1034
2200	→	1385
2200	→	1044
2200	→	2222
1205	→	591
1205	→	1466
1293	→	1946
1293	→	2070
1293	→	2096
1293	→	2310
2171	→	786
1181	→	599
1181	→	213
1181	→	562
1181	→	3
1181	→	9
1181	→	44
67	→	9
67	→	192
2010	→	1986
2035	→	1889
538	→	1942
538	→	2062
538	→	2100
2274	→	100
2287	→	610
2287	→	623
665	→	1045
665	→	1238
665	→	1284
1180	→	1940
1180	→	2056
1180	→	2098
1500	→	741
1500	→	141
1500	→	584
1500	→	340
1500	→	142
1500	→	68
1500	→	246
1500	→	419
1500	→	4
1500	→	164
1500	→	214
906	→	622
906	→	702
906	→	861
906	→	449
906	→	828
906	→	765
906	→	2009
143	→	92
143	→	536
2262	→	100
569	→	1041
569	→	1234
569	→	1295
2351	→	610
2351	→	766
2351	→	623
803	→	1454
2248	→	319
2248	→	2416
1672	→	2290
2	→	89
2	→	161
2	→	264
2	→	342
2	→	448
2	→	588
2008	→	1987
2161	→	642
2165	→	320
1679	→	830
2411	→	9
4	→	68
4	→	142
4	→	246
4	→	340
4	→	419
4	→	584
941	→	2138
265	→	216
265	→	1232
804	→	4
804	→	773
804	→	749
804	→	120
804	→	864
804	→	757
804	→	643
118	→	92
118	→	507
449	→	420
1504	→	1492
1945	→	100
876	→	1
876	→	828
876	→	861
876	→	702
876	→	622
876	→	420
876	→	449
876	→	765
827	→	417
1779	→	878
1451	→	642
1001	→	1982
1814	→	92
508	→	1620
2417	→	773
1015	→	599
359	→	312
359	→	560
359	→	358
359	→	91
359	→	8
359	→	266
359	→	464
359	→	5
359	→	2203
359	→	2222
379	→	676
2147	→	757
2147	→	2337
1155	→	417
1155	→	1452
1879	→	217
16	→	1435
2209	→	2410
1461	→	320
1843	→	974
862	→	847
862	→	1123
913	→	2140
2254	→	1986
421	→	781
421	→	863
887	→	765
887	→	420
887	→	449
887	→	2253
795	→	2156
1334	→	773
1334	→	749
1334	→	120
1334	→	584
1334	→	340
1334	→	142
1334	→	68
1334	→	246
1334	→	419
1334	→	4
1334	→	864
1334	→	757
1334	→	643
93	→	1653
1962	→	391
2006	→	1985
1270	→	1243
623	→	610
738	→	665
581	→	561
985	→	163
1143	→	425
1221	→	1208
559	→	224
559	→	1462
1436	→	642
2101	→	599
2101	→	2358
2353	→	2342
100	→	932
100	→	1043
100	→	1236
100	→	1297
1296	→	1285
1771	→	878
1378	→	711
1455	→	642
1219	→	1208
1432	→	750
1432	→	1551
944	→	935
1559	→	798
1044	→	1034
1044	→	1385
2264	→	100
1006	→	997
1958	→	2225
621	→	610
1401	→	731
295	→	3
295	→	599
295	→	213
295	→	562
295	→	9
295	→	44
1399	→	536
1873	→	163
2177	→	847
1943	→	100
1980	→	2341
2387	→	100
217	→	1472
635	→	625
69	→	9
69	→	163
1983	→	319
1983	→	2154
1080	→	1984
2202	→	2191
758	→	1005
2187	→	846
710	→	171
806	→	1144
2276	→	647
1239	→	609
42	→	9
719	→	569
216	→	286
216	→	551
216	→	764
681	→	1033
681	→	1240
681	→	1926
681	→	2201
1122	→	1114
2299	→	2278
2079	→	624
2079	→	2178
162	→	92
162	→	516
950	→	935
950	→	1431
637	→	625
1510	→	786
1384	→	712
856	→	847
847	→	868
2332	→	213
948	→	935
948	→	1429
893	→	878
763	→	616
2270	→	100
952	→	935
1975	→	786
1975	→	658
1975	→	600
2139	→	642
905	→	1978
1025	→	288
245	→	216
245	→	1218
17	→	888
17	→	943
17	→	1253
946	→	935
946	→	1427
1149	→	267
683	→	4
683	→	773
683	→	749
683	→	120
683	→	864
683	→	757
683	→	643
1822	→	92
164	→	1961
1148	→	1778
1148	→	1819
1148	→	1878
1148	→	2086
2328	→	213
2401	→	287
2401	→	2414
666	→	5
666	→	711
666	→	312
666	→	610
666	→	766
666	→	623
666	→	323
666	→	359
666	→	1297
666	→	1043
666	→	100
666	→	1945
2405	→	2279
1407	→	741
1928	→	2261
1928	→	2325
2220	→	2203
703	→	1680
2324	→	213
2324	→	2354
267	→	216
267	→	588
267	→	342
267	→	161
267	→	89
267	→	264
267	→	448
267	→	2
267	→	313
2210	→	2424
517	→	508
858	→	847
1153	→	417
1153	→	1437
492	→	890
492	→	947
492	→	993
492	→	1263
2109	→	711
320	→	1162
320	→	1172
320	→	1311
320	→	2219
1087	→	2213
2026	→	100
1266	→	1243
1796	→	878
1368	→	685
1457	→	765
2226	→	377
1422	→	213
1422	→	1503
285	→	216
1360	→	685
1434	→	750
1434	→	1558
1281	→	644
1264	→	1243
465	→	420
465	→	624
465	→	846
848	→	1121
670	→	1142
2355	→	786
378	→	410
1120	→	1112
1959	→	2203
1959	→	2223
1959	→	2255
1959	→	2323
649	→	2217
1165	→	507
92	→	538
92	→	1024
92	→	1204
92	→	1433
1002	→	599
1002	→	213
1002	→	562
1002	→	3
1002	→	9
1002	→	44
358	→	2025
358	→	2132
358	→	2221
1903	→	287
1903	→	2124
2272	→	100
2303	→	668
2415	→	750
195	→	164
1947	→	100
2125	→	731
1233	→	1208
1251	→	1795
1251	→	1811
1251	→	1836
1251	→	2078
1320	→	323
1320	→	623
1320	→	5
1320	→	621
1942	→	2269
1942	→	2329
611	→	1458
418	→	6
418	→	667
418	→	642
418	→	561
418	→	217
418	→	589
418	→	863
418	→	781
418	→	421
418	→	583
418	→	1209
418	→	2157
418	→	485
418	→	10
418	→	933
266	→	1944
266	→	2064
266	→	2102
1241	→	609
1777	→	878
785	→	614
396	→	4
396	→	820
396	→	538
396	→	92
396	→	507
396	→	118
396	→	796
875	→	1450
875	→	1456
1615	→	806
632	→	892
632	→	949
632	→	1265
632	→	1838
447	→	420
447	→	638
447	→	859
1167	→	556
1167	→	1182
321	→	5
321	→	711
321	→	312
321	→	359
321	→	610
321	→	623
321	→	323
321	→	343
321	→	1233
321	→	1297
321	→	1043
321	→	100
321	→	1945
321	→	2203
321	→	2222
682	→	984
682	→	1026
682	→	1866
682	→	1976
2413	→	213
2413	→	2422
539	→	508
539	→	739
539	→	764
539	→	286
539	→	517
539	→	2
539	→	216
539	→	247
1088	→	1963
1088	→	2011
1088	→	2130
2359	→	806
2326	→	213
2326	→	2356
2419	→	775
1949	→	379
1981	→	319
1981	→	2146
2336	→	610
1465	→	773
312	→	377
312	→	711
1300	→	1285
395	→	1111
395	→	1158
395	→	1404
1147	→	2104
1147	→	2108
780	→	632
2425	→	417
1617	→	806
2167	→	774
1941	→	100
607	→	2296
819	→	803
1914	→	562
1914	→	1616
1914	→	599
1914	→	213
1914	→	9
1914	→	44
1946	→	2273
1946	→	2333
1960	→	1327
1960	→	118
1960	→	584
1960	→	340
1960	→	142
1960	→	68
1960	→	246
1960	→	419
1960	→	4
1960	→	820
1960	→	796
1820	→	92
247	→	216
247	→	1220
1731	→	828
1731	→	861
1731	→	702
1731	→	622
1731	→	1
1731	→	420
1731	→	449
1731	→	765
879	→	2007
1673	→	538
1673	→	2304
2157	→	642
2089	→	624
2089	→	2184
420	→	622
420	→	640
420	→	702
420	→	795
420	→	861
1₁(1946)	→	1947
1₁(2372)	→	2373
1₁(911)	→	912
1₁(1220)	→	1221
1₁(765)	→	766
1₁(95)	→	96
1₁(1669)	→	1670
1₁(1287)	→	1288
1₁(2360)	→	2361
1₁(600)	→	601
1₁(622)	→	623
1₁(487)	→	488
1₁(817)	→	818
1₁(910)	→	911
1₁(1377)	→	1378
1₁(1176)	→	1177
1₁(170)	→	171
1₁(358)	→	359
1₁(1313)	→	1314
1₁(938)	→	939
1₁(761)	→	762
1₁(360)	→	361
1₁(1379)	→	1380
1₁(659)	→	660
1₁(1024)	→	1025
1₁(2223)	→	2224
1₁(670)	→	671
1₁(322)	→	323
1₁(1625)	→	1626
1₁(1555)	→	1556
1₁(1321)	→	1322
1₁(1317)	→	1318
1₁(1007)	→	1008
1₁(1614)	→	1615
1₁(1114)	→	1115
1₁(673)	→	674
1₁(1045)	→	1046
1₁(1724)	→	1725
1₁(646)	→	647
1₁(1087)	→	1088
1₁(1458)	→	1459
1₁(1033)	→	1034
1₁(2225)	→	2226
1₁(806)	→	807
1₁(394)	→	395
1₁(787)	→	788
1₁(801)	→	802
1₁(1014)	→	1015
1₁(412)	→	413
1₁(292)	→	293
1₁(342)	→	343
1₁(647)	→	648
1₁(649)	→	650
1₁(767)	→	768
1₁(1012)	→	1013
1₁(510)	→	511
1₁(733)	→	734
1₁(1711)	→	1712
1₁(808)	→	809
1₁(340)	→	341
1₁(383)	→	384
1₁(96)	→	97
1₁(1145)	→	1146
1₁(609)	→	610
1₁(734)	→	735
1₁(1182)	→	1183
1₁(1612)	→	1613
1₁(939)	→	940
1₁(1493)	→	1494
1₁(2335)	→	2336
1₁(1218)	→	1219
1₁(1041)	→	1042
1₁(311)	→	312
1₁(423)	→	424
1₁(643)	→	644
1₁(1043)	→	1044
1₁(852)	→	853
1₁(869)	→	870
1₁(593)	→	594
1₁(775)	→	776
1₁(620)	→	621
1₁(2358)	→	2359
1₁(758)	→	759
1₁(320)	→	321
1₁(1721)	→	1722
1₁(13)	→	14
1₁(716)	→	717
1₁(1940)	→	1941
1₁(1280)	→	1281
1₁(866)	→	867
1₁(2108)	→	2109
1₁(1327)	→	1328
1₁(1942)	→	1943
1₁(395)	→	396
1₁(613)	→	614
1₁(826)	→	827
1₁(171)	→	172
1₁(14)	→	15
1₁(2275)	→	2276
1₁(805)	→	806
1₁(746)	→	747
1₁(864)	→	865
1₁(1079)	→	1080
1₁(769)	→	770
1₁(1232)	→	1233
1₁(514)	→	515
1₁(565)	→	566
1₁(676)	→	677
1₁(1323)	→	1324
1₁(1616)	→	1617
1₁(1944)	→	1945
1₁(294)	→	295
1₁(669)	→	670
1₁(1088)	→	1089
1₁(1725)	→	1726
1₁(489)	→	490
1₁(2356)	→	2357
1₁(998)	→	999
1₁(164)	→	165
1₁(287)	→	288
1₁(870)	→	871
1₁(714)	→	715
1₁(1314)	→	1315
1₁(221)	→	222
1₁(557)	→	558
1₁(1928)	→	1929
1₁(831)	→	832
5₂(1951)	→	1952
5₂(1965)	→	1966
5₂(974)	→	975
5₂(2349)	→	2350
5₂(1976)	→	1977
5₂(2208)	→	2209
5₂(2210)	→	2211
5₂(2204)	→	2205
5₂(2203)	→	2204
0₂(1950)	→	1951
0₂(1795)	→	1796
0₂(1987)	→	1988
0₂(880)	→	881
0₂(981)	→	982
0₂(1971)	→	1972
0₂(877)	→	878
0₂(2280)	→	2281
0₂(1770)	→	1771
0₂(894)	→	895
0₂(1912)	→	1913
0₂(1888)	→	1889
0₂(976)	→	977
0₂(975)	→	976
0₂(1855)	→	1856
0₂(2027)	→	2028
0₂(888)	→	889
0₂(1993)	→	1994
0₂(1793)	→	1794
0₂(1859)	→	1860
0₂(2249)	→	2250
0₂(2045)	→	2046
0₂(1954)	→	1955
0₂(2042)	→	2043
0₂(2028)	→	2029
0₂(1970)	→	1971
0₂(905)	→	906
0₂(1778)	→	1779
0₂(2005)	→	2006
0₂(2346)	→	2347
0₂(1952)	→	1953
0₂(1884)	→	1885
0₂(896)	→	897
0₂(2350)	→	2351
0₂(2195)	→	2196
0₂(892)	→	893
0₂(2209)	→	2210
0₂(899)	→	900
0₂(2197)	→	2198
0₂(1866)	→	1867
0₂(886)	→	887
0₂(2196)	→	2197
0₂(2043)	→	2044
0₂(890)	→	891
0₂(1984)	→	1985
0₂(1776)	→	1777
4₂(2041)	→	2042
4₂(2034)	→	2035
4₂(1909)	→	1910
4₂(879)	→	880
4₂(1968)	→	1969
4₂(2044)	→	2045
4₂(1883)	→	1884
4₂(898)	→	899
4₂(2048)	→	2049
4₂(2032)	→	2033
4₂(1904)	→	1905
4₂(1926)	→	1927
4₂(1956)	→	1957
4₂(982)	→	983
4₂(1880)	→	1881
4₂(1992)	→	1993
4₂(2191)	→	2192
4₂(2038)	→	2039
5₁(419)	→	420
5₁(1236)	→	1237
5₁(1359)	→	1360
5₁(2178)	→	2179
5₁(1238)	→	1239
5₁(1367)	→	1368
5₁(677)	→	678
5₁(1073)	→	1074
5₁(2080)	→	2081
5₁(377)	→	378
5₁(2070)	→	2071
5₁(410)	→	411
5₁(1497)	→	1498
5₁(1706)	→	1707
5₁(1622)	→	1623
5₁(1116)	→	1117
5₁(1240)	→	1241
5₁(1234)	→	1235
5₁(1705)	→	1706
5₁(682)	→	683
5₁(1556)	→	1557
5₁(2086)	→	2087
5₁(814)	→	815
5₁(2174)	→	2175
5₁(791)	→	792
5₁(2424)	→	2425
5₁(828)	→	829
5₁(820)	→	821
5₁(1330)	→	1331
5₁(2164)	→	2165
5₁(483)	→	484
5₁(2064)	→	2065
5₁(1333)	→	1334
5₁(2180)	→	2181
5₁(2088)	→	2089
5₁(1269)	→	1270
5₁(859)	→	860
5₁(1111)	→	1112
5₁(861)	→	862
5₁(1112)	→	1113
5₁(779)	→	780
5₁(847)	→	848
5₁(1456)	→	1457
5₁(825)	→	826
5₁(1119)	→	1120
5₁(1265)	→	1266
5₁(446)	→	447
5₁(2182)	→	2183
5₁(846)	→	847
5₁(92)	→	93
5₁(674)	→	675
5₁(1329)	→	1330
5₁(1253)	→	1254
5₁(464)	→	465
5₁(802)	→	803
5₁(1318)	→	1319
5₁(387)	→	388
5₁(1460)	→	1461
5₁(611)	→	612
5₁(1242)	→	1243
5₁(678)	→	679
5₁(935)	→	936
5₁(1462)	→	1463
5₁(679)	→	680
5₁(768)	→	769
5₁(2186)	→	2187
5₁(448)	→	449
5₁(1255)	→	1256
5₁(857)	→	858
5₁(1963)	→	1964
5₁(466)	→	467
5₁(783)	→	784
5₁(2072)	→	2073
5₁(823)	→	824
5₁(1263)	→	1264
5₁(1328)	→	1329
5₁(764)	→	765
5₁(2062)	→	2063
5₁(1125)	→	1126
5₁(2054)	→	2055
5₁(2176)	→	2177
5₁(2184)	→	2185
5₁(2078)	→	2079
5₁(684)	→	685
5₁(855)	→	856
5₁(1472)	→	1473
5₁(414)	→	415
5₁(416)	→	417
5₁(1361)	→	1362
5₁(2056)	→	2057
1₀(3)	→	5
1₀(6)	→	5
1₀(5)	→	5
1₀(4)	→	5
1₀(2)	→	5
1₀(1)	→	5
3₀(2)	→	6
3₀(6)	→	6
3₀(4)	→	6
3₀(1)	→	6
3₀(3)	→	6
3₀(5)	→	6
3₂(1989)	→	1990
3₂(1907)	→	1908
3₂(878)	→	879
3₂(2290)	→	2291
3₂(1966)	→	1967
3₂(2298)	→	2299
3₂(2296)	→	2297
3₂(2288)	→	2289
3₂(2009)	→	2010
3₂(2031)	→	2032
3₂(1861)	→	1862
3₂(2211)	→	2212
3₂(2207)	→	2208
3₂(2284)	→	2285
3₂(1885)	→	1886
3₂(2352)	→	2353
3₂(2007)	→	2008
3₂(1985)	→	1986
3₂(2192)	→	2193
3₂(2046)	→	2047
3₂(1974)	→	1975
3₂(1986)	→	1987
3₂(2292)	→	2293
3₂(1881)	→	1882
3₂(2198)	→	2199
3₂(2030)	→	2031
3₂(2420)	→	2421
3₂(897)	→	898
3₂(2277)	→	2278
3₂(2348)	→	2349
3₂(881)	→	882
3₂(2193)	→	2194
3₂(1973)	→	1974
3₂(2029)	→	2030
3₂(2343)	→	2344
3₂(2253)	→	2254
3₂(1858)	→	1859
3₂(2344)	→	2345
3₂(2341)	→	2342
3₂(2040)	→	2041
3₂(2294)	→	2295
3₂(1967)	→	1968
3₂(900)	→	901
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
2₁(1123)	→	1124
2₁(912)	→	913
2₁(286)	→	287
2₁(1247)	→	1248
2₁(140)	→	141
2₁(1158)	→	1159
2₁(1730)	→	1731
2₁(512)	→	513
2₁(1948)	→	1949
2₁(1464)	→	1465
2₁(934)	→	935
2₁(490)	→	491
2₁(142)	→	143
2₁(1620)	→	1621
2₁(97)	→	98
2₁(1164)	→	1165
2₁(1452)	→	1453
2₁(192)	→	193
2₁(1626)	→	1627
2₁(994)	→	995
2₁(2263)	→	2264
2₁(2386)	→	2387
2₁(2416)	→	2417
2₁(1146)	→	1147
2₁(391)	→	392
2₁(628)	→	629
2₁(824)	→	825
2₁(98)	→	99
2₁(1653)	→	1654
2₁(1084)	→	1085
2₁(1494)	→	1495
2₁(1086)	→	1087
2₁(222)	→	223
2₁(686)	→	687
2₁(1009)	→	1010
2₁(117)	→	118
2₁(1037)	→	1038
2₁(378)	→	379
2₁(671)	→	672
2₁(741)	→	742
2₁(1001)	→	1002
2₁(169)	→	170
2₁(1162)	→	1163
2₁(663)	→	664
2₁(810)	→	811
2₁(1081)	→	1082
2₁(913)	→	914
2₁(940)	→	941
2₁(798)	→	799
2₁(2011)	→	2012
2₁(821)	→	822
2₁(2271)	→	2272
2₁(509)	→	510
2₁(393)	→	394
2₁(411)	→	412
2₁(661)	→	662
2₁(1624)	→	1625
2₁(385)	→	386
2₁(625)	→	626
2₁(731)	→	732
2₁(739)	→	740
2₁(167)	→	168
2₁(736)	→	737
2₁(161)	→	162
2₁(1121)	→	1122
2₁(15)	→	16
2₁(803)	→	804
2₁(1077)	→	1078
2₁(1026)	→	1027
2₁(1437)	→	1438
2₁(872)	→	873
2₁(194)	→	195
2₁(2269)	→	2270
2₁(735)	→	736
2₁(951)	→	952
2₁(1552)	→	1553
2₁(119)	→	120
2₁(289)	→	290
2₁(777)	→	778
2₁(1819)	→	1820
2₁(16)	→	17
2₁(2110)	→	2111
2₁(788)	→	789
2₁(1406)	→	1407
2₁(217)	→	218
2₁(1315)	→	1316
2₁(947)	→	948
2₁(224)	→	225
2₁(381)	→	382
2₁(943)	→	944
2₁(592)	→	593
2₁(1244)	→	1245
2₁(712)	→	713
2₁(875)	→	876
2₁(1398)	→	1399
2₁(707)	→	708
2₁(163)	→	164
2₁(737)	→	738
2₁(945)	→	946
2₁(2025)	→	2026
2₁(809)	→	810
2₁(1492)	→	1493
2₁(610)	→	611
2₁(2154)	→	2155
2₁(949)	→	950
2₁(784)	→	785
2₁(863)	→	864
2₁(1805)	→	1806
2₁(642)	→	643
2₁(1727)	→	1728
2₁(786)	→	787
2₁(612)	→	613
2₁(1813)	→	1814
2₁(615)	→	616
2₁(91)	→	92
2₁(999)	→	1000
2₁(1821)	→	1822
2₁(1902)	→	1903
2₁(291)	→	292
2₁(315)	→	316
2₁(1113)	→	1114
2₁(941)	→	942
2₁(2261)	→	2262
2₁(2398)	→	2399
2₁(389)	→	390
2₁(751)	→	752
2₁(1156)	→	1157
2₁(426)	→	427
2₁(1811)	→	1812
2₁(818)	→	819
2₁(1074)	→	1075
2₁(715)	→	716
2₁(2400)	→	2401
2₁(1291)	→	1292
2₁(2255)	→	2256
2₁(1011)	→	1012
2₁(795)	→	796
2₁(645)	→	646
2₁(2273)	→	2274
2₁(2146)	→	2147
2₁(1289)	→	1290
2₁(213)	→	214
2₁(766)	→	767
2₁(816)	→	817
4₁(1075)	→	1076
4₁(995)	→	996
4₁(284)	→	285
4₁(1509)	→	1510
4₁(742)	→	743
4₁(568)	→	569
4₁(602)	→	603
4₁(781)	→	782
4₁(2354)	→	2355
4₁(750)	→	751
4₁(1293)	→	1294
4₁(2172)	→	2173
4₁(757)	→	758
4₁(290)	→	291
4₁(1178)	→	1179
4₁(1212)	→	1213
4₁(266)	→	267
4₁(312)	→	313
4₁(1726)	→	1727
4₁(1667)	→	1668
4₁(681)	→	682
4₁(732)	→	733
4₁(1034)	→	1035
4₁(1180)	→	1181
4₁(1670)	→	1671
4₁(2170)	→	2171
4₁(874)	→	875
4₁(1709)	→	1710
4₁(832)	→	833
4₁(1312)	→	1313
4₁(491)	→	492
4₁(920)	→	921
4₁(1400)	→	1401
4₁(569)	→	570
4₁(215)	→	216
4₁(916)	→	917
4₁(558)	→	559
4₁(1085)	→	1086
4₁(907)	→	908
4₁(2422)	→	2423
4₁(536)	→	537
4₁(755)	→	756
4₁(1147)	→	1148
4₁(1503)	→	1504
4₁(1623)	→	1624
4₁(218)	→	219
4₁(1010)	→	1011
4₁(422)	→	423
4₁(850)	→	851
4₁(1729)	→	1730
4₁(392)	→	393
4₁(599)	→	600
4₁(605)	→	606
4₁(918)	→	919
4₁(264)	→	265
4₁(1678)	→	1679
4₁(507)	→	508
4₁(1209)	→	1210
4₁(508)	→	509
4₁(815)	→	816
4₁(754)	→	755
4₁(244)	→	245
4₁(10)	→	11
4₁(1332)	→	1333
4₁(1285)	→	1286
4₁(1505)	→	1506
4₁(689)	→	690
4₁(760)	→	761
4₁(871)	→	872
4₁(567)	→	568
4₁(747)	→	748
4₁(2124)	→	2125
4₁(556)	→	557
4₁(665)	→	666
4₁(1491)	→	1492
4₁(703)	→	704
4₁(100)	→	101
4₁(1179)	→	1180
4₁(702)	→	703
4₁(516)	→	517
4₁(379)	→	380
4₁(668)	→	669
4₁(246)	→	247
4₁(829)	→	830
4₁(538)	→	539
4₀(3)	→	2
4₀(5)	→	2
4₀(2)	→	2
4₀(4)	→	2
4₀(1)	→	2
4₀(6)	→	2
0₀(2)	→	3
0₀(4)	→	3
0₀(3)	→	3
0₀(6)	→	3
0₀(1)	→	3
0₀(5)	→	3
0₁(627)	→	628
0₁(606)	→	607
0₁(711)	→	712
0₁(1383)	→	1384
0₁(1013)	→	1014
0₁(94)	→	95
0₁(17)	→	18
0₁(1498)	→	1499
0₁(317)	→	318
0₁(166)	→	167
0₁(1288)	→	1289
0₁(771)	→	772
0₁(776)	→	777
0₁(1005)	→	1006
0₁(796)	→	797
0₁(1150)	→	1151
0₁(1251)	→	1252
0₁(513)	→	514
0₁(492)	→	493
0₁(640)	→	641
0₁(2132)	→	2133
0₁(1402)	→	1403
0₁(1301)	→	1302
0₁(807)	→	808
0₁(2327)	→	2328
0₁(2331)	→	2332
0₁(384)	→	385
0₁(1213)	→	1214
0₁(865)	→	866
0₁(382)	→	383
0₁(624)	→	625
0₁(632)	→	633
0₁(1499)	→	1500
0₁(709)	→	710
0₁(799)	→	800
0₁(636)	→	637
0₁(660)	→	661
0₁(937)	→	938
0₁(1404)	→	1405
0₁(41)	→	42
0₁(390)	→	391
0₁(1433)	→	1434
0₁(936)	→	937
0₁(1680)	→	1681
0₁(425)	→	426
0₁(223)	→	224
0₁(2414)	→	2415
0₁(848)	→	849
0₁(597)	→	598
0₁(2104)	→	2105
0₁(561)	→	562
0₁(89)	→	90
0₁(219)	→	220
0₁(1282)	→	1283
0₁(1421)	→	1422
0₁(8)	→	9
0₁(591)	→	592
0₁(868)	→	869
0₁(2130)	→	2131
0₁(2333)	→	2334
0₁(511)	→	512
0₁(1083)	→	1084
0₁(318)	→	319
0₁(1168)	→	1169
0₁(1385)	→	1386
0₁(1553)	→	1554
0₁(1080)	→	1081
0₁(1117)	→	1118
0₁(316)	→	317
0₁(1427)	→	1428
0₁(68)	→	69
0₁(2412)	→	2413
0₁(2329)	→	2330
0₁(2100)	→	2101
0₁(1211)	→	1212
0₁(1284)	→	1285
0₁(66)	→	67
0₁(1248)	→	1249
0₁(1039)	→	1040
0₁(1297)	→	1298
0₁(629)	→	630
0₁(1038)	→	1039
0₁(1431)	→	1432
0₁(1961)	→	1962
0₁(43)	→	44
0₁(603)	→	604
0₁(908)	→	909
0₁(2102)	→	2103
0₁(388)	→	389
0₁(424)	→	425
0₁(1708)	→	1709
0₁(1723)	→	1724
0₁(93)	→	94
0₁(634)	→	635
0₁(11)	→	12
0₁(1713)	→	1714
0₁(552)	→	553
0₁(749)	→	750
0₁(638)	→	639
0₁(1381)	→	1382
0₁(644)	→	645
0₁(2096)	→	2097
0₁(1495)	→	1496
0₁(99)	→	100
0₁(1872)	→	1873
0₁(759)	→	760
0₁(1299)	→	1300
0₁(1210)	→	1211
0₁(2325)	→	2326
0₁(1668)	→	1669
0₁(914)	→	915
0₁(2323)	→	2324
0₁(830)	→	831
0₁(2241)	→	2242
0₁(1142)	→	1143
0₁(792)	→	793
0₁(793)	→	794
0₁(2410)	→	2411
0₁(614)	→	615
0₁(770)	→	771
0₁(2098)	→	2099
0₁(849)	→	850
0₁(762)	→	763
0₁(996)	→	997
0₁(713)	→	714
0₁(596)	→	597
0₁(706)	→	707
0₁(789)	→	790
0₁(1246)	→	1247
0₁(1429)	→	1430
0₁(551)	→	552
0₁(1978)	→	1979
0₁(1172)	→	1173
0₁(984)	→	985
0₁(1707)	→	1708
0₁(293)	→	294
0₁(1000)	→	1001
0₁(1243)	→	1244
0₁(486)	→	487
0₁(1148)	→	1149
0₁(717)	→	718
0₁(604)	→	605
0₁(415)	→	416
0₁(1295)	→	1296
0₁(1078)	→	1079
3₁(774)	→	775
3₁(1152)	→	1153
3₁(685)	→	686
3₁(220)	→	221
3₁(417)	→	418
3₁(165)	→	166
3₁(1311)	→	1312
3₁(662)	→	663
3₁(1982)	→	1983
3₁(667)	→	668
3₁(1728)	→	1729
3₁(704)	→	705
3₁(1214)	→	1215
3₁(560)	→	561
3₁(1316)	→	1317
3₁(1353)	→	1354
3₁(687)	→	688
3₁(1621)	→	1622
3₁(1878)	→	1879
3₁(708)	→	709
3₁(1319)	→	1320
3₁(616)	→	617
3₁(428)	→	429
3₁(800)	→	801
3₁(778)	→	779
3₁(488)	→	489
3₁(1035)	→	1036
3₁(2148)	→	2149
3₁(1115)	→	1116
3₁(813)	→	814
3₁(822)	→	823
3₁(1173)	→	1174
3₁(1175)	→	1176
3₁(420)	→	421
3₁(2418)	→	2419
3₁(1292)	→	1293
3₁(1154)	→	1155
3₁(1331)	→	1332
3₁(2156)	→	2157
3₁(752)	→	753
3₁(2138)	→	2139
3₁(1003)	→	1004
3₁(743)	→	744
3₁(1373)	→	1374
3₁(564)	→	565
3₁(834)	→	835
3₁(2337)	→	2338
3₁(601)	→	602
3₁(12)	→	13
3₁(718)	→	719
3₁(2339)	→	2340
3₁(1710)	→	1711
3₁(580)	→	581
3₁(753)	→	754
3₁(313)	→	314
3₁(664)	→	665
3₁(319)	→	320
3₁(2166)	→	2167
3₁(2140)	→	2141
3₁(1166)	→	1167
3₁(2168)	→	2169
3₁(1980)	→	1981
3₁(216)	→	217
3₁(1208)	→	1209
3₁(1454)	→	1455
3₁(566)	→	567
3₁(607)	→	608
3₁(427)	→	428
3₁(811)	→	812
3₁(1671)	→	1672
3₁(680)	→	681
3₁(1174)	→	1175
3₁(485)	→	486
3₁(1286)	→	1287
3₁(588)	→	589
3₁(2406)	→	2407
3₁(1558)	→	1559
3₁(1672)	→	1673
3₁(705)	→	706
3₁(1551)	→	1552
3₁(1450)	→	1451
3₁(594)	→	595
3₁(773)	→	774
3₁(2392)	→	2393
3₁(932)	→	933
3₁(851)	→	852
3₁(688)	→	689
3₁(563)	→	564
3₁(1076)	→	1077
3₁(413)	→	414
3₁(658)	→	659
3₁(745)	→	746
3₁(790)	→	791
3₁(997)	→	998
3₁(380)	→	381
3₁(582)	→	583
3₁(168)	→	169
3₁(2106)	→	2107
3₁(1204)	→	1205
3₁(1496)	→	1497
3₁(648)	→	649
3₁(1712)	→	1713
3₁(909)	→	910
3₁(631)	→	632
3₁(314)	→	315
3₁(590)	→	591
3₁(993)	→	994
3₁(562)	→	563
3₁(2304)	→	2305
3₁(2160)	→	2161
3₁(797)	→	798
3₁(554)	→	555
3₁(672)	→	673
3₁(2247)	→	2248
3₁(2310)	→	2311
3₁(586)	→	587
3₁(1036)	→	1037
3₁(626)	→	627
3₁(288)	→	289
3₁(873)	→	874
3₁(1177)	→	1178
3₁(1435)	→	1436
3₁(744)	→	745
3₁(1008)	→	1009
3₁(1249)	→	1250
3₁(553)	→	554
3₁(853)	→	854
3₁(2394)	→	2395
3₁(2302)	→	2303
3₁(1554)	→	1555
3₁(421)	→	422
3₁(555)	→	556
3₁(833)	→	834
3₁(584)	→	585
3₁(782)	→	783
3₁(2408)	→	2409
3₁(1245)	→	1246
3₁(630)	→	631
3₁(1466)	→	1467
3₁(1250)	→	1251
3₁(1290)	→	1291
3₁(9)	→	10
3₁(595)	→	596
3₁(1144)	→	1145
1₂(2215)	→	2216
1₂(2345)	→	2346
1₂(1857)	→	1858
1₂(2217)	→	2218
1₂(978)	→	979
1₂(2286)	→	2287
1₂(2213)	→	2214
1₂(2206)	→	2207
1₂(2039)	→	2040
1₂(901)	→	902
1₂(2219)	→	2220
1₂(1969)	→	1970
1₂(883)	→	884
1₂(1959)	→	1960
1₂(902)	→	903
1₂(1990)	→	1991
1₂(882)	→	883
1₂(2221)	→	2222
1₂(1864)	→	1865
1₂(2285)	→	2286
1₂(2279)	→	2280
1₂(2282)	→	2283
1₂(1863)	→	1864
1₂(1886)	→	1887
1₂(1988)	→	1989
1₂(2033)	→	2034
1₂(2190)	→	2191
1₂(1913)	→	1914
1₂(2283)	→	2284
1₂(1958)	→	1959
1₂(977)	→	978
1₂(2201)	→	2202
1₂(1906)	→	1907
1₂(1911)	→	1912
1₂(2199)	→	2200
5₀(1)	→	1
5₀(6)	→	1
5₀(5)	→	1
5₀(2)	→	1
5₀(3)	→	1
5₀(4)	→	1
2₂(1887)	→	1888
2₂(2278)	→	2279
2₂(1862)	→	1863
2₂(1953)	→	1954
2₂(979)	→	980
2₂(903)	→	904
2₂(1838)	→	1839
2₂(1836)	→	1837
2₂(1957)	→	1958
2₂(1860)	→	1861
2₂(1844)	→	1845
2₂(2342)	→	2343
2₂(1910)	→	1911
2₂(2205)	→	2206
2₂(884)	→	885
2₂(1972)	→	1973
2₂(2194)	→	2195
2₂(1905)	→	1906
2₂(1955)	→	1956
2₂(1842)	→	1843
2₂(2347)	→	2348
2₂(1889)	→	1890
2₂(2404)	→	2405
2₂(1882)	→	1883
2₂(1991)	→	1992
2₂(1856)	→	1857
2₂(980)	→	981
2₂(1908)	→	1909
2₂(904)	→	905
2₂(885)	→	886
2₂(2281)	→	2282
2₂(973)	→	974

The automaton is closed under rewriting as it is compatible.