Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3589)

The rewrite relation of the following TRS is considered.

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

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

0(0(0(x1)))	→	5(5(3(3(2(3(2(2(4(0(x1))))))))))	(44)
5(0(0(x1)))	→	4(3(3(0(5(1(4(3(2(1(x1))))))))))	(45)
2(0(0(0(x1))))	→	2(4(3(2(4(0(1(2(2(0(x1))))))))))	(46)
0(0(3(1(x1))))	→	3(0(3(4(3(2(2(2(2(1(x1))))))))))	(47)
0(0(3(1(x1))))	→	4(2(0(4(5(5(3(3(2(1(x1))))))))))	(48)
0(2(4(5(x1))))	→	2(3(2(5(3(0(4(4(3(5(x1))))))))))	(49)
0(4(0(0(0(x1)))))	→	2(1(5(5(5(5(0(3(4(1(x1))))))))))	(50)
0(0(3(1(0(x1)))))	→	0(3(2(5(3(2(0(1(5(0(x1))))))))))	(51)
4(3(1(0(4(x1)))))	→	4(4(4(1(4(4(2(3(2(4(x1))))))))))	(52)
2(0(2(0(4(x1)))))	→	3(2(1(1(2(3(4(1(3(5(x1))))))))))	(53)
0(5(2(0(4(x1)))))	→	3(0(1(5(4(4(3(2(1(3(x1))))))))))	(54)
5(2(0(0(5(x1)))))	→	5(0(3(5(4(3(3(0(1(0(x1))))))))))	(55)
0(0(0(2(5(x1)))))	→	5(0(5(2(4(3(3(2(5(5(x1))))))))))	(56)
0(0(5(0(0(1(x1))))))	→	4(0(1(0(5(5(5(5(1(2(x1))))))))))	(57)
0(5(0(5(3(1(x1))))))	→	0(3(3(5(3(2(3(2(4(2(x1))))))))))	(58)
4(2(0(4(5(1(x1))))))	→	5(5(0(1(1(3(2(1(0(1(x1))))))))))	(59)
3(0(0(0(0(2(x1))))))	→	1(5(3(1(3(3(4(5(0(1(x1))))))))))	(60)
0(1(5(0(0(2(x1))))))	→	3(2(5(3(2(2(5(3(5(2(x1))))))))))	(61)
4(1(3(1(2(2(x1))))))	→	3(4(1(2(2(2(3(5(1(1(x1))))))))))	(62)
3(1(0(2(0(3(x1))))))	→	3(4(3(3(5(1(5(5(0(3(x1))))))))))	(63)
1(4(1(2(1(4(x1))))))	→	1(5(4(4(4(1(2(5(5(3(x1))))))))))	(64)
2(3(3(1(0(5(x1))))))	→	0(1(5(1(5(5(5(3(3(0(x1))))))))))	(65)
0(2(0(3(1(5(x1))))))	→	4(3(5(1(0(1(5(5(4(2(x1))))))))))	(66)
4(0(4(1(0(0(0(x1)))))))	→	5(4(2(1(2(1(2(4(4(2(x1))))))))))	(67)
2(4(1(2(0(2(0(x1)))))))	→	2(4(3(1(1(4(2(4(4(2(x1))))))))))	(68)
4(2(2(0(0(3(0(x1)))))))	→	0(3(4(5(5(3(5(0(1(0(x1))))))))))	(69)
0(2(0(0(5(3(0(x1)))))))	→	4(4(0(3(4(5(1(3(2(0(x1))))))))))	(70)
2(0(0(3(1(0(1(x1)))))))	→	4(1(1(0(5(3(0(1(0(1(x1))))))))))	(71)
0(2(0(0(2(0(1(x1)))))))	→	4(4(0(1(1(3(1(2(2(1(x1))))))))))	(72)
5(3(1(2(0(0(2(x1)))))))	→	4(3(0(0(1(2(2(4(5(2(x1))))))))))	(73)
3(0(0(4(0(0(2(x1)))))))	→	3(2(4(5(0(0(1(1(1(1(x1))))))))))	(74)
0(0(0(0(4(1(2(x1)))))))	→	4(1(3(1(1(2(0(4(1(2(x1))))))))))	(75)
1(2(3(5(0(4(2(x1)))))))	→	1(2(1(3(2(4(0(3(0(2(x1))))))))))	(76)
0(5(4(0(2(5(2(x1)))))))	→	0(1(2(0(5(2(2(2(2(1(x1))))))))))	(77)
3(1(0(2(2(0(3(x1)))))))	→	4(3(2(4(1(1(5(4(1(3(x1))))))))))	(78)
0(0(4(2(0(4(3(x1)))))))	→	0(3(0(1(1(3(5(4(2(3(x1))))))))))	(79)
3(1(0(4(2(0(4(x1)))))))	→	3(0(3(1(2(2(1(1(3(4(x1))))))))))	(80)
4(0(4(5(0(4(4(x1)))))))	→	4(2(4(3(0(1(1(5(4(4(x1))))))))))	(81)
0(2(0(5(2(0(5(x1)))))))	→	4(4(2(0(5(2(4(3(2(3(x1))))))))))	(82)
2(4(1(4(1(2(5(x1)))))))	→	0(3(0(2(1(3(4(2(3(1(x1))))))))))	(83)
0(5(0(1(1(4(5(x1)))))))	→	3(0(4(1(5(5(5(4(3(4(x1))))))))))	(84)
4(0(2(1(1(4(5(x1)))))))	→	4(2(2(4(4(4(5(5(3(4(x1))))))))))	(85)
3(1(0(0(2(4(5(x1)))))))	→	4(2(1(1(3(4(2(4(3(2(x1))))))))))	(86)

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:

1206	→	617
314	→	1
314	→	671
314	→	305
314	→	669
314	→	9
314	→	482
314	→	86
314	→	44
339	→	1089
339	→	1117
1602	→	1980
1151	→	2183
846	→	835
2124	→	559
2124	→	2287
534	→	510
534	→	878
534	→	164
534	→	4
534	→	536
534	→	1979
534	→	2143
534	→	1733
2166	→	165
2593	→	559
2253	→	645
2253	→	2328
2393	→	559
917	→	904
2178	→	88
89	→	191
1513	→	191
789	→	1085
789	→	1113
789	→	1534
1057	→	338
1441	→	884
1441	→	625
1441	→	878
1441	→	164
1441	→	4
1441	→	510
1441	→	536
1441	→	1979
1441	→	2143
1441	→	1733
1529	→	1521
750	→	938
356	→	331
356	→	509
356	→	355
356	→	139
356	→	64
356	→	275
356	→	436
356	→	5
356	→	374
356	→	1010
1492	→	768
860	→	825
2110	→	808
533	→	2019
533	→	2435
658	→	6
658	→	845
658	→	581
658	→	567
658	→	88
658	→	140
658	→	511
658	→	2192
658	→	645
658	→	2255
658	→	2176
1624	→	809
2141	→	559
1630	→	870
1603	→	645
1603	→	1765
10	→	1561
2196	→	191
2277	→	870
1163	→	1796
1163	→	1954
1163	→	2121
1163	→	2250
1163	→	2258
1163	→	2262
2100	→	645
2100	→	2459
2100	→	2484
2247	→	807
1261	→	1254
97	→	2
97	→	236
97	→	306
97	→	278
97	→	650
734	→	1074
734	→	1111
1379	→	1365
2198	→	559
1638	→	1732
2116	→	559
2116	→	2289
915	→	904
1688	→	919
1864	→	225
1717	→	919
1885	→	225
578	→	568
781	→	313
374	→	331
374	→	1571
96	→	1087
96	→	1115
96	→	1536
1435	→	722
2182	→	88
560	→	673
560	→	692
1782	→	200
1979	→	559
2211	→	2457
1972	→	2523
1593	→	807
1363	→	559
1363	→	1452
628	→	748
995	→	1822
995	→	1857
995	→	1898
995	→	1931
995	→	2173
1740	→	2519
2056	→	1033
2056	→	308
511	→	756
2070	→	628
2126	→	559
2126	→	2276
2434	→	297
2434	→	783
1916	→	397
276	→	225
276	→	1031
276	→	1143
466	→	2
466	→	741
466	→	255
466	→	615
668	→	4
668	→	884
668	→	625
668	→	510
668	→	827
668	→	800
668	→	808
668	→	534
668	→	332
1887	→	225
2483	→	332
625	→	1948
625	→	2125
625	→	2246
625	→	2254
625	→	2268
1953	→	457
1953	→	2085
18	→	1
18	→	482
18	→	163
18	→	484
18	→	86
18	→	1732
18	→	1649
624	→	615
2086	→	660
226	→	387
226	→	1205
1118	→	397
2249	→	807
2260	→	2377
2545	→	807
120	→	88
3	→	41
3	→	117
3	→	277
3	→	373
3	→	455
3	→	533
2335	→	200
333	→	1428
772	→	657
2271	→	809
553	→	2175
1628	→	809
1634	→	870
1033	→	618
817	→	645
817	→	1378
817	→	1426
225	→	500
1114	→	397
460	→	1436
1995	→	559
2232	→	807
2149	→	458
626	→	615
2438	→	2426
1294	→	1284
805	→	2461
1858	→	225
740	→	725
2012	→	1009
2012	→	649
2012	→	670
2012	→	672
2012	→	647
2012	→	807
2012	→	397
646	→	3
646	→	844
646	→	672
646	→	670
2252	→	2400
2539	→	296
1340	→	559
1340	→	1633
9	→	163
9	→	305
9	→	484
9	→	671
331	→	809
331	→	818
5	→	64
5	→	139
5	→	275
5	→	355
5	→	436
5	→	509
774	→	765
2143	→	559
2275	→	870
1190	→	1179
1190	→	1512
1932	→	397
65	→	9
2524	→	88
1918	→	397
199	→	1
199	→	671
199	→	305
199	→	669
199	→	9
199	→	482
199	→	86
199	→	44
199	→	582
199	→	659
199	→	457
199	→	67
199	→	308
199	→	1033
199	→	1732
199	→	1638
199	→	1649
456	→	397
2215	→	2204
483	→	458
891	→	2451
255	→	225
255	→	1046
1134	→	457
1134	→	1297
1768	→	191
1768	→	1779
1646	→	2352
1646	→	2367
1646	→	2375
1646	→	2449
1646	→	2542
1646	→	2552
1646	→	2554
1970	→	2521
1806	→	776
1806	→	457
1806	→	1949
674	→	1538
674	→	1569
1866	→	225
90	→	200
622	→	198
1344	→	559
1344	→	1631
892	→	1933
892	→	1960
892	→	2115
892	→	2231
892	→	2260
892	→	2264
397	→	647
397	→	649
397	→	807
397	→	1009
2323	→	191
2323	→	2332
2471	→	692
2471	→	673
2471	→	560
304	→	233
2444	→	8
2444	→	2538
2444	→	2540
2520	→	88
1164	→	692
1164	→	354
1164	→	5
1164	→	673
1164	→	560
1164	→	2269
1601	→	645
1601	→	1767
1132	→	457
1132	→	1293
1162	→	2453
2118	→	559
1	→	85
1	→	161
1	→	235
1	→	330
1	→	396
1	→	535
841	→	1364
826	→	339
826	→	1489
2460	→	458
2325	→	191
2325	→	2334
877	→	789
877	→	1483
1298	→	1284
1570	→	821
2122	→	559
2122	→	2272
2256	→	2394
755	→	645
1112	→	397
667	→	903
667	→	936
667	→	1347
833	→	726
332	→	886
2190	→	88
1838	→	1823
1154	→	510
2454	→	559
2557	→	809
1507	→	396
342	→	331
342	→	1563
197	→	2474
1645	→	2592
1130	→	614
2212	→	2443
747	→	95
1934	→	2101
2370	→	457
2370	→	2447
44	→	9
1342	→	559
1342	→	1629
2084	→	660
2288	→	870
2331	→	191
2331	→	2340
1515	→	191
606	→	1380
1616	→	645
1616	→	1771
2395	→	559
2577	→	17
842	→	667
536	→	510
536	→	878
612	→	1151
2176	→	88
735	→	4
735	→	884
735	→	625
735	→	878
735	→	164
735	→	510
735	→	536
735	→	1979
735	→	2143
735	→	1733
1772	→	191
1772	→	1781
881	→	870
881	→	1053
881	→	1434
297	→	1481
297	→	1528
993	→	2201
1554	→	397
86	→	9
86	→	482
86	→	669
86	→	535
86	→	330
86	→	161
86	→	85
86	→	235
86	→	396
86	→	1
86	→	1732
86	→	1638
86	→	1649
1348	→	559
1348	→	1450
1030	→	297
1030	→	1520
556	→	510
556	→	869
233	→	1189
233	→	2013
233	→	2057
1421	→	720
518	→	206
1373	→	692
1373	→	354
1373	→	5
1373	→	673
1373	→	560
1373	→	2267
1373	→	2269
1622	→	809
2333	→	200
1971	→	510
161	→	1978
2563	→	191
2563	→	2568
2058	→	2047
1766	→	191
1766	→	1773
2112	→	2101
2565	→	191
2565	→	2570
1564	→	820
912	→	1884
912	→	1923
912	→	2199
614	→	1946
614	→	2123
614	→	2233
614	→	2252
614	→	2266
844	→	835
844	→	439
844	→	533
844	→	373
844	→	117
844	→	41
844	→	277
844	→	455
844	→	3
844	→	846
1453	→	736
1926	→	397
2174	→	396
509	→	2191
2003	→	2437
207	→	1
207	→	671
207	→	305
207	→	669
207	→	9
207	→	482
207	→	86
207	→	776
207	→	1732
207	→	1638
207	→	1649
207	→	1949
976	→	671
976	→	305
976	→	669
976	→	9
976	→	535
976	→	330
976	→	161
976	→	85
976	→	235
976	→	396
976	→	1
976	→	482
976	→	86
976	→	1732
976	→	1638
976	→	1649
257	→	225
172	→	4
172	→	884
172	→	625
172	→	878
172	→	164
172	→	510
172	→	536
172	→	332
172	→	1979
172	→	2143
172	→	1733
779	→	2416
779	→	2439
1084	→	884
1084	→	625
1084	→	878
1084	→	164
1084	→	4
1084	→	510
1084	→	536
1084	→	2143
1084	→	1979
171	→	1178
171	→	2424
2550	→	2578
648	→	638
648	→	1491
810	→	847
810	→	854
6	→	66
6	→	141
6	→	224
6	→	371
6	→	438
6	→	555
554	→	510
554	→	614
554	→	764
554	→	880
554	→	949
2569	→	200
404	→	197
1032	→	1555
1539	→	803
88	→	296
88	→	581
88	→	627
88	→	845
2448	→	660
2213	→	846
2213	→	439
2213	→	3
2213	→	844
1186	→	2140
2368	→	1934
1092	→	1075
555	→	2185
2458	→	87
2458	→	2482
1292	→	884
1292	→	625
1292	→	510
1292	→	827
1292	→	4
1292	→	800
1292	→	808
1292	→	534
2200	→	559
1047	→	1032
613	→	3
613	→	807
613	→	647
613	→	672
613	→	670
613	→	649
613	→	397
699	→	575
615	→	741
615	→	255
615	→	557
615	→	341
615	→	119
615	→	43
615	→	256
615	→	419
615	→	2
615	→	626
776	→	765
67	→	9
67	→	457
67	→	659
1146	→	502
657	→	1153
485	→	458
2022	→	581
2022	→	2069
2022	→	2195
2403	→	559
1346	→	559
204	→	1553
437	→	397
437	→	637
437	→	799
1647	→	9
1647	→	669
1647	→	85
1647	→	235
1647	→	396
1647	→	535
1647	→	330
1647	→	161
1647	→	1
1647	→	482
1647	→	86
1647	→	1732
1647	→	1649
2263	→	809
1490	→	765
569	→	728
853	→	197
1188	→	807
1188	→	647
1188	→	672
1188	→	3
1188	→	670
1188	→	649
1188	→	397
808	→	800
808	→	827
2	→	43
2	→	119
2	→	256
2	→	341
2	→	419
2	→	557
313	→	916
313	→	931
313	→	1362
313	→	1637
2329	→	191
2329	→	2338
937	→	919
954	→	950
954	→	969
2267	→	809
4	→	8
4	→	87
4	→	254
4	→	353
4	→	421
4	→	553
1291	→	1689
1291	→	1716
1291	→	2144
118	→	88
118	→	577
2551	→	645
2551	→	2562
1150	→	510
1945	→	1934
582	→	568
582	→	605
582	→	1446
2258	→	2392
1711	→	919
557	→	2193
501	→	1254
1821	→	309
2579	→	559
801	→	1058
2571	→	200
1451	→	736
904	→	1029
580	→	568
508	→	17
2417	→	627
1587	→	807
1535	→	800
2341	→	200
2147	→	559
2553	→	645
2553	→	2564
16	→	2119
1059	→	1056
1997	→	559
2048	→	2502
913	→	236
913	→	2
1224	→	818
1224	→	331
1224	→	297
1224	→	509
1224	→	355
1224	→	139
1224	→	64
1224	→	275
1224	→	436
1224	→	5
1224	→	783
1224	→	372
2184	→	88
2254	→	2402
1063	→	800
1334	→	559
1045	→	1032
2475	→	2462
535	→	2177
2436	→	2425
2265	→	809
1692	→	88
306	→	1260
2255	→	645
2255	→	2330
2376	→	457
2376	→	2445
623	→	1952
623	→	2138
623	→	2248
623	→	2256
623	→	2270
2442	→	2425
2456	→	559
2456	→	2558
1600	→	1994
1705	→	88
636	→	5
636	→	818
636	→	331
636	→	297
636	→	783
636	→	372
85	→	1648
85	→	1687
85	→	1704
85	→	2142
2440	→	2425
1482	→	758
2353	→	225
140	→	88
140	→	567
2327	→	191
2327	→	2336
1216	→	1471
672	→	660
1455	→	738
2098	→	660
1832	→	818
1832	→	1571
1832	→	1010
1832	→	331
1832	→	374
1440	→	1863
1440	→	1915
236	→	225
236	→	1044
236	→	1145
236	→	1465
1556	→	822
1543	→	812
1526	→	1865
1526	→	1917
1526	→	2197
1632	→	870
694	→	700
2192	→	88
506	→	2099
506	→	2111
1943	→	741
1943	→	255
1943	→	2
1943	→	615
1187	→	1970
2339	→	200
234	→	1
234	→	305
234	→	671
234	→	765
234	→	776
234	→	9
234	→	65
234	→	457
234	→	1949
2337	→	200
2202	→	397
806	→	312
806	→	1374
885	→	870
885	→	1062
1780	→	200
42	→	9
1179	→	1215
1179	→	1514
719	→	5
719	→	692
719	→	354
719	→	673
719	→	560
719	→	2267
719	→	2269
1122	→	1283
2257	→	645
2257	→	2326
2251	→	807
162	→	88
162	→	579
162	→	843
1396	→	458
1259	→	843
1541	→	559
1910	→	1899
2269	→	809
1572	→	820
948	→	753
2186	→	88
278	→	225
1090	→	1075
458	→	1157
893	→	482
893	→	163
893	→	484
893	→	86
893	→	85
893	→	235
893	→	396
893	→	535
893	→	330
893	→	161
893	→	1
893	→	1732
893	→	1649
763	→	206
952	→	786
1447	→	1436
566	→	312
2194	→	88
1372	→	1691
1372	→	1710
1372	→	2146
2139	→	559
2139	→	2274
2290	→	870
198	→	1395
198	→	1420
1429	→	722
1484	→	765
1774	→	200
2076	→	660
2014	→	2003
771	→	2418
771	→	2441
17	→	1133
17	→	1341
17	→	1594
17	→	1615
17	→	1621
17	→	1944
1116	→	397
1149	→	2179
2543	→	807
2541	→	559
510	→	559
510	→	625
510	→	775
510	→	884
510	→	953
727	→	206
1537	→	800
718	→	914
718	→	918
718	→	1360
164	→	720
2068	→	628
1144	→	502
1017	→	305
1017	→	671
1017	→	765
1017	→	1
1017	→	776
1017	→	9
1017	→	457
1017	→	1949
1148	→	510
1361	→	559
2401	→	559
2452	→	559
398	→	782
398	→	1542
870	→	989
666	→	1147
206	→	1091
206	→	1119
206	→	1506
206	→	1837
206	→	1909
2234	→	807
703	→	169
1153	→	2189
974	→	2472
203	→	2203
928	→	306
928	→	500
928	→	1145
928	→	225
928	→	1044
928	→	1465
928	→	236
2078	→	660
340	→	5
340	→	818
340	→	331
340	→	374
340	→	10
340	→	1010
142	→	88
142	→	834
465	→	1121
465	→	1343
465	→	1586
465	→	1600
465	→	1623
1290	→	1972
670	→	660
1649	→	1638
1472	→	749
2188	→	191
2355	→	225
1120	→	397
422	→	397
932	→	919
2522	→	88
790	→	3
790	→	844
1741	→	953
1741	→	775
1741	→	559
1741	→	510
1741	→	720
1741	→	164
1741	→	878
1741	→	536
1741	→	1979
1741	→	2143
1741	→	1733
1955	→	457
1955	→	2097
2446	→	660
574	→	2117
1527	→	844
2450	→	559
2450	→	2560
575	→	1131
575	→	1339
575	→	1592
575	→	1602
575	→	1627
575	→	1807
2473	→	2462
1947	→	457
1947	→	2077
2559	→	870
1375	→	1365
1016	→	2002
1016	→	2021
1016	→	2046
1942	→	2354
1942	→	2369
1942	→	2455
1942	→	2544
1942	→	2550
1942	→	2556
2561	→	870
558	→	510
558	→	623
558	→	773
558	→	882
1908	→	671
1908	→	305
1908	→	9
1908	→	44
2145	→	559
2145	→	2165
611	→	1345
2261	→	645
2261	→	2322
372	→	331
680	→	206
680	→	1540
354	→	331
1562	→	820
2591	→	559
194	→	777
1152	→	510
1973	→	510
2180	→	88
1924	→	397
1615	→	1996
1961	→	457
1961	→	2075
576	→	5
576	→	692
576	→	354
576	→	673
576	→	560
576	→	10
576	→	2269
166	→	1454
2020	→	581
2020	→	2067
2020	→	2187
2378	→	559
439	→	397
1088	→	1075
992	→	2214
2510	→	278
2510	→	650
975	→	2148
975	→	2163
2485	→	332
2419	→	627
1949	→	457
1949	→	2083
1981	→	559
2164	→	332
996	→	671
996	→	305
996	→	669
996	→	9
996	→	535
996	→	330
996	→	161
996	→	85
996	→	235
996	→	396
996	→	1
996	→	482
996	→	86
996	→	1732
996	→	1638
996	→	1649
2273	→	870
2259	→	645
2259	→	2324
395	→	4
395	→	884
395	→	625
395	→	878
395	→	164
395	→	510
395	→	536
395	→	2143
395	→	1979
1147	→	2181
192	→	736
780	→	1149
656	→	1333
2120	→	559
1061	→	800
1381	→	1368
1595	→	807
1941	→	2576
2552	→	2590
1466	→	742
355	→	1886
355	→	1925
459	→	712
459	→	1820
879	→	870
1086	→	1075
2555	→	809
883	→	870
883	→	1060
1427	→	720
1690	→	88
1808	→	1797
420	→	397
3₁(2568)	→	2569
3₁(2289)	→	2290
3₁(911)	→	912
3₁(765)	→	766
3₁(905)	→	906
3₁(95)	→	96
3₁(1538)	→	1539
3₁(2338)	→	2339
3₁(1185)	→	1186
3₁(2570)	→	2571
3₁(15)	→	16
3₁(563)	→	564
3₁(2336)	→	2337
3₁(200)	→	201
3₁(196)	→	197
3₁(910)	→	911
3₁(1781)	→	1782
3₁(438)	→	439
3₁(419)	→	420
3₁(1257)	→	1258
3₁(2558)	→	2559
3₁(887)	→	888
3₁(1925)	→	1926
3₁(671)	→	672
3₁(2083)	→	2084
3₁(815)	→	816
3₁(761)	→	762
3₁(1124)	→	1125
3₁(2340)	→	2341
3₁(1553)	→	1554
3₁(659)	→	660
3₁(889)	→	890
3₁(2445)	→	2446
3₁(679)	→	680
3₁(2231)	→	2232
3₁(1371)	→	1372
3₁(1117)	→	1118
3₁(455)	→	456
3₁(989)	→	990
3₁(607)	→	608
3₁(2332)	→	2333
3₁(2085)	→	2086
3₁(421)	→	422
3₁(2544)	→	2545
3₁(2334)	→	2335
3₁(1592)	→	1593
3₁(2560)	→	2561
3₁(1773)	→	1774
3₁(1075)	→	1076
3₁(1113)	→	1114
3₁(2077)	→	2078
3₁(642)	→	643
3₁(394)	→	395
3₁(198)	→	199
3₁(1917)	→	1918
3₁(645)	→	646
3₁(1454)	→	1455
3₁(837)	→	838
3₁(332)	→	333
3₁(2075)	→	2076
3₁(2233)	→	2234
3₁(2542)	→	2543
3₁(834)	→	835
3₁(1012)	→	1013
3₁(882)	→	883
3₁(841)	→	842
3₁(890)	→	891
3₁(610)	→	611
3₁(1115)	→	1116
3₁(1111)	→	1112
3₁(724)	→	725
3₁(635)	→	636
3₁(309)	→	310
3₁(232)	→	233
3₁(1923)	→	1924
3₁(561)	→	562
3₁(312)	→	313
3₁(1182)	→	1183
3₁(729)	→	730
3₁(463)	→	464
3₁(94)	→	95
3₁(460)	→	461
3₁(843)	→	844
3₁(1256)	→	1257
3₁(878)	→	879
3₁(809)	→	810
3₁(713)	→	714
3₁(643)	→	644
3₁(1183)	→	1184
3₁(169)	→	170
3₁(869)	→	870
3₁(503)	→	504
3₁(720)	→	721
3₁(788)	→	789
3₁(1283)	→	1284
3₁(1931)	→	1932
3₁(12)	→	13
3₁(502)	→	503
3₁(1158)	→	1159
3₁(2276)	→	2277
3₁(845)	→	846
3₁(297)	→	298
3₁(880)	→	881
3₁(1446)	→	1447
3₁(1293)	→	1294
3₁(1631)	→	1632
3₁(89)	→	90
3₁(629)	→	630
3₁(2447)	→	2448
3₁(717)	→	718
3₁(1633)	→	1634
3₁(971)	→	972
3₁(2250)	→	2251
3₁(608)	→	609
3₁(827)	→	828
3₁(2443)	→	2444
3₁(660)	→	661
3₁(399)	→	400
3₁(459)	→	460
3₁(2272)	→	2273
3₁(884)	→	885
3₁(1297)	→	1298
3₁(2097)	→	2098
3₁(14)	→	15
3₁(2248)	→	2249
3₁(2246)	→	2247
3₁(436)	→	437
3₁(225)	→	226
3₁(873)	→	874
3₁(194)	→	195
3₁(975)	→	976
3₁(769)	→	770
3₁(737)	→	738
3₁(1119)	→	1120
3₁(1078)	→	1079
3₁(565)	→	566
3₁(1125)	→	1126
3₁(1586)	→	1587
3₁(1128)	→	1129
3₁(1629)	→	1630
3₁(619)	→	620
3₁(823)	→	824
3₁(669)	→	670
3₁(229)	→	230
3₁(1223)	→	1224
3₁(389)	→	390
3₁(2287)	→	2288
3₁(1367)	→	1368
3₁(1525)	→	1526
3₁(1083)	→	1084
3₁(973)	→	974
3₁(1217)	→	1218
3₁(570)	→	571
3₁(2201)	→	2202
3₁(615)	→	616
3₁(1594)	→	1595
3₁(2274)	→	2275
3₁(802)	→	803
3₁(1284)	→	1285
3₁(1015)	→	1016
3₁(1779)	→	1780
3₁(1915)	→	1916
3₁(396)	→	397
3₁(1380)	→	1381
1₂(2002)	→	2003
1₂(1934)	→	1935
1₂(942)	→	943
1₂(2439)	→	2440
1₂(2435)	→	2436
1₂(1905)	→	1906
1₂(1710)	→	1711
1₂(1687)	→	1688
1₂(2013)	→	2014
1₂(2431)	→	2432
1₂(922)	→	923
1₂(2008)	→	2009
1₂(1828)	→	1829
1₂(1734)	→	1735
1₂(2106)	→	2107
1₂(931)	→	932
1₂(918)	→	919
1₂(2441)	→	2442
1₂(2011)	→	2012
1₂(2462)	→	2463
1₂(1899)	→	1900
1₂(2425)	→	2426
1₂(2505)	→	2506
1₂(2108)	→	2109
1₂(936)	→	937
1₂(2205)	→	2206
1₂(1716)	→	1717
1₂(2209)	→	2210
1₂(2424)	→	2425
1₂(938)	→	939
1₂(2206)	→	2207
1₂(2437)	→	2438
3₂(946)	→	947
3₂(940)	→	941
3₂(2469)	→	2470
3₂(2210)	→	2211
3₂(926)	→	927
3₂(2101)	→	2102
3₂(2204)	→	2205
3₂(1936)	→	1937
3₂(1907)	→	1908
3₂(1909)	→	1910
3₂(1643)	→	1644
3₂(2427)	→	2428
3₂(2465)	→	2466
3₂(1898)	→	1899
3₂(1901)	→	1902
3₂(925)	→	926
3₂(1937)	→	1938
3₂(1738)	→	1739
3₂(2433)	→	2434
3₂(2508)	→	2509
3₂(2048)	→	2049
3₂(1940)	→	1941
3₂(945)	→	946
3₂(1644)	→	1645
3₂(1804)	→	1805
3₂(920)	→	921
3₂(2212)	→	2213
3₂(2052)	→	2053
3₂(1824)	→	1825
3₂(1801)	→	1802
3₂(2055)	→	2056
3₂(2007)	→	2008
3₂(2102)	→	2103
3₂(1641)	→	1642
3₂(1797)	→	1798
3₂(2009)	→	2010
3₂(2006)	→	2007
4₂(1798)	→	1799
4₂(1739)	→	1740
4₂(927)	→	928
4₂(1826)	→	1827
4₂(1829)	→	1830
4₂(1903)	→	1904
4₂(947)	→	948
4₂(2509)	→	2510
4₂(1799)	→	1800
4₂(2214)	→	2215
4₂(1938)	→	1939
4₂(1831)	→	1832
4₂(1830)	→	1831
4₂(2502)	→	2503
4₂(1638)	→	1639
4₂(2005)	→	2006
4₂(1902)	→	1903
4₂(1827)	→	1828
4₂(1822)	→	1823
4₂(921)	→	922
4₂(2203)	→	2204
4₂(1736)	→	1737
4₂(2432)	→	2433
4₂(1837)	→	1838
4₂(941)	→	942
4₂(2468)	→	2469
0₁(1946)	→	1947
0₁(751)	→	752
0₁(757)	→	758
0₁(2369)	→	2370
0₁(1489)	→	1490
0₁(93)	→	94
0₁(517)	→	518
0₁(746)	→	747
0₁(2576)	→	2577
0₁(204)	→	205
0₁(1948)	→	1949
0₁(974)	→	975
0₁(840)	→	841
0₁(731)	→	732
0₁(766)	→	767
0₁(775)	→	776
0₁(1952)	→	1953
0₁(41)	→	42
0₁(831)	→	832
0₁(778)	→	779
0₁(1121)	→	1122
0₁(822)	→	823
0₁(728)	→	729
0₁(805)	→	806
0₁(951)	→	952
0₁(1011)	→	1012
0₁(647)	→	648
0₁(2457)	→	2458
0₁(993)	→	994
0₁(1483)	→	1484
0₁(8)	→	9
0₁(816)	→	817
0₁(166)	→	167
0₁(228)	→	229
0₁(1129)	→	1130
0₁(745)	→	746
0₁(773)	→	774
0₁(85)	→	86
0₁(507)	→	508
0₁(637)	→	638
0₁(464)	→	465
0₁(1123)	→	1124
0₁(1372)	→	1373
0₁(43)	→	44
0₁(66)	→	67
0₁(197)	→	198
0₁(1032)	→	1033
0₁(515)	→	516
0₁(1131)	→	1132
0₁(718)	→	719
0₁(1365)	→	1366
0₁(567)	→	568
0₁(1179)	→	1180
0₁(909)	→	910
0₁(581)	→	582
0₁(676)	→	677
0₁(298)	→	299
0₁(577)	→	578
0₁(2173)	→	2174
0₁(764)	→	765
0₁(573)	→	574
0₁(64)	→	65
0₁(1133)	→	1134
0₁(1437)	→	1438
0₁(1481)	→	1482
0₁(1960)	→	1961
0₁(667)	→	668
0₁(313)	→	314
0₁(1161)	→	1162
0₁(579)	→	580
0₁(458)	→	459
0₁(2099)	→	2100
0₁(725)	→	726
0₁(1954)	→	1955
0₁(750)	→	751
0₁(1506)	→	1507
0₁(2375)	→	2376
0₁(1291)	→	1292
0₁(307)	→	308
4₀(3)	→	5
4₀(6)	→	5
4₀(5)	→	5
4₀(4)	→	5
4₀(2)	→	5
4₀(1)	→	5
1₀(2)	→	6
1₀(6)	→	6
1₀(4)	→	6
1₀(1)	→	6
1₀(3)	→	6
1₀(5)	→	6
2₂(1732)	→	1733
2₂(1803)	→	1804
2₂(1639)	→	1640
2₂(1733)	→	1734
2₂(2503)	→	2504
2₂(2207)	→	2208
2₂(1825)	→	1826
2₂(1900)	→	1901
2₂(1642)	→	1643
2₂(1805)	→	1806
2₂(2046)	→	2047
2₂(1640)	→	1641
2₂(1737)	→	1738
2₂(1823)	→	1824
2₂(2208)	→	2209
2₂(2504)	→	2505
2₂(919)	→	920
2₂(2430)	→	2431
2₂(2051)	→	2052
2₂(2429)	→	2430
2₂(2057)	→	2058
2₂(939)	→	940
2₂(1740)	→	1741
2₂(2054)	→	2055
2₂(2050)	→	2051
2₂(2428)	→	2429
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
4₁(170)	→	171
4₁(644)	→	645
4₁(912)	→	913
4₁(2262)	→	2263
4₁(341)	→	342
4₁(756)	→	757
4₁(753)	→	754
4₁(1491)	→	1492
4₁(1258)	→	1259
4₁(856)	→	857
4₁(1058)	→	1059
4₁(296)	→	297
4₁(504)	→	505
4₁(1222)	→	1223
4₁(870)	→	871
4₁(692)	→	693
4₁(800)	→	801
4₁(227)	→	228
4₁(906)	→	907
4₁(203)	→	204
4₁(634)	→	635
4₁(734)	→	735
4₁(353)	→	354
4₁(824)	→	825
4₁(972)	→	973
4₁(335)	→	336
4₁(330)	→	331
4₁(1523)	→	1524
4₁(716)	→	717
4₁(1009)	→	1010
4₁(655)	→	656
4₁(741)	→	742
4₁(2264)	→	2265
4₁(400)	→	401
4₁(857)	→	858
4₁(96)	→	97
4₁(226)	→	227
4₁(355)	→	356
4₁(789)	→	790
4₁(373)	→	374
4₁(1623)	→	1624
4₁(700)	→	701
4₁(90)	→	91
4₁(782)	→	783
4₁(1054)	→	1055
4₁(1010)	→	1011
4₁(1055)	→	1056
4₁(339)	→	340
4₁(559)	→	560
4₁(653)	→	654
4₁(847)	→	848
4₁(167)	→	168
4₁(401)	→	402
4₁(858)	→	859
4₁(334)	→	335
4₁(1077)	→	1078
4₁(9)	→	10
4₁(872)	→	873
4₁(461)	→	462
4₁(1621)	→	1622
4₁(1029)	→	1030
4₁(1526)	→	1527
4₁(206)	→	207
4₁(338)	→	339
4₁(195)	→	196
4₁(1181)	→	1182
4₁(1440)	→	1441
4₁(2266)	→	2267
4₁(1627)	→	1628
4₁(995)	→	996
4₁(726)	→	727
4₁(828)	→	829
4₁(2270)	→	2271
4₁(836)	→	837
4₁(698)	→	699
4₁(2556)	→	2557
4₁(606)	→	607
4₁(786)	→	787
4₁(767)	→	768
4₁(2554)	→	2555
4₁(2268)	→	2269
4₁(852)	→	853
4₁(1465)	→	1466
4₁(1370)	→	1371
4₁(337)	→	338
4₁(654)	→	655
4₁(818)	→	819
4₁(992)	→	993
4₁(1126)	→	1127
4₁(371)	→	372
4₁(388)	→	389
4₁(723)	→	724
2₁(1524)	→	1525
2₁(618)	→	619
2₁(1339)	→	1340
2₁(1426)	→	1427
2₁(807)	→	808
2₁(393)	→	394
2₁(742)	→	743
2₁(1996)	→	1997
2₁(970)	→	971
2₁(1450)	→	1451
2₁(632)	→	633
2₁(695)	→	696
2₁(743)	→	744
2₁(1218)	→	1219
2₁(1972)	→	1973
2₁(333)	→	334
2₁(2117)	→	2118
2₁(1219)	→	1220
2₁(553)	→	554
2₁(1053)	→	1054
2₁(2449)	→	2450
2₁(562)	→	563
2₁(331)	→	332
2₁(758)	→	759
2₁(779)	→	780
2₁(1994)	→	1995
2₁(859)	→	860
2₁(2564)	→	2565
2₁(509)	→	510
2₁(2453)	→	2454
2₁(1362)	→	1363
2₁(2146)	→	2147
2₁(888)	→	889
2₁(1771)	→	1772
2₁(233)	→	234
2₁(88)	→	89
2₁(2144)	→	2145
2₁(1153)	→	1154
2₁(193)	→	194
2₁(557)	→	558
2₁(2197)	→	2198
2₁(2165)	→	2166
2₁(799)	→	800
2₁(994)	→	995
2₁(1333)	→	1334
2₁(1016)	→	1017
2₁(2328)	→	2329
2₁(771)	→	772
2₁(1079)	→	1080
2₁(621)	→	622
2₁(205)	→	206
2₁(311)	→	312
2₁(2330)	→	2331
2₁(2590)	→	2591
2₁(1512)	→	1513
2₁(1060)	→	1061
2₁(1220)	→	1221
2₁(2199)	→	2200
2₁(832)	→	833
2₁(2138)	→	2139
2₁(2140)	→	2141
2₁(2592)	→	2593
2₁(1980)	→	1981
2₁(1014)	→	1015
2₁(1082)	→	1083
2₁(533)	→	534
2₁(2324)	→	2325
2₁(2322)	→	2323
2₁(569)	→	570
2₁(555)	→	556
2₁(191)	→	192
2₁(969)	→	970
2₁(2121)	→	2122
2₁(1151)	→	1152
2₁(2119)	→	2120
2₁(2402)	→	2403
2₁(2115)	→	2116
2₁(11)	→	12
2₁(308)	→	309
2₁(2142)	→	2143
2₁(2482)	→	2483
2₁(192)	→	193
2₁(1341)	→	1342
2₁(1145)	→	1146
2₁(1420)	→	1421
2₁(1765)	→	1766
2₁(876)	→	877
2₁(1536)	→	1537
2₁(1147)	→	1148
2₁(390)	→	391
2₁(1143)	→	1144
2₁(2392)	→	2393
2₁(2484)	→	2485
2₁(768)	→	769
2₁(560)	→	561
2₁(2377)	→	2378
2₁(2125)	→	2126
2₁(171)	→	172
2₁(631)	→	632
2₁(1157)	→	1158
2₁(630)	→	631
2₁(1452)	→	1453
2₁(163)	→	164
2₁(835)	→	836
2₁(2394)	→	2395
2₁(2163)	→	2164
2₁(1820)	→	1821
2₁(1514)	→	1515
2₁(693)	→	694
2₁(2540)	→	2541
2₁(2326)	→	2327
2₁(886)	→	887
2₁(1534)	→	1535
2₁(651)	→	652
2₁(1767)	→	1768
2₁(904)	→	905
2₁(231)	→	232
2₁(2451)	→	2452
2₁(2400)	→	2401
2₁(1149)	→	1150
2₁(168)	→	169
2₁(535)	→	536
2₁(839)	→	840
2₁(1343)	→	1344
2₁(1062)	→	1063
2₁(949)	→	950
2₁(617)	→	618
2₁(812)	→	813
2₁(1978)	→	1979
2₁(1360)	→	1361
2₁(164)	→	165
2₁(505)	→	506
2₁(953)	→	954
2₁(825)	→	826
2₁(754)	→	755
2₁(1345)	→	1346
2₁(813)	→	814
2₁(10)	→	11
2₁(13)	→	14
2₁(787)	→	788
2₁(2455)	→	2456
2₁(501)	→	502
2₁(1540)	→	1541
2₁(871)	→	872
2₁(697)	→	698
2₁(398)	→	399
2₁(2578)	→	2579
2₁(2562)	→	2563
2₁(2123)	→	2124
2₁(2187)	→	2188
2₁(1347)	→	1348
2₁(1970)	→	1971
2₁(2195)	→	2196
2₁(829)	→	830
5₀(3)	→	2
5₀(5)	→	2
5₀(2)	→	2
5₀(4)	→	2
5₀(1)	→	2
5₀(6)	→	2
3₀(2)	→	3
3₀(4)	→	3
3₀(3)	→	3
3₀(6)	→	3
3₀(1)	→	3
3₀(5)	→	3
5₁(92)	→	93
5₁(1285)	→	1286
5₁(1287)	→	1288
5₁(574)	→	575
5₁(1857)	→	1858
5₁(1013)	→	1014
5₁(17)	→	18
5₁(302)	→	303
5₁(801)	→	802
5₁(1205)	→	1206
5₁(1369)	→	1370
5₁(300)	→	301
5₁(256)	→	257
5₁(623)	→	624
5₁(1162)	→	1163
5₁(2352)	→	2353
5₁(513)	→	514
5₁(277)	→	278
5₁(854)	→	855
5₁(1216)	→	1217
5₁(1563)	→	1564
5₁(650)	→	651
5₁(730)	→	731
5₁(855)	→	856
5₁(512)	→	513
5₁(1180)	→	1181
5₁(305)	→	306
5₁(254)	→	255
5₁(2354)	→	2355
5₁(1255)	→	1256
5₁(1286)	→	1287
5₁(506)	→	507
5₁(783)	→	784
5₁(462)	→	463
5₁(990)	→	991
5₁(649)	→	650
5₁(235)	→	236
5₁(752)	→	753
5₁(1520)	→	1521
5₁(1368)	→	1369
5₁(674)	→	675
5₁(1863)	→	1864
5₁(848)	→	849
5₁(662)	→	663
5₁(991)	→	992
5₁(511)	→	512
5₁(641)	→	642
5₁(1074)	→	1075
5₁(1528)	→	1529
5₁(230)	→	231
5₁(616)	→	617
5₁(656)	→	657
5₁(514)	→	515
5₁(1289)	→	1290
5₁(722)	→	723
5₁(202)	→	203
5₁(500)	→	501
5₁(310)	→	311
5₁(611)	→	612
5₁(299)	→	300
5₁(663)	→	664
5₁(1085)	→	1086
5₁(620)	→	621
5₁(1884)	→	1885
5₁(1886)	→	1887
5₁(908)	→	909
5₁(605)	→	606
5₁(892)	→	893
5₁(819)	→	820
5₁(673)	→	674
5₁(402)	→	403
5₁(850)	→	851
5₁(16)	→	17
5₁(564)	→	565
5₁(661)	→	662
5₁(224)	→	225
5₁(678)	→	679
5₁(638)	→	639
5₁(1087)	→	1088
5₁(1127)	→	1128
5₁(625)	→	626
5₁(1561)	→	1562
5₁(891)	→	892
5₁(830)	→	831
5₁(575)	→	576
5₁(715)	→	716
5₁(777)	→	778
5₁(614)	→	615
5₁(849)	→	850
5₁(1366)	→	1367
5₁(1260)	→	1261
5₁(1436)	→	1437
5₁(1091)	→	1092
5₁(465)	→	466
5₁(275)	→	276
5₁(1571)	→	1572
5₁(712)	→	713
5₁(1186)	→	1187
5₁(1865)	→	1866
5₁(714)	→	715
5₁(1089)	→	1090
5₁(301)	→	302
5₁(628)	→	629
5₁(665)	→	666
5₁(1163)	→	1164
5₁(639)	→	640
5₁(201)	→	202
1₁(516)	→	517
1₁(2183)	→	2184
1₁(1395)	→	1396
1₁(666)	→	667
1₁(403)	→	404
1₁(1615)	→	1616
1₁(165)	→	166
1₁(2069)	→	2070
1₁(2254)	→	2255
1₁(820)	→	821
1₁(677)	→	678
1₁(701)	→	702
1₁(821)	→	822
1₁(484)	→	485
1₁(2538)	→	2539
1₁(2179)	→	2180
1₁(1542)	→	1543
1₁(2459)	→	2460
1₁(675)	→	676
1₁(1056)	→	1057
1₁(1288)	→	1289
1₁(736)	→	737
1₁(1555)	→	1556
1₁(2148)	→	2149
1₁(696)	→	697
1₁(392)	→	393
1₁(652)	→	653
1₁(397)	→	398
1₁(1215)	→	1216
1₁(2523)	→	2524
1₁(780)	→	781
1₁(759)	→	760
1₁(749)	→	750
1₁(2418)	→	2419
1₁(1428)	→	1429
1₁(510)	→	511
1₁(950)	→	951
1₁(1438)	→	1439
1₁(814)	→	815
1₁(2521)	→	2522
1₁(1189)	→	1190
1₁(306)	→	307
1₁(875)	→	876
1₁(2175)	→	2176
1₁(914)	→	915
1₁(664)	→	665
1₁(2191)	→	2192
1₁(903)	→	904
1₁(762)	→	763
1₁(1704)	→	1705
1₁(1374)	→	1375
1₁(748)	→	749
1₁(2177)	→	2178
1₁(1439)	→	1440
1₁(640)	→	641
1₁(1600)	→	1601
1₁(2189)	→	2190
1₁(657)	→	658
1₁(1364)	→	1365
1₁(738)	→	739
1₁(336)	→	337
1₁(1122)	→	1123
1₁(785)	→	786
1₁(1602)	→	1603
1₁(387)	→	388
1₁(1434)	→	1435
1₁(770)	→	771
1₁(811)	→	812
1₁(2019)	→	2020
1₁(482)	→	483
1₁(391)	→	392
1₁(694)	→	695
1₁(612)	→	613
1₁(2519)	→	2520
1₁(803)	→	804
1₁(1044)	→	1045
1₁(2067)	→	2068
1₁(2185)	→	2186
1₁(161)	→	162
1₁(851)	→	852
1₁(838)	→	839
1₁(804)	→	805
1₁(633)	→	634
1₁(1076)	→	1077
1₁(733)	→	734
1₁(760)	→	761
1₁(2416)	→	2417
1₁(627)	→	628
1₁(2181)	→	2182
1₁(2252)	→	2253
1₁(2256)	→	2257
1₁(91)	→	92
1₁(141)	→	142
1₁(810)	→	811
1₁(609)	→	610
1₁(139)	→	140
1₁(2258)	→	2259
1₁(1160)	→	1161
1₁(1569)	→	1570
1₁(1178)	→	1179
1₁(457)	→	458
1₁(2193)	→	2194
1₁(1689)	→	1690
1₁(702)	→	703
1₁(784)	→	785
1₁(571)	→	572
1₁(1159)	→	1160
1₁(1081)	→	1082
1₁(1184)	→	1185
1₁(1254)	→	1255
1₁(1031)	→	1032
1₁(1187)	→	1188
1₁(1521)	→	1522
1₁(2021)	→	2022
1₁(1080)	→	1081
1₁(2260)	→	2261
1₁(721)	→	722
1₁(2552)	→	2553
1₁(916)	→	917
1₁(2550)	→	2551
1₁(87)	→	88
1₁(744)	→	745
1₁(1522)	→	1523
1₁(117)	→	118
1₁(303)	→	304
1₁(739)	→	740
1₁(874)	→	875
1₁(568)	→	569
1₁(1378)	→	1379
1₁(1221)	→	1222
1₁(1691)	→	1692
1₁(1471)	→	1472
1₁(1046)	→	1047
1₁(572)	→	573
1₁(1290)	→	1291
1₁(907)	→	908
1₁(119)	→	120
1₁(732)	→	733
5₂(1939)	→	1940
5₂(1802)	→	1803
5₂(2047)	→	2048
5₂(2103)	→	2104
5₂(2053)	→	2054
5₂(2464)	→	2465
5₂(943)	→	944
5₂(2426)	→	2427
5₂(2107)	→	2108
5₂(2467)	→	2468
5₂(2004)	→	2005
5₂(1942)	→	1943
5₂(1646)	→	1647
5₂(1796)	→	1797
5₂(2010)	→	2011
5₂(2104)	→	2105
5₂(2049)	→	2050
5₂(923)	→	924
5₂(2105)	→	2106
5₂(1904)	→	1905
5₂(1645)	→	1646
5₂(2466)	→	2467
5₂(1807)	→	1808
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
0₂(1933)	→	1934
0₂(1735)	→	1736
0₂(2470)	→	2471
0₂(1944)	→	1945
0₂(924)	→	925
0₂(1648)	→	1649
0₂(2211)	→	2212
0₂(1637)	→	1638
0₂(2472)	→	2473
0₂(2474)	→	2475
0₂(2506)	→	2507
0₂(2461)	→	2462
0₂(1906)	→	1907
0₂(2463)	→	2464
0₂(1800)	→	1801
0₂(2111)	→	2112
0₂(2507)	→	2508
0₂(2367)	→	2368
0₂(2003)	→	2004
0₂(1941)	→	1942
0₂(1935)	→	1936
0₂(2109)	→	2110
0₂(944)	→	945

The automaton is closed under rewriting as it is compatible.