Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4934)

The rewrite relation of the following TRS is considered.

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

2493	→	96
1906	→	1887
2521	→	725
1793	→	2564
279	→	236
279	→	465
279	→	1039
279	→	481
279	→	759
279	→	2
279	→	281
2312	→	774
366	→	300
366	→	604
366	→	784
376	→	1124
376	→	1159
376	→	1661
2501	→	97
899	→	2570
733	→	4
733	→	813
733	→	626
733	→	166
733	→	195
733	→	507
733	→	598
733	→	1585
733	→	1653
733	→	1289
733	→	244
733	→	2270
534	→	1
534	→	902
534	→	815
534	→	9
534	→	42
534	→	68
2166	→	96
2253	→	244
2150	→	636
2138	→	595
1437	→	97
1703	→	2165
685	→	707
685	→	1337
835	→	439
835	→	1855
1751	→	774
2338	→	614
745	→	2568
1057	→	738
1057	→	582
1057	→	724
1057	→	525
1057	→	3
1057	→	96
1057	→	576
1057	→	127
1057	→	1887
1057	→	1906
1737	→	774
2367	→	1887
1875	→	1860
1056	→	1924
1056	→	1962
1056	→	2291
2152	→	636
967	→	96
860	→	1368
860	→	1734
2205	→	1179
2205	→	510
2322	→	774
732	→	1030
732	→	1116
732	→	1659
1117	→	1752
1697	→	2163
533	→	1128
533	→	1163
533	→	1665
715	→	3
715	→	738
715	→	582
715	→	567
715	→	96
715	→	147
715	→	724
715	→	525
715	→	576
715	→	127
715	→	1887
715	→	1902
715	→	1906
715	→	2369
1648	→	1625
1648	→	1780
98	→	656
2349	→	876
1288	→	567
809	→	1699
10	→	1857
2297	→	2498
2100	→	567
1313	→	1469
742	→	1588
2247	→	725
2062	→	455
2062	→	2153
97	→	740
97	→	429
97	→	297
97	→	124
97	→	41
97	→	192
97	→	324
97	→	3
97	→	1887
97	→	1888
2173	→	2532
1638	→	1625
1638	→	1766
2142	→	595
1546	→	867
1733	→	773
851	→	1291
851	→	1624
851	→	2131
1284	→	567
1794	→	2305
781	→	308
96	→	539
96	→	582
96	→	616
96	→	738
2185	→	2534
1704	→	244
1280	→	567
1782	→	1932
2211	→	2196
326	→	1897
2239	→	725
1784	→	1948
882	→	565
701	→	685
655	→	3
655	→	97
655	→	539
655	→	616
655	→	125
655	→	1887
655	→	1888
2146	→	595
2457	→	525
2457	→	2500
2457	→	2520
2056	→	455
2056	→	2151
811	→	2103
811	→	2143
811	→	2258
2590	→	96
706	→	306
391	→	2077
1097	→	1089
2070	→	455
2070	→	2155
1625	→	1784
1923	→	96
2132	→	2121
145	→	96
145	→	537
145	→	578
145	→	736
1160	→	1149
1160	→	1370
466	→	456
1670	→	235
299	→	1907
1408	→	1396
1158	→	813
1158	→	626
1158	→	166
1158	→	393
1158	→	263
1158	→	144
1158	→	8
1158	→	165
1158	→	299
1158	→	4
1158	→	195
1158	→	2249
1158	→	1653
1158	→	1289
1158	→	244
1158	→	2270
2369	→	1887
2483	→	96
625	→	2
625	→	543
625	→	481
625	→	759
625	→	236
625	→	281
625	→	1455
1589	→	626
2054	→	431
2054	→	2335
18	→	1
18	→	815
18	→	902
18	→	44
18	→	1396
18	→	1408
18	→	2278
624	→	1126
624	→	1161
624	→	1663
624	→	2212
2534	→	2558
2402	→	174
365	→	1905
2249	→	165
643	→	244
643	→	1175
3	→	41
3	→	124
3	→	192
3	→	297
3	→	324
3	→	429
583	→	568
583	→	836
583	→	2369
1506	→	243
955	→	1730
2170	→	96
2278	→	815
812	→	802
812	→	543
812	→	455
812	→	2
812	→	236
812	→	264
772	→	642
691	→	375
2156	→	636
2389	→	174
2389	→	2528
2080	→	525
2080	→	2185
2080	→	2240
2154	→	636
213	→	166
2583	→	2589
617	→	1454
1324	→	1314
1294	→	595
1258	→	1250
1858	→	905
646	→	979
861	→	565
298	→	236
298	→	483
298	→	1041
298	→	1395
298	→	2248
411	→	368
411	→	696
1467	→	2093
1467	→	2141
1467	→	2252
2140	→	595
9	→	815
9	→	844
9	→	902
1706	→	244
1714	→	1911
1714	→	2287
2535	→	244
1931	→	980
620	→	2230
647	→	766
5	→	67
5	→	95
5	→	212
5	→	280
5	→	343
5	→	410
147	→	96
147	→	567
2041	→	431
2041	→	2311
2030	→	2366
515	→	4
515	→	813
515	→	626
515	→	166
515	→	893
515	→	526
515	→	854
515	→	540
515	→	193
1999	→	166
1055	→	2293
456	→	1538
1664	→	815
1183	→	2101
1183	→	2139
1183	→	2256
618	→	2187
765	→	602
2491	→	96
175	→	3
175	→	740
175	→	738
175	→	582
175	→	96
175	→	125
175	→	97
175	→	1887
175	→	1888
1220	→	2032
1220	→	2055
1220	→	2271
1646	→	1625
1646	→	1774
325	→	300
325	→	782
2172	→	97
2308	→	244
1095	→	738
1095	→	582
1095	→	724
1095	→	525
1095	→	3
1095	→	96
1095	→	576
1095	→	127
1095	→	1887
1095	→	1906
1095	→	2369
1344	→	543
1344	→	236
1344	→	391
1344	→	278
1344	→	163
1344	→	43
1344	→	194
1344	→	326
1344	→	2
1344	→	262
1662	→	815
193	→	166
193	→	931
1965	→	1887
1031	→	1149
1031	→	1374
1900	→	1887
2072	→	525
2072	→	2171
2072	→	2238
1668	→	235
1164	→	1149
1164	→	1372
1898	→	1887
2301	→	2474
2280	→	815
1162	→	1149
1162	→	1387
1416	→	1396
1493	→	718
1	→	93
1	→	126
1	→	233
1	→	261
1	→	365
1	→	367
1308	→	595
1902	→	1887
2295	→	2492
1040	→	1032
654	→	1004
654	→	1068
654	→	1309
654	→	1870
739	→	725
695	→	685
127	→	96
127	→	525
127	→	576
127	→	724
901	→	6
901	→	786
901	→	431
901	→	300
901	→	583
901	→	577
901	→	782
901	→	325
1267	→	2546
965	→	96
1338	→	1709
1318	→	543
1318	→	481
1318	→	759
1318	→	2
1318	→	236
1318	→	281
1318	→	1455
1753	→	774
1317	→	2053
1317	→	2069
1317	→	2210
1317	→	2283
392	→	368
392	→	694
392	→	845
392	→	410
392	→	280
392	→	95
392	→	67
392	→	212
392	→	343
392	→	5
392	→	2194
1713	→	2116
1713	→	2135
1713	→	2250
2293	→	2490
2024	→	2354
505	→	456
505	→	1490
747	→	954
747	→	1669
747	→	1899
2117	→	567
1986	→	740
1986	→	429
1986	→	297
1986	→	124
1986	→	41
1986	→	192
1986	→	324
1986	→	3
1986	→	97
1986	→	1888
2529	→	455
44	→	9
723	→	463
2288	→	235
761	→	823
748	→	6
748	→	786
748	→	431
748	→	300
748	→	773
748	→	344
748	→	836
748	→	568
748	→	583
748	→	782
748	→	325
1700	→	244
634	→	1705
842	→	1211
1988	→	1977
2039	→	431
2039	→	2323
2310	→	773
536	→	526
735	→	725
1772	→	1940
125	→	96
343	→	1903
2304	→	244
1414	→	1396
309	→	3
309	→	738
309	→	582
309	→	724
309	→	525
309	→	96
309	→	576
309	→	127
309	→	740
309	→	125
309	→	97
309	→	1179
309	→	1887
309	→	1906
309	→	1888
309	→	2369
1005	→	1549
1654	→	1625
1654	→	1782
1654	→	2454
1373	→	636
1157	→	2071
783	→	774
783	→	1409
783	→	1492
1971	→	1887
2533	→	244
868	→	533
2563	→	2196
1402	→	97
1402	→	539
1402	→	616
1402	→	125
1402	→	41
1402	→	192
1402	→	324
1402	→	429
1402	→	297
1402	→	124
1402	→	3
1402	→	1887
1402	→	1888
2305	→	2482
1896	→	1416
1896	→	1414
1896	→	1410
1896	→	1408
1766	→	1946
1499	→	718
1127	→	1117
1410	→	1396
2565	→	2196
552	→	1
552	→	902
552	→	815
552	→	9
552	→	42
540	→	526
540	→	854
540	→	893
1453	→	702
2174	→	97
346	→	300
346	→	595
2136	→	2121
1699	→	2159
2092	→	525
2573	→	2196
1311	→	1446
810	→	3
810	→	740
810	→	738
810	→	582
810	→	96
810	→	125
810	→	97
648	→	876
1984	→	2401
6	→	69
6	→	146
6	→	214
6	→	235
6	→	345
6	→	412
302	→	553
2569	→	2196
2064	→	455
2064	→	2149
2499	→	96
1235	→	1212
1235	→	1456
1256	→	902
1256	→	815
1256	→	1
1256	→	9
1256	→	42
1539	→	761
627	→	1578
921	→	815
921	→	902
921	→	44
921	→	1396
921	→	1408
921	→	2278
577	→	568
1042	→	1032
345	→	1901
2106	→	567
2213	→	2196
377	→	3
377	→	738
377	→	582
377	→	724
377	→	525
377	→	96
377	→	576
377	→	127
377	→	1887
377	→	1906
377	→	2369
1438	→	2301
1302	→	595
1302	→	2348
1186	→	1178
308	→	966
308	→	1691
308	→	1964
2031	→	300
1701	→	2161
105	→	1
105	→	815
105	→	902
105	→	44
105	→	42
105	→	2278
394	→	368
394	→	684
1292	→	567
484	→	456
2171	→	2530
237	→	636
1585	→	165
174	→	1232
2158	→	236
615	→	596
615	→	869
615	→	1257
699	→	685
565	→	962
565	→	1683
565	→	1974
368	→	700
368	→	758
900	→	1703
2500	→	2583
264	→	236
264	→	455
264	→	1037
264	→	1586
538	→	526
2033	→	431
2033	→	2321
2022	→	2368
1684	→	235
853	→	4
853	→	215
853	→	432
301	→	716
2025	→	300
1014	→	740
1014	→	738
1014	→	582
1014	→	96
1014	→	429
1014	→	297
1014	→	124
1014	→	41
1014	→	192
1014	→	324
1014	→	3
1014	→	125
1014	→	97
1014	→	1887
1014	→	1888
1036	→	633
808	→	1047
808	→	1458
2	→	43
2	→	163
2	→	194
2	→	278
2	→	326
2	→	391
814	→	802
787	→	774
787	→	1415
787	→	1498
787	→	1707
2144	→	595
4	→	8
4	→	144
4	→	165
4	→	263
4	→	299
4	→	393
344	→	300
344	→	773
463	→	1224
2584	→	244
1069	→	1048
1069	→	1758
244	→	1289
244	→	1301
244	→	1653
827	→	713
843	→	732
1761	→	869
1666	→	815
2571	→	2196
1451	→	684
300	→	431
300	→	614
300	→	786
369	→	1088
1550	→	766
440	→	5
440	→	758
440	→	845
440	→	700
440	→	368
440	→	1454
440	→	617
440	→	2194
281	→	236
281	→	481
508	→	559
1587	→	165
1390	→	236
16	→	2566
602	→	911
602	→	1540
1059	→	1048
1059	→	1760
1470	→	710
1715	→	215
1715	→	393
1715	→	263
1715	→	144
1715	→	8
1715	→	165
1715	→	299
1715	→	4
1715	→	432
2477	→	96
1773	→	647
1094	→	2040
1094	→	2063
1094	→	2279
1343	→	2307
93	→	1874
93	→	1976
93	→	2000
93	→	2022
93	→	2193
2475	→	96
2531	→	244
1491	→	719
1692	→	235
1125	→	1117
1125	→	1736
2255	→	244
1270	→	815
1270	→	902
1270	→	1
1270	→	68
2023	→	300
1925	→	96
1369	→	236
1698	→	244
581	→	568
1705	→	2167
1221	→	902
1221	→	815
1221	→	1
1221	→	9
1221	→	42
1871	→	1860
1963	→	1887
1436	→	2297
1856	→	903
1869	→	1396
1869	→	1408
989	→	649
759	→	828
104	→	1015
104	→	1058
104	→	1450
104	→	1872
104	→	1987
834	→	2030
834	→	2232
514	→	1287
514	→	1293
514	→	1647
2241	→	725
1455	→	703
1455	→	2299
1497	→	718
236	→	504
236	→	543
697	→	685
746	→	1697
1013	→	2079
1939	→	980
1044	→	1032
2148	→	617
1632	→	654
2162	→	96
1401	→	1859
1401	→	1998
1401	→	2024
1401	→	2147
2094	→	567
2233	→	617
1873	→	1860
2567	→	2196
1184	→	813
1184	→	626
1184	→	166
1184	→	893
1184	→	526
1184	→	393
1184	→	263
1184	→	144
1184	→	8
1184	→	165
1184	→	299
1184	→	4
1184	→	854
1184	→	540
1184	→	193
1255	→	2099
1255	→	2137
1255	→	2254
991	→	96
635	→	2
635	→	543
635	→	236
635	→	262
563	→	2337
234	→	166
234	→	811
234	→	922
934	→	10
1686	→	235
1038	→	1032
1780	→	1938
42	→	9
1581	→	2157
1581	→	2309
2257	→	244
579	→	568
2251	→	244
1735	→	773
1795	→	786
1795	→	431
1795	→	300
1795	→	583
1795	→	412
1795	→	235
1795	→	146
1795	→	69
1795	→	214
1795	→	345
1795	→	6
1795	→	577
1795	→	782
1795	→	325
1510	→	1501
709	→	1323
1910	→	96
2186	→	97
278	→	2105
278	→	2145
278	→	2269
2270	→	244
1447	→	686
566	→	1
566	→	815
566	→	902
566	→	68
566	→	44
566	→	1396
566	→	1089
566	→	1097
566	→	2278
909	→	1279
909	→	1637
909	→	2120
1975	→	1887
2194	→	617
2290	→	235
1774	→	1930
245	→	2
245	→	543
245	→	481
245	→	759
245	→	236
245	→	281
245	→	262
245	→	802
245	→	455
245	→	264
245	→	814
245	→	1455
17	→	1701
2231	→	710
2160	→	96
1286	→	567
714	→	1283
714	→	1299
714	→	1639
1583	→	740
1583	→	738
1583	→	582
1583	→	96
1583	→	429
1583	→	297
1583	→	124
1583	→	41
1583	→	192
1583	→	324
1583	→	3
1583	→	125
1583	→	97
1583	→	1887
1583	→	1888
164	→	96
164	→	535
164	→	580
164	→	734
1439	→	97
2168	→	96
168	→	702
1129	→	1117
1129	→	1750
1260	→	554
68	→	9
1933	→	980
1508	→	1501
2298	→	244
768	→	1250
464	→	4
464	→	813
464	→	626
464	→	166
464	→	195
464	→	2249
464	→	1653
464	→	1289
464	→	244
464	→	2270
2324	→	774
413	→	368
413	→	698
324	→	1886
2302	→	244
215	→	166
215	→	801
1696	→	244
2286	→	235
693	→	685
928	→	2562
1457	→	702
2078	→	525
2078	→	2173
2078	→	2246
2307	→	2484
2130	→	759
1695	→	2169
1904	→	1887
722	→	2195
1093	→	2091
2292	→	235
482	→	456
1227	→	1212
1227	→	1438
1227	→	1509
629	→	1796
1708	→	838
1445	→	97
1290	→	567
2188	→	686
2355	→	1887
953	→	815
953	→	902
953	→	44
953	→	1396
953	→	1408
953	→	2278
1660	→	815
775	→	862
932	→	11
1225	→	1212
1225	→	1436
1225	→	1452
1225	→	1500
375	→	1234
2272	→	815
1444	→	2295
2306	→	244
574	→	943
574	→	990
574	→	1667
2303	→	2476
2102	→	567
575	→	244
1985	→	2388
1985	→	2456
195	→	166
195	→	393
195	→	263
195	→	144
195	→	8
195	→	165
195	→	299
195	→	4
2294	→	244
1947	→	980
2530	→	2554
2559	→	96
852	→	964
852	→	1685
1233	→	1212
1233	→	1444
1233	→	1507
1775	→	647
1016	→	1005
1016	→	1547
1375	→	636
910	→	747
2561	→	96
558	→	532
1908	→	1887
1050	→	1259
1759	→	869
1783	→	647
1388	→	636
1785	→	647
1269	→	1909
1269	→	1972
1269	→	2285
660	→	2572
2296	→	244
961	→	564
507	→	1185
507	→	1263
1781	→	647
785	→	774
785	→	1413
785	→	1496
822	→	780
194	→	2038
194	→	2061
194	→	2277
1912	→	96
2104	→	567
603	→	244
603	→	933
605	→	596
551	→	1285
551	→	1307
551	→	1645
1973	→	1887
70	→	9
875	→	103
930	→	815
930	→	902
930	→	1
930	→	44
1797	→	1791
1371	→	636
929	→	2303
2547	→	614
166	→	506
166	→	626
166	→	646
166	→	813
1702	→	244
737	→	725
439	→	1226
439	→	1786
1468	→	738
1468	→	582
1468	→	567
1468	→	3
1468	→	96
1468	→	147
1468	→	1887
1468	→	1902
2284	→	815
2485	→	96
2300	→	829
1123	→	633
1949	→	980
2164	→	96
2336	→	774
262	→	236
262	→	1043
262	→	1407
262	→	1584
2259	→	244
2455	→	508
94	→	9
94	→	93
94	→	233
94	→	365
94	→	367
94	→	261
94	→	126
94	→	1
94	→	44
94	→	2278
1300	→	595
780	→	1389
780	→	1732
430	→	368
430	→	692
430	→	1096
1640	→	1625
1640	→	1772
661	→	307
327	→	300
1941	→	980
2001	→	166
1548	→	1542
1731	→	854
2555	→	96
2532	→	2560
963	→	96
1767	→	647
307	→	1695
1582	→	1922
1582	→	1970
1582	→	2289
3₁(1122)	→	1123
3₁(507)	→	508
3₁(1220)	→	1221
3₁(1792)	→	1793
3₁(1998)	→	1999
3₁(1094)	→	1095
3₁(1645)	→	1646
3₁(539)	→	540
3₁(1212)	→	1213
3₁(1624)	→	1625
3₁(638)	→	639
3₁(657)	→	658
3₁(817)	→	818
3₁(1215)	→	1216
3₁(624)	→	625
3₁(732)	→	733
3₁(741)	→	742
3₁(928)	→	929
3₁(2258)	→	2259
3₁(2252)	→	2253
3₁(1540)	→	1541
3₁(1316)	→	1317
3₁(639)	→	640
3₁(1176)	→	1177
3₁(820)	→	821
3₁(689)	→	690
3₁(532)	→	533
3₁(528)	→	529
3₁(192)	→	193
3₁(597)	→	598
3₁(761)	→	762
3₁(568)	→	569
3₁(656)	→	657
3₁(537)	→	538
3₁(2269)	→	2270
3₁(9)	→	10
3₁(848)	→	849
3₁(238)	→	239
3₁(1710)	→	1711
3₁(1312)	→	1313
3₁(623)	→	624
3₁(1117)	→	1118
3₁(2000)	→	2001
3₁(506)	→	507
3₁(745)	→	746
3₁(1317)	→	1318
3₁(1461)	→	1462
3₁(533)	→	534
3₁(933)	→	934
3₁(214)	→	215
3₁(1584)	→	1585
3₁(303)	→	304
3₁(771)	→	772
3₁(1639)	→	1640
3₁(1544)	→	1545
3₁(1628)	→	1629
3₁(642)	→	643
3₁(1637)	→	1638
3₁(1219)	→	1220
3₁(708)	→	709
3₁(212)	→	213
3₁(376)	→	377
3₁(856)	→	857
3₁(596)	→	597
3₁(1010)	→	1011
3₁(1786)	→	1787
3₁(1711)	→	1712
3₁(16)	→	17
3₁(839)	→	840
3₁(637)	→	638
3₁(780)	→	781
3₁(743)	→	744
3₁(233)	→	234
3₁(525)	→	526
3₁(860)	→	861
3₁(690)	→	691
3₁(1259)	→	1260
3₁(705)	→	706
3₁(2254)	→	2255
3₁(729)	→	730
3₁(431)	→	432
3₁(1793)	→	1794
3₁(1588)	→	1589
3₁(849)	→	850
3₁(775)	→	776
3₁(774)	→	775
3₁(1051)	→	1052
3₁(1446)	→	1447
3₁(768)	→	769
3₁(903)	→	904
3₁(1004)	→	1005
3₁(165)	→	166
3₁(1581)	→	1582
3₁(1730)	→	1731
3₁(704)	→	705
3₁(1175)	→	1176
3₁(2250)	→	2251
3₁(660)	→	661
3₁(1505)	→	1506
3₁(2454)	→	2455
3₁(2256)	→	2257
3₁(1653)	→	1654
3₁(171)	→	172
3₁(2248)	→	2249
3₁(436)	→	437
3₁(719)	→	720
3₁(864)	→	865
3₁(194)	→	195
3₁(1647)	→	1648
3₁(553)	→	554
3₁(1586)	→	1587
3₁(619)	→	620
3₁(722)	→	723
3₁(1032)	→	1033
3₁(2187)	→	2188
3₁(899)	→	900
3₁(685)	→	686
3₁(804)	→	805
3₁(535)	→	536
3₁(898)	→	899
3₁(1015)	→	1016
3₁(838)	→	839
3₂(912)	→	913
3₂(1987)	→	1988
3₂(2568)	→	2569
3₂(2572)	→	2573
3₂(2564)	→	2565
3₂(1860)	→	1861
3₂(2570)	→	2571
3₂(2212)	→	2213
3₂(1976)	→	1977
3₂(2562)	→	2563
3₂(2566)	→	2567
3₂(2200)	→	2201
3₂(1867)	→	1868
3₂(2210)	→	2211
3₂(2195)	→	2196
3₂(919)	→	920
3₂(2201)	→	2202
3₂(2122)	→	2123
3₂(1982)	→	1983
4₂(916)	→	917
4₂(911)	→	912
4₂(1895)	→	1896
4₂(952)	→	953
4₂(1859)	→	1860
4₂(1874)	→	1875
4₂(1872)	→	1873
4₂(1889)	→	1890
4₂(1870)	→	1871
4₂(982)	→	983
4₂(1864)	→	1865
4₂(988)	→	989
4₂(1981)	→	1982
4₂(946)	→	947
4₂(1861)	→	1862
4₂(913)	→	914
4₂(1980)	→	1981
5₂(951)	→	952
5₂(981)	→	982
5₂(915)	→	916
5₂(2204)	→	2205
5₂(1888)	→	1889
5₂(986)	→	987
5₂(1894)	→	1895
5₂(1893)	→	1894
5₂(1863)	→	1864
5₂(945)	→	946
5₂(987)	→	988
5₂(950)	→	951
5₂(2128)	→	2129
5₂(2121)	→	2122
2₁(1760)	→	1761
2₁(616)	→	617
2₁(429)	→	430
2₁(1089)	→	1090
2₁(923)	→	924
2₁(371)	→	372
2₁(1695)	→	1696
2₁(959)	→	960
2₁(463)	→	464
2₁(926)	→	927
2₁(1691)	→	1692
2₁(2401)	→	2402
2₁(1465)	→	1466
2₁(876)	→	877
2₁(569)	→	570
2₁(559)	→	560
2₁(410)	→	411
2₁(101)	→	102
2₁(842)	→	843
2₁(167)	→	168
2₁(650)	→	651
2₁(1031)	→	1032
2₁(1039)	→	1040
2₁(1705)	→	1706
2₁(2147)	→	2148
2₁(412)	→	413
2₁(1397)	→	1398
2₁(1458)	→	1459
2₁(2532)	→	2533
2₁(1667)	→	1668
2₁(2388)	→	2389
2₁(766)	→	767
2₁(391)	→	392
2₁(819)	→	820
2₁(439)	→	440
2₁(960)	→	961
2₁(841)	→	842
2₁(831)	→	832
2₁(1791)	→	1792
2₁(633)	→	634
2₁(174)	→	175
2₁(11)	→	12
2₁(1398)	→	1399
2₁(712)	→	713
2₁(776)	→	777
2₁(2287)	→	2288
2₁(844)	→	845
2₁(858)	→	859
2₁(14)	→	15
2₁(375)	→	376
2₁(368)	→	369
2₁(1542)	→	1543
2₁(1456)	→	1457
2₁(2289)	→	2290
2₁(805)	→	806
2₁(1450)	→	1451
2₁(2297)	→	2298
2₁(604)	→	605
2₁(1703)	→	1704
2₁(2295)	→	2296
2₁(1685)	→	1686
2₁(2285)	→	2286
2₁(1155)	→	1156
2₁(1041)	→	1042
2₁(168)	→	169
2₁(1342)	→	1343
2₁(881)	→	882
2₁(1669)	→	1670
2₁(599)	→	600
2₁(1007)	→	1008
2₁(2291)	→	2292
2₁(1006)	→	1007
2₁(2534)	→	2535
2₁(600)	→	601
2₁(1037)	→	1038
2₁(1339)	→	1340
2₁(393)	→	394
2₁(367)	→	368
2₁(1683)	→	1684
2₁(630)	→	631
2₁(2232)	→	2233
2₁(1697)	→	1698
2₁(1787)	→	1788
2₁(703)	→	704
2₁(1013)	→	1014
2₁(1578)	→	1579
2₁(437)	→	438
2₁(237)	→	238
2₁(2530)	→	2531
2₁(893)	→	894
2₁(242)	→	243
2₁(614)	→	615
2₁(2293)	→	2294
2₁(1399)	→	1400
2₁(1012)	→	1013
2₁(777)	→	778
2₁(2307)	→	2308
2₁(897)	→	898
2₁(958)	→	959
2₁(1501)	→	1502
2₁(1701)	→	1702
2₁(173)	→	174
2₁(1179)	→	1180
2₁(531)	→	532
2₁(1309)	→	1310
2₁(1629)	→	1630
2₁(857)	→	858
2₁(1043)	→	1044
2₁(461)	→	462
2₁(1157)	→	1158
2₁(1263)	→	1264
2₁(512)	→	513
2₁(1452)	→	1453
2₁(595)	→	596
2₁(878)	→	879
2₁(2305)	→	2306
2₁(1093)	→	1094
2₁(99)	→	100
2₁(510)	→	511
2₁(824)	→	825
2₁(2303)	→	2304
2₁(369)	→	370
2₁(626)	→	627
2₁(1758)	→	1759
2₁(725)	→	726
2₁(1699)	→	1700
2₁(2301)	→	2302
2₁(572)	→	573
2₁(2193)	→	2194
2₁(1181)	→	1182
2₁(651)	→	652
2₁(652)	→	653
2₁(1218)	→	1219
2₁(544)	→	545
2₁(830)	→	831
2₁(100)	→	101
2₁(2583)	→	2584
2₀(3)	→	5
2₀(6)	→	5
2₀(5)	→	5
2₀(4)	→	5
2₀(2)	→	5
2₀(1)	→	5
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
0₂(2124)	→	2125
0₂(2202)	→	2203
0₂(2198)	→	2199
0₂(2129)	→	2130
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
5₁(1216)	→	1217
5₁(299)	→	300
5₁(807)	→	808
5₁(555)	→	556
5₁(825)	→	826
5₁(529)	→	530
5₁(1784)	→	1785
5₁(1058)	→	1059
5₁(1464)	→	1465
5₁(2022)	→	2023
5₁(97)	→	98
5₁(2040)	→	2041
5₁(1153)	→	1154
5₁(582)	→	583
5₁(1549)	→	1550
5₁(1503)	→	1504
5₁(906)	→	907
5₁(1766)	→	1767
5₁(2309)	→	2310
5₁(1128)	→	1129
5₁(554)	→	555
5₁(826)	→	827
5₁(833)	→	834
5₁(1299)	→	1300
5₁(574)	→	575
5₁(763)	→	764
5₁(1630)	→	1631
5₁(1772)	→	1773
5₁(578)	→	579
5₁(1268)	→	1269
5₁(564)	→	565
5₁(770)	→	771
5₁(649)	→	650
5₁(867)	→	868
5₁(711)	→	712
5₁(365)	→	366
5₁(458)	→	459
5₁(343)	→	344
5₁(543)	→	544
5₁(1269)	→	1270
5₁(1116)	→	1117
5₁(576)	→	577
5₁(709)	→	710
5₁(823)	→	824
5₁(2143)	→	2144
5₁(815)	→	816
5₁(1396)	→	1397
5₁(2032)	→	2033
5₁(862)	→	863
5₁(1120)	→	1121
5₁(1056)	→	1057
5₁(688)	→	689
5₁(1047)	→	1048
5₁(1048)	→	1049
5₁(1121)	→	1122
5₁(601)	→	602
5₁(1266)	→	1267
5₁(2030)	→	2031
5₁(1714)	→	1715
5₁(956)	→	957
5₁(779)	→	780
5₁(103)	→	104
5₁(1502)	→	1503
5₁(1541)	→	1542
5₁(806)	→	807
5₁(102)	→	103
5₁(2137)	→	2138
5₁(580)	→	581
5₁(308)	→	309
5₁(646)	→	647
5₁(2546)	→	2547
5₁(869)	→	870
5₁(1579)	→	1580
5₁(877)	→	878
5₁(1780)	→	1781
5₁(2024)	→	2025
5₁(2337)	→	2338
5₁(1462)	→	1463
5₁(345)	→	346
5₁(2038)	→	2039
5₁(2139)	→	2140
5₁(832)	→	833
5₁(640)	→	641
5₁(2145)	→	2146
5₁(1782)	→	1783
5₁(726)	→	727
5₁(2230)	→	2231
5₁(747)	→	748
5₁(2053)	→	2054
5₁(326)	→	327
5₁(300)	→	301
5₁(727)	→	728
5₁(1293)	→	1294
5₁(778)	→	779
5₁(924)	→	925
5₁(1301)	→	1302
5₁(1068)	→	1069
5₁(1734)	→	1735
5₁(12)	→	13
5₁(434)	→	435
5₁(1631)	→	1632
5₁(435)	→	436
5₁(1124)	→	1125
5₁(1469)	→	1470
5₁(1152)	→	1153
5₁(852)	→	853
5₁(1580)	→	1581
5₁(2141)	→	2142
5₁(1307)	→	1308
5₁(1732)	→	1733
5₁(1774)	→	1775
5₁(459)	→	460
5₁(720)	→	721
5₁(1150)	→	1151
5₁(1126)	→	1127
5₁(1582)	→	1583
5₁(324)	→	325
5₁(567)	→	568
5₁(1547)	→	1548
5₁(456)	→	457
5₁(562)	→	563
5₁(565)	→	566
0₁(1033)	→	1034
0₁(235)	→	236
0₁(1466)	→	1467
0₁(1509)	→	1510
0₁(742)	→	743
0₁(2240)	→	2241
0₁(2323)	→	2324
0₁(1050)	→	1051
0₁(263)	→	264
0₁(302)	→	303
0₁(2299)	→	2300
0₁(908)	→	909
0₁(236)	→	237
0₁(261)	→	262
0₁(1183)	→	1184
0₁(828)	→	829
0₁(758)	→	759
0₁(527)	→	528
0₁(2063)	→	2064
0₁(782)	→	783
0₁(836)	→	837
0₁(1736)	→	1737
0₁(851)	→	852
0₁(460)	→	461
0₁(1454)	→	1455
0₁(1252)	→	1253
0₁(297)	→	298
0₁(1504)	→	1505
0₁(2069)	→	2070
0₁(462)	→	463
0₁(863)	→	864
0₁(872)	→	873
0₁(1314)	→	1315
0₁(728)	→	729
0₁(278)	→	279
0₁(1372)	→	1373
0₁(550)	→	551
0₁(621)	→	622
0₁(526)	→	527
0₁(1340)	→	1341
0₁(1709)	→	1710
0₁(2321)	→	2322
0₁(762)	→	763
0₁(1752)	→	1753
0₁(1389)	→	1390
0₁(2157)	→	2158
0₁(1091)	→	1092
0₁(716)	→	717
0₁(2151)	→	2152
0₁(736)	→	737
0₁(786)	→	787
0₁(686)	→	687
0₁(2153)	→	2154
0₁(879)	→	880
0₁(811)	→	812
0₁(2335)	→	2336
0₁(818)	→	819
0₁(740)	→	741
0₁(2055)	→	2056
0₁(570)	→	571
0₁(280)	→	281
0₁(1159)	→	1160
0₁(636)	→	637
0₁(1213)	→	1214
0₁(731)	→	732
0₁(547)	→	548
0₁(907)	→	908
0₁(734)	→	735
0₁(306)	→	307
0₁(1254)	→	1255
0₁(724)	→	725
0₁(1054)	→	1055
0₁(241)	→	242
0₁(847)	→	848
0₁(373)	→	374
0₁(1467)	→	1468
0₁(1538)	→	1539
0₁(239)	→	240
0₁(2246)	→	2247
0₁(1156)	→	1157
0₁(1163)	→	1164
0₁(713)	→	714
0₁(2348)	→	2349
0₁(1035)	→	1036
0₁(1370)	→	1371
0₁(2311)	→	2312
0₁(1255)	→	1256
0₁(631)	→	632
0₁(1625)	→	1626
0₁(855)	→	856
0₁(784)	→	785
0₁(905)	→	906
0₁(530)	→	531
0₁(1387)	→	1388
0₁(2528)	→	2529
0₁(514)	→	515
0₁(721)	→	722
0₁(1507)	→	1508
0₁(304)	→	305
0₁(1750)	→	1751
0₁(1161)	→	1162
0₁(909)	→	910
0₁(2155)	→	2156
0₁(2238)	→	2239
0₁(658)	→	659
0₁(2061)	→	2062
0₁(1707)	→	1708
0₁(1500)	→	1501
0₁(1214)	→	1215
0₁(738)	→	739
0₁(801)	→	802
0₁(1374)	→	1375
0₁(1250)	→	1251
0₁(546)	→	547
0₁(1052)	→	1053
0₁(244)	→	245
0₁(813)	→	814
0₁(647)	→	648
0₁(1251)	→	1252
0₁(1030)	→	1031
0₁(2520)	→	2521
0₁(1713)	→	1714
0₁(714)	→	715
0₁(760)	→	761
0₁(1217)	→	1218
0₁(1154)	→	1155
0₁(551)	→	552
0₁(866)	→	867
0₁(1368)	→	1369
0₁(702)	→	703
0₁(641)	→	642
0₁(773)	→	774
0₁(548)	→	549
0₁(2149)	→	2150
0₁(837)	→	838
0₀(3)	→	2
0₀(5)	→	2
0₀(2)	→	2
0₀(4)	→	2
0₀(1)	→	2
0₀(6)	→	2
1₀(2)	→	3
1₀(4)	→	3
1₀(3)	→	3
1₀(6)	→	3
1₀(1)	→	3
1₀(5)	→	3
4₁(710)	→	711
4₁(816)	→	817
4₁(707)	→	708
4₁(1311)	→	1312
4₁(1413)	→	1414
4₁(1409)	→	1410
4₁(1009)	→	1010
4₁(563)	→	564
4₁(508)	→	509
4₁(98)	→	99
4₁(1338)	→	1339
4₁(854)	→	855
4₁(618)	→	619
4₁(834)	→	835
4₁(829)	→	830
4₁(13)	→	14
4₁(1008)	→	1009
4₁(305)	→	306
4₁(902)	→	903
4₁(67)	→	68
4₁(69)	→	70
4₁(957)	→	958
4₁(1088)	→	1089
4₁(632)	→	633
4₁(169)	→	170
4₁(718)	→	719
4₁(648)	→	649
4₁(104)	→	105
4₁(41)	→	42
4₁(874)	→	875
4₁(1151)	→	1152
4₁(433)	→	434
4₁(1267)	→	1268
4₁(8)	→	9
4₁(549)	→	550
4₁(1659)	→	1660
4₁(1665)	→	1666
4₁(808)	→	809
4₁(1395)	→	1396
4₁(1323)	→	1324
4₁(922)	→	923
4₁(1185)	→	1186
4₁(1049)	→	1050
4₁(1177)	→	1178
4₁(654)	→	655
4₁(1401)	→	1402
4₁(1463)	→	1464
4₁(2279)	→	2280
4₁(2283)	→	2284
4₁(1663)	→	1664
4₁(620)	→	621
4₁(629)	→	630
4₁(1661)	→	1662
4₁(43)	→	44
4₁(1053)	→	1054
4₁(2277)	→	2278
4₁(1096)	→	1097
4₁(93)	→	94
4₁(556)	→	557
4₁(1545)	→	1546
4₁(457)	→	458
4₁(1119)	→	1120
4₁(2271)	→	2272
4₁(925)	→	926
4₁(10)	→	11
4₁(769)	→	770
4₁(602)	→	603
4₁(1460)	→	1461
4₁(598)	→	599
4₁(370)	→	371
4₁(1490)	→	1491
4₁(870)	→	871
4₁(1415)	→	1416
4₁(1253)	→	1254
4₁(873)	→	874
4₁(931)	→	932
4₁(170)	→	171
4₁(1341)	→	1342
4₁(1855)	→	1856
4₁(301)	→	302
4₁(1407)	→	1408
4₁(1313)	→	1314
1₁(1226)	→	1227
1₁(1055)	→	1056
1₁(1492)	→	1493
1₁(1796)	→	1797
1₁(929)	→	930
1₁(560)	→	561
1₁(821)	→	822
1₁(372)	→	373
1₁(2105)	→	2106
1₁(687)	→	688
1₁(904)	→	905
1₁(1924)	→	1925
1₁(573)	→	574
1₁(653)	→	654
1₁(2554)	→	2555
1₁(17)	→	18
1₁(374)	→	375
1₁(955)	→	956
1₁(1337)	→	1338
1₁(696)	→	697
1₁(1092)	→	1093
1₁(2091)	→	2092
1₁(850)	→	851
1₁(2116)	→	2117
1₁(2482)	→	2483
1₁(880)	→	881
1₁(964)	→	965
1₁(759)	→	760
1₁(465)	→	466
1₁(954)	→	955
1₁(859)	→	860
1₁(1626)	→	1627
1₁(802)	→	803
1₁(1118)	→	1119
1₁(966)	→	967
1₁(1790)	→	1791
1₁(700)	→	701
1₁(1011)	→	1012
1₁(124)	→	125
1₁(163)	→	164
1₁(840)	→	841
1₁(2163)	→	2164
1₁(1438)	→	1439
1₁(2498)	→	2499
1₁(764)	→	765
1₁(1315)	→	1316
1₁(1794)	→	1795
1₁(2492)	→	2493
1₁(1232)	→	1233
1₁(2456)	→	2457
1₁(1283)	→	1284
1₁(1287)	→	1288
1₁(845)	→	846
1₁(2161)	→	2162
1₁(561)	→	562
1₁(622)	→	623
1₁(1291)	→	1292
1₁(144)	→	145
1₁(1265)	→	1266
1₁(2071)	→	2072
1₁(1005)	→	1006
1₁(307)	→	308
1₁(2476)	→	2477
1₁(240)	→	241
1₁(730)	→	731
1₁(1090)	→	1091
1₁(1627)	→	1628
1₁(1922)	→	1923
1₁(2474)	→	2475
1₁(2103)	→	2104
1₁(504)	→	505
1₁(900)	→	901
1₁(1034)	→	1035
1₁(96)	→	97
1₁(2490)	→	2491
1₁(1909)	→	1910
1₁(694)	→	695
1₁(1180)	→	1181
1₁(990)	→	991
1₁(895)	→	896
1₁(871)	→	872
1₁(803)	→	804
1₁(1543)	→	1544
1₁(511)	→	512
1₁(2185)	→	2186
1₁(1285)	→	1286
1₁(1459)	→	1460
1₁(2500)	→	2501
1₁(2558)	→	2559
1₁(243)	→	244
1₁(627)	→	628
1₁(1257)	→	1258
1₁(2560)	→	2561
1₁(2589)	→	2590
1₁(1436)	→	1437
1₁(1224)	→	1225
1₁(513)	→	514
1₁(746)	→	747
1₁(1234)	→	1235
1₁(2165)	→	2166
1₁(2099)	→	2100
1₁(1496)	→	1497
1₁(438)	→	439
1₁(1498)	→	1499
1₁(455)	→	456
1₁(767)	→	768
1₁(865)	→	866
1₁(2159)	→	2160
1₁(1712)	→	1713
1₁(1310)	→	1311
1₁(2077)	→	2078
1₁(846)	→	847
1₁(1178)	→	1179
1₁(432)	→	433
1₁(2484)	→	2485
1₁(1400)	→	1401
1₁(1911)	→	1912
1₁(1857)	→	1858
1₁(2169)	→	2170
1₁(2173)	→	2174
1₁(1211)	→	1212
1₁(692)	→	693
1₁(894)	→	895
1₁(166)	→	167
1₁(15)	→	16
1₁(2171)	→	2172
1₁(571)	→	572
1₁(146)	→	147
1₁(172)	→	173
1₁(2079)	→	2080
1₁(1788)	→	1789
1₁(1149)	→	1150
1₁(809)	→	810
1₁(1789)	→	1790
1₁(628)	→	629
1₁(126)	→	127
1₁(557)	→	558
1₁(684)	→	685
1₁(659)	→	660
1₁(744)	→	745
1₁(509)	→	510
1₁(634)	→	635
1₁(483)	→	484
1₁(698)	→	699
1₁(962)	→	963
1₁(2101)	→	2102
1₁(617)	→	618
1₁(95)	→	96
1₁(1289)	→	1290
1₁(1279)	→	1280
1₁(2093)	→	2094
1₁(896)	→	897
1₁(927)	→	928
1₁(1182)	→	1183
1₁(1343)	→	1344
1₁(2167)	→	2168
1₁(481)	→	482
1₁(717)	→	718
1₁(1444)	→	1445
1₁(545)	→	546
1₁(1264)	→	1265
1₂(2135)	→	2136
1₂(2366)	→	2367
1₂(2196)	→	2197
1₂(920)	→	921
1₂(1977)	→	1978
1₂(1972)	→	1973
1₂(1970)	→	1971
1₂(1974)	→	1975
1₂(1930)	→	1931
1₂(1964)	→	1965
1₂(1940)	→	1941
1₂(2131)	→	2132
1₂(943)	→	944
1₂(1899)	→	1900
1₂(2120)	→	2121
1₂(1948)	→	1949
1₂(1897)	→	1898
1₂(1866)	→	1867
1₂(979)	→	980
1₂(918)	→	919
1₂(1901)	→	1902
1₂(2127)	→	2128
1₂(2203)	→	2204
1₂(1962)	→	1963
1₂(2354)	→	2355
1₂(944)	→	945
1₂(1886)	→	1887
1₂(1946)	→	1947
1₂(1907)	→	1908
1₂(1938)	→	1939
1₂(1887)	→	1888
1₂(1903)	→	1904
1₂(1868)	→	1869
1₂(980)	→	981
1₂(1983)	→	1984
1₂(1905)	→	1906
1₂(2368)	→	2369
1₂(2125)	→	2126
1₂(1932)	→	1933
4₀(1)	→	1
4₀(6)	→	1
4₀(5)	→	1
4₀(2)	→	1
4₀(3)	→	1
4₀(4)	→	1
2₂(2199)	→	2200
2₂(1978)	→	1979
2₂(2123)	→	2124
2₂(983)	→	984
2₂(948)	→	949
2₂(1862)	→	1863
2₂(2126)	→	2127
2₂(1890)	→	1891
2₂(1979)	→	1980
2₂(1892)	→	1893
2₂(949)	→	950
2₂(984)	→	985
2₂(985)	→	986
2₂(1984)	→	1985
2₂(914)	→	915
2₂(1891)	→	1892
2₂(1985)	→	1986
2₂(947)	→	948
2₂(917)	→	918
2₂(2197)	→	2198
2₂(1865)	→	1866

The automaton is closed under rewriting as it is compatible.