Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4141)

The rewrite relation of the following TRS is considered.

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

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:

2645	→	1020
2778	→	1728
2948	→	721
1198	→	724
2430	→	420
3012	→	335
2073	→	882
364	→	1321
364	→	1530
2818	→	2415
2124	→	1030
2124	→	89
2124	→	1127
2124	→	4
2124	→	852
2124	→	291
2124	→	464
2124	→	9
2124	→	1427
2124	→	1311
2124	→	1341
2124	→	2466
2124	→	2415
2124	→	2804
2421	→	2971
534	→	4
534	→	1030
534	→	89
534	→	420
534	→	9
534	→	1028
534	→	41
534	→	1135
534	→	90
534	→	446
534	→	43
534	→	591
534	→	357
534	→	429
534	→	65
534	→	1427
534	→	1311
534	→	1322
534	→	1428
534	→	1339
534	→	1417
534	→	1284
534	→	1295
534	→	2434
534	→	2430
534	→	2450
534	→	2415
534	→	2857
534	→	2874
534	→	2820
534	→	2997
534	→	2751
534	→	570
534	→	3010
534	→	3107
2849	→	2415
1940	→	600
2770	→	1728
3050	→	2966
731	→	722
917	→	889
917	→	1785
128	→	119
128	→	1103
128	→	1789
745	→	722
1674	→	2314
1674	→	2364
1674	→	2914
1496	→	1404
263	→	556
263	→	998
1737	→	934
1529	→	1434
2367	→	1456
1406	→	937
271	→	2
271	→	1096
271	→	356
271	→	817
271	→	384
271	→	805
1463	→	1371
356	→	491
356	→	816
356	→	933
356	→	1093
338	→	290
860	→	3
860	→	960
860	→	197
860	→	889
860	→	932
860	→	1154
860	→	998
860	→	556
860	→	263
860	→	744
860	→	235
860	→	1683
860	→	2933
860	→	2960
860	→	2946
967	→	533
2268	→	1130
1117	→	2540
1117	→	2775
2641	→	998
2740	→	1728
2659	→	1119
98	→	1
98	→	600
98	→	664
98	→	888
98	→	647
98	→	916
98	→	621
98	→	2547
1624	→	1609
2181	→	491
2362	→	2832
2362	→	2883
214	→	186
214	→	742
897	→	3
897	→	1165
897	→	766
897	→	186
1475	→	2435
1475	→	2850
2525	→	600
1630	→	9
1989	→	420
1989	→	2199
1989	→	2259
2944	→	2933
1142	→	570
880	→	2279
10	→	253
10	→	1119
1166	→	1155
2196	→	664
2196	→	1
2196	→	934
2100	→	935
2100	→	2157
1691	→	1082
97	→	1746
97	→	1949
97	→	1976
2208	→	1063
2509	→	356
401	→	1325
401	→	1534
2198	→	2188
1248	→	9
2394	→	1655
2784	→	1728
851	→	270
1284	→	1417
2851	→	2415
571	→	6
571	→	320
571	→	1136
571	→	1104
571	→	1118
571	→	318
571	→	1094
571	→	338
571	→	1166
571	→	301
571	→	2776
743	→	722
2468	→	420
2549	→	600
561	→	531
1237	→	1387
1948	→	491
2363	→	119
383	→	1310
383	→	1521
1979	→	721
608	→	298
1209	→	623
1209	→	664
1209	→	797
1209	→	1940
1209	→	934
2647	→	1020
2396	→	1655
3082	→	1728
1993	→	420
1993	→	2201
1993	→	2263
2206	→	420
1977	→	721
3107	→	2415
167	→	119
167	→	1115
2902	→	492
1757	→	2514
1757	→	2560
1757	→	2582
3073	→	1573
472	→	1623
472	→	1631
2804	→	2415
1273	→	1407
502	→	931
502	→	1530
502	→	622
502	→	317
502	→	127
502	→	40
502	→	196
502	→	364
502	→	1
502	→	600
502	→	1790
502	→	2539
502	→	2541
119	→	262
119	→	562
119	→	968
119	→	1117
2434	→	420
2434	→	3009
2732	→	1728
145	→	119
145	→	1113
2517	→	600
299	→	1
299	→	664
299	→	934
299	→	623
299	→	2541
491	→	2932
491	→	2947
491	→	2996
491	→	3106
2369	→	1456
1724	→	1716
260	→	2078
18	→	1
18	→	600
18	→	664
18	→	916
18	→	621
18	→	623
1103	→	2538
1103	→	2769
2428	→	420
365	→	356
365	→	804
365	→	1089
365	→	2243
1141	→	1665
1141	→	1680
1141	→	2306
3125	→	600
1118	→	1104
41	→	9
41	→	420
41	→	1028
2260	→	1119
2047	→	2568
2047	→	2642
120	→	691
120	→	818
3	→	87
3	→	168
3	→	236
3	→	300
3	→	403
3	→	620
499	→	1595
499	→	1748
499	→	2275
1246	→	975
1104	→	1095
1104	→	525
1104	→	648
1104	→	335
1104	→	118
1104	→	8
1104	→	185
1104	→	355
1104	→	6
1104	→	879
1104	→	290
1104	→	1728
1104	→	2776
2278	→	1157
600	→	931
382	→	356
691	→	1167
691	→	1437
2156	→	1006
1102	→	966
817	→	796
1011	→	1727
1011	→	1935
2583	→	119
500	→	1
500	→	931
500	→	600
500	→	916
500	→	621
500	→	664
500	→	934
500	→	502
500	→	2539
500	→	2541
1114	→	1104
1531	→	1522
1995	→	796
1324	→	1311
1789	→	2714
1789	→	2899
2438	→	420
187	→	466
187	→	3
805	→	796
146	→	2449
146	→	2819
3111	→	2415
2252	→	11
298	→	1199
298	→	1247
298	→	1455
298	→	1475
298	→	1551
298	→	2397
2539	→	600
2683	→	1200
919	→	889
2049	→	960
2049	→	197
2049	→	3
2049	→	889
2049	→	932
2049	→	2933
2049	→	2960
2049	→	2946
9	→	89
9	→	464
9	→	1030
729	→	194
647	→	600
647	→	888
647	→	2159
5	→	66
5	→	166
5	→	234
5	→	289
5	→	401
5	→	599
774	→	260
147	→	119
147	→	1111
1200	→	1364
3010	→	570
671	→	1980
2685	→	1200
2966	→	934
698	→	499
598	→	570
1126	→	533
65	→	9
65	→	429
3065	→	1456
1454	→	1359
1055	→	2267
1027	→	194
1681	→	262
1681	→	1844
1681	→	2115
319	→	2546
319	→	2777
3040	→	1200
1618	→	931
1618	→	600
1618	→	623
1618	→	916
1618	→	621
1618	→	2541
1664	→	1096
1664	→	1082
3018	→	3041
1991	→	420
1991	→	2197
1991	→	2261
1134	→	570
2409	→	2398
973	→	1236
973	→	1466
381	→	1338
381	→	1536
2361	→	1457
1295	→	1284
2707	→	186
1110	→	966
90	→	1135
193	→	1740
193	→	2414
3185	→	570
1031	→	1020
1031	→	1725
473	→	1920
473	→	1988
473	→	2008
2989	→	1019
1068	→	97
2444	→	420
2007	→	119
2373	→	1573
1164	→	1155
2301	→	1200
1341	→	1311
2280	→	1157
1162	→	570
2523	→	600
1416	→	603
1758	→	1117
1758	→	562
1758	→	5
1758	→	262
1758	→	968
1758	→	119
1758	→	1682
1758	→	1522
1758	→	1539
1	→	40
1	→	127
1	→	196
1	→	317
1	→	364
1	→	622
3133	→	721
1936	→	600
2582	→	2842
2582	→	2889
1726	→	1716
2701	→	1456
1902	→	1136
1907	→	2393
1010	→	1957
1010	→	2881
2460	→	420
1776	→	494
2857	→	2415
2833	→	2415
690	→	297
2244	→	1097
2423	→	2676
2423	→	2678
2423	→	2690
2423	→	2692
2423	→	2706
2423	→	2797
2256	→	1105
977	→	4
977	→	1030
977	→	89
977	→	1127
977	→	852
977	→	291
977	→	464
977	→	9
977	→	1427
977	→	1311
977	→	1341
977	→	2466
977	→	2415
977	→	2804
1112	→	1104
127	→	2433
127	→	2856
127	→	2945
127	→	2959
1004	→	607
895	→	1947
895	→	1974
895	→	2205
601	→	1272
601	→	1497
601	→	2070
1994	→	2283
1994	→	2347
1994	→	2374
969	→	1775
570	→	1939
570	→	2751
2357	→	2344
1721	→	2300
1721	→	2308
1721	→	2358
1721	→	2362
1721	→	2370
1721	→	2406
1111	→	2548
1111	→	2783
2557	→	721
1938	→	600
1426	→	797
1478	→	119
1722	→	664
1722	→	1
1722	→	934
2424	→	502
2424	→	1790
2424	→	2539
2424	→	2541
2024	→	119
2841	→	2415
2990	→	3081
2990	→	3124
197	→	186
197	→	721
197	→	1163
428	→	298
2392	→	798
1934	→	356
1934	→	2251
426	→	2103
2503	→	420
723	→	2584
2084	→	886
1029	→	1020
1029	→	1723
402	→	356
402	→	795
402	→	1080
1522	→	1682
2748	→	1728
2812	→	2415
1790	→	502
2577	→	501
2577	→	3011
2972	→	931
2820	→	2415
1161	→	1986
261	→	1
261	→	916
261	→	931
261	→	600
261	→	621
261	→	664
261	→	934
2176	→	2943
2176	→	2957
2176	→	2998
2176	→	3104
235	→	186
235	→	744
235	→	1154
2776	→	1728
816	→	1294
816	→	1517
816	→	1587
2715	→	9
269	→	2105
2997	→	89
2997	→	3116
2250	→	1099
2746	→	1728
1654	→	533
1654	→	1126
1373	→	623
1373	→	664
1373	→	797
1373	→	1940
1373	→	934
2432	→	420
2533	→	600
2563	→	420
2563	→	2644
2563	→	2664
2214	→	1081
2941	→	3039
2941	→	3070
2941	→	3072
186	→	766
186	→	1165
186	→	2508
186	→	2562
2348	→	1456
2365	→	1456
540	→	532
493	→	1013
3029	→	1200
526	→	1005
526	→	2072
1339	→	1311
1921	→	356
3071	→	1456
976	→	1941
976	→	2745
1913	→	697
2730	→	2383
1322	→	1311
1322	→	2785
1311	→	1427
597	→	1742
597	→	2875
2692	→	3091
2692	→	3112
2677	→	1200
2677	→	3083
2071	→	883
1477	→	2441
1477	→	2840
6	→	8
6	→	118
6	→	185
6	→	335
6	→	355
6	→	648
2752	→	1728
2407	→	2398
2466	→	420
2569	→	2638
2798	→	8
2798	→	2901
2798	→	2965
2925	→	356
404	→	356
1539	→	1522
2693	→	119
2942	→	817
2942	→	805
1456	→	1655
88	→	9
88	→	420
88	→	4
88	→	1028
88	→	41
88	→	1427
88	→	1311
88	→	1322
88	→	2434
88	→	2415
88	→	2857
2106	→	931
823	→	497
3119	→	420
3119	→	3184
384	→	356
1351	→	693
2802	→	2415
3063	→	3048
1282	→	603
2458	→	420
2515	→	356
2200	→	2188
1293	→	797
2171	→	664
2171	→	1
2171	→	934
237	→	186
498	→	1907
498	→	2186
3027	→	2966
3115	→	421
2158	→	1007
363	→	259
336	→	290
336	→	2277
1297	→	1284
1168	→	1342
270	→	1221
270	→	1259
270	→	1464
270	→	1477
270	→	1540
270	→	1802
270	→	2372
270	→	2408
1987	→	420
1987	→	2257
67	→	9
67	→	448
67	→	1019
2274	→	570
2009	→	119
2894	→	186
2262	→	1119
1516	→	1424
301	→	290
301	→	2253
803	→	97
2025	→	2457
2025	→	2811
859	→	1744
859	→	1955
859	→	1978
2	→	64
2	→	146
2	→	215
2	→	337
2	→	383
2	→	663
2008	→	2451
2008	→	2817
1950	→	491
2195	→	2516
2195	→	2731
2411	→	2398
4	→	42
4	→	144
4	→	213
4	→	319
4	→	381
4	→	646
941	→	859
804	→	1283
804	→	1508
804	→	1572
1291	→	2382
2797	→	3017
2797	→	3055
2379	→	1609
118	→	2465
118	→	2803
2924	→	3028
2924	→	3064
449	→	421
2915	→	127
1018	→	773
2258	→	1119
2874	→	2415
1786	→	504
501	→	2708
501	→	2893
1222	→	1200
3121	→	420
188	→	1062
1666	→	1893
1666	→	2360
2709	→	9
1550	→	600
1550	→	623
1550	→	40
1550	→	196
1550	→	364
1550	→	622
1550	→	317
1550	→	127
1550	→	1
1814	→	1805
802	→	2025
802	→	2180
508	→	17
318	→	290
318	→	2255
1535	→	1522
2876	→	2415
2991	→	1104
1505	→	1414
16	→	1608
16	→	1629
2048	→	2473
2048	→	2554
2048	→	2556
2859	→	2415
2254	→	1105
421	→	684
421	→	1054
421	→	1692
887	→	859
795	→	1296
795	→	1519
795	→	1589
1094	→	1081
2531	→	600
2346	→	2122
2436	→	420
1915	→	1908
1915	→	2176
2884	→	420
2514	→	2684
2514	→	2700
357	→	591
2006	→	2443
2006	→	2834
1012	→	17
1012	→	1713
2023	→	2437
2023	→	2848
623	→	600
623	→	2099
2442	→	420
3117	→	421
2508	→	2682
2508	→	2698
2576	→	2924
2576	→	2988
1743	→	420
12	→	2249
1177	→	693
1436	→	934
2810	→	2415
169	→	119
1533	→	1522
3084	→	2400
1604	→	2600
2890	→	420
2327	→	1200
2639	→	998
672	→	194
2315	→	1311
1543	→	2207
2835	→	2415
1021	→	1738
2264	→	1119
1605	→	916
1605	→	931
1605	→	1
1605	→	600
1605	→	621
3090	→	8
1632	→	9
1958	→	420
621	→	600
621	→	916
2177	→	492
2585	→	819
2960	→	721
3105	→	2415
290	→	525
290	→	879
290	→	1095
2202	→	2188
1326	→	1311
126	→	96
2946	→	2933
2276	→	1155
1207	→	2729
2691	→	1456
216	→	186
216	→	730
2299	→	2122
1675	→	356
1675	→	1082
1675	→	1096
2900	→	186
2375	→	1573
1756	→	2376
1756	→	2378
1396	→	975
2786	→	2400
1745	→	420
1745	→	2271
1090	→	1081
1739	→	360
3113	→	420
1975	→	721
2290	→	2337
17	→	1933
17	→	1992
17	→	2006
1116	→	1104
2541	→	600
2160	→	1006
2699	→	1456
896	→	1914
896	→	1990
896	→	2023
1537	→	1522
1549	→	2522
1549	→	2739
2371	→	186
1361	→	724
1956	→	491
168	→	2459
168	→	2809
1260	→	9
2452	→	420
2643	→	491
1476	→	119
1933	→	2326
1933	→	2368
664	→	600
664	→	918
2405	→	1616
254	→	2043
858	→	2000
858	→	2161
2377	→	9
492	→	501
492	→	665
492	→	2990
1474	→	1394
320	→	290
320	→	648
320	→	335
320	→	118
320	→	8
320	→	185
320	→	355
320	→	6
320	→	1728
320	→	2778
2026	→	119
2307	→	1200
2309	→	9
722	→	844
722	→	1188
722	→	1446
2000	→	2467
2000	→	2801
2665	→	1119
1445	→	1349
465	→	421
1271	→	937
2601	→	889
649	→	600
3127	→	2933
422	→	535
422	→	768
932	→	889
932	→	960
932	→	1813
1741	→	420
2422	→	3089
2422	→	3120
2272	→	570
2426	→	2415
2450	→	420
2768	→	1728
2738	→	1728
1520	→	1509
474	→	5
474	→	1117
474	→	562
474	→	262
474	→	968
474	→	119
474	→	1682
474	→	1522
474	→	1539
195	→	1
195	→	600
195	→	623
195	→	916
195	→	621
195	→	664
195	→	934
1113	→	2530
1113	→	2753
2123	→	2524
2123	→	2747
1320	→	934
2843	→	2415
935	→	1261
935	→	1488
1942	→	600
2561	→	420
2561	→	2646
2561	→	2658
1518	→	1509
1908	→	1994
1908	→	2213
2901	→	3110
2901	→	3118
2901	→	3126
2901	→	3132
144	→	2429
144	→	2873
43	→	9
43	→	446
3092	→	2415
1552	→	186
194	→	1937
194	→	2737
2104	→	931
2999	→	89
2999	→	3114
767	→	722
767	→	2640
403	→	1323
403	→	1532
2679	→	9
447	→	421
2547	→	600
427	→	2410
427	→	2502
166	→	2431
166	→	2858
1702	→	770
1920	→	2320
1920	→	2366
1088	→	859
1803	→	2155
2359	→	1456
1850	→	532
1588	→	1573
1747	→	420
1747	→	2273
2284	→	1200
1590	→	1573
2882	→	2415
1123	→	1644
1981	→	420
1981	→	2265
2958	→	721
1465	→	1456
430	→	421
2120	→	2289
2120	→	2349
1061	→	260
2754	→	1728
1262	→	1397
1189	→	1352
2474	→	420
2474	→	2666
1914	→	2395
2266	→	1119
2667	→	570
291	→	852
291	→	1127
2001	→	119
355	→	1340
355	→	1538
1548	→	2425
1548	→	2427
2555	→	491
2321	→	1200
1808	→	895
1115	→	2532
1115	→	2767
1582	→	798
1₁(2642)	→	2643
1₁(1122)	→	1123
1₁(2914)	→	2915
1₁(3089)	→	3090
1₁(123)	→	124
1₁(556)	→	557
1₁(355)	→	356
1₁(424)	→	425
1₁(2120)	→	2121
1₁(934)	→	935
1₁(1804)	→	1805
1₁(563)	→	564
1₁(527)	→	528
1₁(1947)	→	1948
1₁(691)	→	692
1₁(1845)	→	1846
1₁(2257)	→	2258
1₁(2265)	→	2266
1₁(119)	→	120
1₁(381)	→	382
1₁(2161)	→	2162
1₁(1914)	→	1915
1₁(1081)	→	1082
1₁(360)	→	361
1₁(2797)	→	2798
1₁(9)	→	10
1₁(2658)	→	2659
1₁(2924)	→	2925
1₁(559)	→	560
1₁(2664)	→	2665
1₁(665)	→	666
1₁(1097)	→	1098
1₁(421)	→	422
1₁(2514)	→	2515
1₁(1596)	→	1597
1₁(1907)	→	1908
1₁(1005)	→	1006
1₁(2099)	→	2100
1₁(401)	→	402
1₁(935)	→	936
1₁(772)	→	773
1₁(1994)	→	1995
1₁(771)	→	772
1₁(1544)	→	1545
1₁(886)	→	887
1₁(1813)	→	1814
1₁(801)	→	802
1₁(1084)	→	1085
1₁(1095)	→	1096
1₁(1008)	→	1009
1₁(403)	→	404
1₁(1846)	→	1847
1₁(1101)	→	1102
1₁(364)	→	365
1₁(1107)	→	1108
1₁(383)	→	384
1₁(2159)	→	2160
1₁(1933)	→	1934
1₁(1157)	→	1158
1₁(795)	→	796
1₁(1949)	→	1950
1₁(560)	→	561
1₁(1920)	→	1921
1₁(1738)	→	1739
1₁(1955)	→	1956
1₁(2180)	→	2181
1₁(427)	→	428
1₁(2155)	→	2156
1₁(852)	→	853
1₁(601)	→	602
1₁(1002)	→	1003
1₁(816)	→	817
1₁(849)	→	850
1₁(90)	→	91
1₁(12)	→	13
1₁(2261)	→	2262
1₁(1721)	→	1722
1₁(298)	→	299
1₁(564)	→	565
1₁(894)	→	895
1₁(1063)	→	1064
1₁(770)	→	771
1₁(2554)	→	2555
1₁(536)	→	537
1₁(2569)	→	2570
1₁(1123)	→	1124
1₁(971)	→	972
1₁(605)	→	606
1₁(11)	→	12
1₁(2263)	→	2264
1₁(937)	→	938
1₁(1086)	→	1087
1₁(1055)	→	1056
1₁(1138)	→	1139
1₁(769)	→	770
1₁(1125)	→	1126
1₁(191)	→	192
1₁(1141)	→	1142
1₁(189)	→	190
1₁(1546)	→	1547
1₁(2118)	→	2119
1₁(722)	→	723
1₁(2508)	→	2509
1₁(1108)	→	1109
1₁(804)	→	805
1₁(2259)	→	2260
1₁(1059)	→	1060
1₁(359)	→	360
1₁(270)	→	271
1₁(973)	→	974
1₁(591)	→	592
1₁(1909)	→	1910
1₂(1894)	→	1895
1₂(1690)	→	1691
1₂(2419)	→	2420
1₂(1526)	→	1527
1₂(1203)	→	1204
1₂(3020)	→	3021
1₂(2406)	→	2407
1₂(1286)	→	1287
1₂(2939)	→	2940
1₂(1191)	→	1192
1₂(2423)	→	2424
1₂(2410)	→	2411
1₂(1513)	→	1514
1₂(2401)	→	2402
1₂(1284)	→	1285
1₂(1365)	→	1366
1₂(1311)	→	1312
1₂(1509)	→	1510
1₂(2408)	→	2409
1₂(2360)	→	2361
1₂(1663)	→	1664
1₂(1168)	→	1169
1₂(1388)	→	1389
1₂(1701)	→	1702
1₂(1237)	→	1238
1₂(1265)	→	1266
1₂(1502)	→	1503
1₂(1353)	→	1354
1₂(1471)	→	1472
1₂(1674)	→	1675
1₂(1171)	→	1172
1₂(1202)	→	1203
1₂(1189)	→	1190
1₂(1895)	→	1896
1₂(2292)	→	2293
1₂(2293)	→	2294
1₂(2422)	→	2423
1₂(2402)	→	2403
1₂(1578)	→	1579
1₂(1408)	→	1409
1₂(1460)	→	1461
1₂(1451)	→	1452
1₂(2941)	→	2942
1₂(1313)	→	1314
1₂(1736)	→	1737
1₂(2350)	→	2351
1₂(2338)	→	2339
1₂(3060)	→	3061
1₂(1343)	→	1344
1₂(3018)	→	3019
1₂(1489)	→	1490
1₂(1576)	→	1577
1₂(1192)	→	1193
1₂(2397)	→	2398
1₂(1262)	→	1263
1₂(1498)	→	1499
1₂(1456)	→	1457
1₂(1653)	→	1654
1₂(2290)	→	2291
1₂(2416)	→	2417
1₂(1287)	→	1288
1₂(1240)	→	1241
1₂(1398)	→	1399
1₂(2383)	→	2384
1₂(1200)	→	1201
1₂(1239)	→	1240
1₂(1276)	→	1277
1₂(1314)	→	1315
1₂(3021)	→	3022
1₂(1442)	→	1443
1₂(1609)	→	1610
1₂(1273)	→	1274
1₂(1418)	→	1419
1₂(1467)	→	1468
1₂(1264)	→	1265
1₂(1275)	→	1276
1₂(1428)	→	1429
1₂(1438)	→	1439
1₂(1493)	→	1494
1₂(1170)	→	1171
1₂(1447)	→	1448
1₂(2354)	→	2355
1₂(3056)	→	3057
1₂(1522)	→	1523
1₂(3042)	→	3043
3₂(1696)	→	1697
3₂(2801)	→	2802
3₂(1367)	→	1368
3₂(1268)	→	1269
3₂(1669)	→	1670
3₂(2339)	→	2340
3₂(2881)	→	2882
3₂(2425)	→	2426
3₂(1575)	→	1576
3₂(2352)	→	2353
3₂(1732)	→	1733
3₂(1354)	→	1355
3₂(1399)	→	1400
3₂(1236)	→	1237
3₂(1387)	→	1388
3₂(1685)	→	1686
3₂(1167)	→	1168
3₂(2819)	→	2820
3₂(2729)	→	2730
3₂(1400)	→	1401
3₂(2676)	→	2677
3₂(1614)	→	1615
3₂(1288)	→	1289
3₂(1241)	→	1242
3₂(1321)	→	1322
3₂(3044)	→	3045
3₂(1283)	→	1284
3₂(1261)	→	1262
3₂(1469)	→	1470
3₂(1195)	→	1196
3₂(2850)	→	2851
3₂(1193)	→	1194
3₂(1430)	→	1431
3₂(2378)	→	2379
3₂(1672)	→	1673
3₂(2314)	→	2315
3₂(2858)	→	2859
3₂(1188)	→	1189
3₂(1667)	→	1668
3₂(2289)	→	2290
3₂(2684)	→	2685
3₂(1608)	→	1609
3₂(1315)	→	1316
3₂(1277)	→	1278
3₂(1355)	→	1356
3₂(1389)	→	1390
3₂(2840)	→	2841
3₂(3058)	→	3059
3₂(1340)	→	1341
3₂(2817)	→	2818
3₂(3041)	→	3042
3₂(1243)	→	1244
3₂(1427)	→	1428
3₂(2803)	→	2804
3₂(1221)	→	1222
3₂(1323)	→	1324
3₂(2811)	→	2812
3₂(2388)	→	2389
3₂(3028)	→	3029
3₂(2326)	→	2327
3₂(2320)	→	2321
3₂(1429)	→	1430
3₂(1272)	→	1273
3₂(2340)	→	2341
3₂(1174)	→	1175
3₂(2382)	→	2383
3₂(1658)	→	1659
3₂(1344)	→	1345
3₂(2842)	→	2843
3₂(3106)	→	3107
3₂(1290)	→	1291
3₂(1266)	→	1267
3₂(2873)	→	2874
3₂(1204)	→	1205
3₂(2414)	→	2415
3₂(3110)	→	3111
3₂(1342)	→	1343
3₂(1366)	→	1367
3₂(1688)	→	1689
3₂(1511)	→	1512
3₂(1646)	→	1647
3₂(2283)	→	2284
3₂(1172)	→	1173
3₂(1458)	→	1459
3₂(1407)	→	1408
3₂(3104)	→	3105
3₂(1325)	→	1326
3₂(1524)	→	1525
3₂(2300)	→	2301
3₂(1310)	→	1311
3₂(2337)	→	2338
3₂(1500)	→	1501
3₂(1900)	→	1901
3₂(1279)	→	1280
3₂(1617)	→	1618
3₂(1390)	→	1391
3₂(2834)	→	2835
3₂(2875)	→	2876
3₂(3091)	→	3092
3₂(2682)	→	2683
3₂(1491)	→	1492
3₂(1734)	→	1735
3₂(1294)	→	1295
3₂(3022)	→	3023
3₂(1397)	→	1398
3₂(1648)	→	1649
3₂(1364)	→	1365
3₂(1345)	→	1346
3₂(1296)	→	1297
3₂(1699)	→	1700
3₂(1409)	→	1410
3₂(2938)	→	2939
3₂(2848)	→	2849
3₂(2294)	→	2295
3₂(1419)	→	1420
3₂(2296)	→	2297
3₂(2306)	→	2307
3₂(1317)	→	1318
3₂(1417)	→	1418
3₂(1728)	→	1729
3₂(3017)	→	3018
3₂(1199)	→	1200
3₂(1449)	→	1450
3₂(1206)	→	1207
3₂(1651)	→	1652
3₂(2856)	→	2857
3₂(2398)	→	2399
3₂(1338)	→	1339
3₂(3024)	→	3025
3₂(3043)	→	3044
3₂(1656)	→	1657
3₂(1683)	→	1684
3₂(3039)	→	3040
3₂(1420)	→	1421
3₂(1661)	→	1662
3₂(1410)	→	1411
3₂(1352)	→	1353
3₂(2391)	→	2392
3₂(1440)	→	1441
3₂(2809)	→	2810
3₂(1694)	→	1695
3₂(2832)	→	2833
3₂(1623)	→	1624
5₂(2767)	→	2768
5₂(1898)	→	1899
5₂(1662)	→	1663
5₂(1581)	→	1582
5₂(2745)	→	2746
5₂(2769)	→	2770
5₂(1652)	→	1653
5₂(1689)	→	1690
5₂(2737)	→	2738
5₂(2783)	→	2784
5₂(2775)	→	2776
5₂(2751)	→	2752
5₂(1700)	→	1701
5₂(2753)	→	2754
5₂(2935)	→	2936
5₂(2421)	→	2422
5₂(2731)	→	2732
5₂(2777)	→	2778
5₂(1901)	→	1902
5₂(2404)	→	2405
5₂(2747)	→	2748
5₂(3081)	→	3082
5₂(1727)	→	1728
5₂(2739)	→	2740
5₂(1673)	→	1674
0₁(1001)	→	1002
0₁(1935)	→	1936
0₁(2971)	→	2972
0₁(970)	→	971
0₁(2524)	→	2525
0₁(1130)	→	1131
0₁(2538)	→	2539
0₁(295)	→	296
0₁(2540)	→	2541
0₁(2045)	→	2046
0₁(696)	→	697
0₁(856)	→	857
0₁(974)	→	975
0₁(663)	→	664
0₁(2532)	→	2533
0₁(1937)	→	1938
0₁(936)	→	937
0₁(2207)	→	2208
0₁(525)	→	526
0₁(1718)	→	1719
0₁(558)	→	559
0₁(2516)	→	2517
0₁(506)	→	507
0₁(1058)	→	1059
0₁(2166)	→	2167
0₁(728)	→	729
0₁(2190)	→	2191
0₁(622)	→	623
0₁(472)	→	473
0₁(620)	→	621
0₁(880)	→	881
0₁(1602)	→	1603
0₁(965)	→	966
0₁(2081)	→	2082
0₁(646)	→	647
0₁(1062)	→	1063
0₁(2105)	→	2106
0₁(1603)	→	1604
0₁(599)	→	600
0₁(2546)	→	2547
0₁(2965)	→	2966
0₁(264)	→	265
0₁(1789)	→	1790
0₁(2522)	→	2523
0₁(2121)	→	2122
0₁(1000)	→	1001
0₁(259)	→	260
0₁(891)	→	892
0₁(496)	→	497
0₁(539)	→	540
0₁(2117)	→	2118
0₁(2530)	→	2531
0₁(1131)	→	1132
0₁(1939)	→	1940
0₁(602)	→	603
0₁(2103)	→	2104
0₁(258)	→	259
0₁(1756)	→	1757
0₁(596)	→	597
0₁(648)	→	649
0₁(3124)	→	3125
0₁(122)	→	123
0₁(1133)	→	1134
0₁(499)	→	500
0₁(2548)	→	2549
0₁(723)	→	724
0₁(1015)	→	1016
0₁(1132)	→	1133
0₁(796)	→	797
0₁(962)	→	963
0₁(501)	→	502
0₁(1022)	→	1023
0₁(1802)	→	1803
0₁(1941)	→	1942
0₁(797)	→	798
0₁(692)	→	693
0₁(16)	→	17
0₁(933)	→	934
4₀(3)	→	5
4₀(6)	→	5
4₀(5)	→	5
4₀(4)	→	5
4₀(2)	→	5
4₀(1)	→	5
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
0₂(1318)	→	1319
0₂(1615)	→	1616
0₂(1647)	→	1648
0₂(2389)	→	2390
0₂(1684)	→	1685
0₂(1733)	→	1734
0₂(1280)	→	1281
0₂(1459)	→	1460
0₂(2353)	→	2354
0₂(1441)	→	1442
0₂(3059)	→	3060
0₂(1175)	→	1176
0₂(1291)	→	1292
0₂(1657)	→	1658
0₂(1450)	→	1451
0₂(1196)	→	1197
0₂(1668)	→	1669
0₂(2390)	→	2391
0₂(3025)	→	3026
0₂(1269)	→	1270
0₂(1512)	→	1513
0₂(1616)	→	1617
0₂(1470)	→	1471
0₂(1525)	→	1526
0₂(1695)	→	1696
0₂(1492)	→	1493
0₂(2297)	→	2298
0₂(1244)	→	1245
0₂(1207)	→	1208
0₂(1501)	→	1502
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
5₁(882)	→	883
5₁(1155)	→	1156
5₁(1549)	→	1550
5₁(667)	→	668
5₁(1849)	→	1850
5₁(1080)	→	1081
5₁(362)	→	363
5₁(3011)	→	3012
5₁(335)	→	336
5₁(2070)	→	2071
5₁(2194)	→	2195
5₁(1067)	→	1068
5₁(689)	→	690
5₁(1009)	→	1010
5₁(687)	→	688
5₁(1165)	→	1166
5₁(269)	→	270
5₁(2123)	→	2124
5₁(821)	→	822
5₁(467)	→	468
5₁(1089)	→	1090
5₁(2213)	→	2214
5₁(1017)	→	1018
5₁(2079)	→	2080
5₁(688)	→	689
5₁(1751)	→	1752
5₁(1026)	→	1027
5₁(194)	→	195
5₁(1093)	→	1094
5₁(1111)	→	1112
5₁(289)	→	290
5₁(319)	→	320
5₁(1117)	→	1118
5₁(1163)	→	1164
5₁(879)	→	880
5₁(2573)	→	2574
5₁(1103)	→	1104
5₁(2080)	→	2081
5₁(1154)	→	1155
5₁(538)	→	539
5₁(969)	→	970
5₁(2189)	→	2190
5₁(998)	→	999
5₁(1911)	→	1912
5₁(1115)	→	1116
5₁(889)	→	890
5₁(2168)	→	2169
5₁(593)	→	594
5₁(300)	→	301
5₁(727)	→	728
5₁(890)	→	891
5₁(1021)	→	1022
5₁(2275)	→	2276
5₁(2990)	→	2991
5₁(999)	→	1000
5₁(2116)	→	2117
5₁(1113)	→	1114
5₁(557)	→	558
5₁(495)	→	496
5₁(1066)	→	1067
5₁(1124)	→	1125
5₁(570)	→	571
5₁(426)	→	427
5₁(2195)	→	2196
5₁(337)	→	338
5₁(1011)	→	1012
5₁(1106)	→	1107
5₁(768)	→	769
5₁(1135)	→	1136
5₁(845)	→	846
5₁(317)	→	318
5₁(567)	→	568
5₁(976)	→	977
2₁(267)	→	268
2₁(502)	→	503
2₁(2576)	→	2577
2₁(960)	→	961
2₁(1541)	→	1542
2₁(568)	→	569
2₁(262)	→	263
2₁(2600)	→	2601
2₁(1910)	→	1911
2₁(1096)	→	1097
2₁(606)	→	607
2₁(236)	→	237
2₁(2640)	→	2641
2₁(1100)	→	1101
2₁(93)	→	94
2₁(671)	→	672
2₁(2646)	→	2647
2₁(2251)	→	2252
2₁(1754)	→	1755
2₁(1748)	→	1749
2₁(2556)	→	2557
2₁(2370)	→	2371
2₁(532)	→	533
2₁(1121)	→	1122
2₁(1128)	→	1129
2₁(888)	→	889
2₁(592)	→	593
2₁(603)	→	604
2₁(185)	→	186
2₁(1805)	→	1806
2₁(893)	→	894
2₁(1974)	→	1975
2₁(1599)	→	1600
2₁(2197)	→	2198
2₁(2947)	→	2948
2₁(802)	→	803
2₁(1016)	→	1017
2₁(1803)	→	1804
2₁(361)	→	362
2₁(526)	→	527
2₁(95)	→	96
2₁(2191)	→	2192
2₁(2199)	→	2200
2₁(466)	→	467
2₁(1140)	→	1141
2₁(1752)	→	1753
2₁(800)	→	801
2₁(2279)	→	2280
2₁(1551)	→	1552
2₁(939)	→	940
2₁(2169)	→	2170
2₁(2167)	→	2168
2₁(896)	→	897
2₁(2638)	→	2639
2₁(2201)	→	2202
2₁(1749)	→	1750
2₁(686)	→	687
2₁(497)	→	498
2₁(2243)	→	2244
2₁(215)	→	216
2₁(916)	→	917
2₁(2164)	→	2165
2₁(2706)	→	2707
2₁(186)	→	187
2₁(1085)	→	1086
2₁(213)	→	214
2₁(2044)	→	2045
2₁(192)	→	193
2₁(724)	→	725
2₁(1054)	→	1055
2₁(504)	→	505
2₁(2082)	→	2083
2₁(470)	→	471
2₁(1547)	→	1548
2₁(1757)	→	1758
2₁(1156)	→	1157
2₁(256)	→	257
2₁(2277)	→	2278
2₁(2893)	→	2894
2₁(1020)	→	1021
2₁(358)	→	359
2₁(855)	→	856
2₁(725)	→	726
2₁(357)	→	358
2₁(2957)	→	2958
2₁(3132)	→	3133
2₁(473)	→	474
2₁(2959)	→	2960
2₁(1056)	→	1057
2₁(1714)	→	1715
2₁(850)	→	851
2₁(2644)	→	2645
2₁(2188)	→	2189
2₁(2083)	→	2084
2₁(1750)	→	1751
2₁(1161)	→	1162
2₁(1600)	→	1601
2₁(666)	→	667
2₁(423)	→	424
2₁(124)	→	125
2₁(291)	→	292
2₁(255)	→	256
2₁(918)	→	919
2₁(529)	→	530
2₁(892)	→	893
2₁(498)	→	499
2₁(1598)	→	1599
2₁(1160)	→	1161
2₁(1978)	→	1979
2₁(2047)	→	2048
2₁(858)	→	859
2₁(1028)	→	1029
2₁(2078)	→	2079
2₁(10)	→	11
2₁(196)	→	197
2₁(1030)	→	1031
2₁(234)	→	235
2₁(1007)	→	1008
2₁(17)	→	18
2₁(1540)	→	1541
2₁(2575)	→	2576
2₁(1013)	→	1014
2₁(2899)	→	2900
2₁(254)	→	255
2₁(468)	→	469
2₁(1023)	→	1024
2₁(1806)	→	1807
2₁(1019)	→	1020
2₁(1976)	→	1977
2₁(2187)	→	2188
2₁(931)	→	932
2₁(773)	→	774
2₁(528)	→	529
1₀(3)	→	2
1₀(5)	→	2
1₀(2)	→	2
1₀(4)	→	2
1₀(1)	→	2
1₀(6)	→	2
2₀(2)	→	3
2₀(4)	→	3
2₀(3)	→	3
2₀(6)	→	3
2₀(1)	→	3
2₀(5)	→	3
3₁(92)	→	93
3₁(1601)	→	1602
3₁(2437)	→	2438
3₁(2467)	→	2468
3₁(1099)	→	1100
3₁(2435)	→	2436
3₁(2473)	→	2474
3₁(2443)	→	2444
3₁(2449)	→	2450
3₁(1247)	→	1248
3₁(40)	→	41
3₁(694)	→	695
3₁(257)	→	258
3₁(530)	→	531
3₁(885)	→	886
3₁(2193)	→	2194
3₁(595)	→	596
3₁(670)	→	671
3₁(1129)	→	1130
3₁(2666)	→	2667
3₁(1755)	→	1756
3₁(3184)	→	3185
3₁(1025)	→	1026
3₁(492)	→	493
3₁(263)	→	264
3₁(13)	→	14
3₁(2431)	→	2432
3₁(607)	→	608
3₁(975)	→	976
3₁(15)	→	16
3₁(290)	→	291
3₁(964)	→	965
3₁(1990)	→	1991
3₁(966)	→	967
3₁(1986)	→	1987
3₁(2186)	→	2187
3₁(2574)	→	2575
3₁(695)	→	696
3₁(2163)	→	2164
3₁(2708)	→	2709
3₁(471)	→	472
3₁(1629)	→	1630
3₁(1992)	→	1993
3₁(2457)	→	2458
3₁(1595)	→	1596
3₁(697)	→	698
3₁(848)	→	849
3₁(2998)	→	2999
3₁(2678)	→	2679
3₁(89)	→	90
3₁(533)	→	534
3₁(1543)	→	1544
3₁(8)	→	9
3₁(2119)	→	2120
3₁(2502)	→	2503
3₁(1631)	→	1632
3₁(1083)	→	1084
3₁(356)	→	357
3₁(1065)	→	1066
3₁(2988)	→	2989
3₁(2427)	→	2428
3₁(2459)	→	2460
3₁(121)	→	122
3₁(294)	→	295
3₁(505)	→	506
3₁(507)	→	508
3₁(2883)	→	2884
3₁(188)	→	189
3₁(2376)	→	2377
3₁(87)	→	88
3₁(822)	→	823
3₁(1988)	→	1989
3₁(2433)	→	2434
3₁(1139)	→	1140
3₁(1807)	→	1808
3₁(66)	→	67
3₁(1109)	→	1110
3₁(2714)	→	2715
3₁(3118)	→	3119
3₁(2560)	→	2561
3₁(2996)	→	2997
3₁(2451)	→	2452
3₁(2115)	→	2116
3₁(961)	→	962
3₁(883)	→	884
3₁(1717)	→	1718
3₁(268)	→	269
3₁(1957)	→	1958
3₁(2584)	→	2585
3₁(1259)	→	1260
3₁(1980)	→	1981
3₁(1740)	→	1741
3₁(2441)	→	2442
3₁(296)	→	297
3₁(2170)	→	2171
3₁(1604)	→	1605
3₁(2562)	→	2563
3₁(1713)	→	1714
3₁(1087)	→	1088
3₁(884)	→	885
3₁(265)	→	266
3₁(963)	→	964
3₁(1119)	→	1120
3₁(2271)	→	2272
3₁(1060)	→	1061
3₁(569)	→	570
3₁(91)	→	92
3₁(2205)	→	2206
3₁(535)	→	536
3₁(1719)	→	1720
3₁(3112)	→	3113
3₁(2267)	→	2268
3₁(1908)	→	1909
3₁(972)	→	973
3₁(2889)	→	2890
3₁(2273)	→	2274
3₁(64)	→	65
3₁(2122)	→	2123
3₁(2249)	→	2250
3₁(3120)	→	3121
3₁(42)	→	43
3₁(2429)	→	2430
3₁(260)	→	261
3₁(818)	→	819
3₁(693)	→	694
3₁(2308)	→	2309
3₁(1746)	→	1747
3₁(1098)	→	1099
3₁(3009)	→	3010
3₁(2570)	→	2571
3₁(968)	→	969
3₁(2465)	→	2466
3₁(1742)	→	1743
3₁(1744)	→	1745
4₁(669)	→	670
4₁(2568)	→	2569
4₁(685)	→	686
4₁(3114)	→	3115
4₁(2000)	→	2001
4₁(266)	→	267
4₁(469)	→	470
4₁(2072)	→	2073
4₁(820)	→	821
4₁(819)	→	820
4₁(766)	→	767
4₁(2253)	→	2254
4₁(187)	→	188
4₁(190)	→	191
4₁(1542)	→	1543
4₁(1014)	→	1015
4₁(940)	→	941
4₁(857)	→	858
4₁(600)	→	601
4₁(1775)	→	1776
4₁(597)	→	598
4₁(448)	→	449
4₁(420)	→	421
4₁(859)	→	860
4₁(2043)	→	2044
4₁(798)	→	799
4₁(2046)	→	2047
4₁(1844)	→	1845
4₁(2572)	→	2573
4₁(1003)	→	1004
4₁(503)	→	504
4₁(1127)	→	1128
4₁(494)	→	495
4₁(2571)	→	2572
4₁(1064)	→	1065
4₁(1104)	→	1105
4₁(422)	→	423
4₁(293)	→	294
4₁(854)	→	855
4₁(2048)	→	2049
4₁(537)	→	538
4₁(144)	→	145
4₁(730)	→	731
4₁(2157)	→	2158
4₁(2176)	→	2177
4₁(1082)	→	1083
4₁(97)	→	98
4₁(566)	→	567
4₁(1725)	→	1726
4₁(1848)	→	1849
4₁(1158)	→	1159
4₁(96)	→	97
4₁(2255)	→	2256
4₁(1753)	→	1754
4₁(847)	→	848
4₁(895)	→	896
4₁(668)	→	669
4₁(604)	→	605
4₁(1680)	→	1681
4₁(799)	→	800
4₁(14)	→	15
4₁(1720)	→	1721
4₁(594)	→	595
4₁(429)	→	430
4₁(193)	→	194
4₁(125)	→	126
4₁(425)	→	426
4₁(292)	→	293
4₁(844)	→	845
4₁(1024)	→	1025
4₁(118)	→	119
4₁(493)	→	494
4₁(1120)	→	1121
4₁(1105)	→	1106
4₁(2162)	→	2163
4₁(120)	→	121
4₁(168)	→	169
4₁(1723)	→	1724
4₁(2165)	→	2166
4₁(1057)	→	1058
4₁(938)	→	939
4₁(742)	→	743
4₁(3116)	→	3117
4₁(2025)	→	2026
4₁(2008)	→	2009
4₁(846)	→	847
4₁(464)	→	465
4₁(565)	→	566
4₁(491)	→	492
4₁(94)	→	95
4₁(562)	→	563
4₁(1847)	→	1848
4₁(1548)	→	1549
4₁(2692)	→	2693
4₁(297)	→	298
4₁(166)	→	167
4₁(146)	→	147
4₁(1159)	→	1160
4₁(1136)	→	1137
4₁(726)	→	727
4₁(1716)	→	1717
4₁(2362)	→	2363
4₁(127)	→	128
4₁(1597)	→	1598
4₁(2901)	→	2902
4₁(721)	→	722
4₁(2006)	→	2007
4₁(684)	→	685
4₁(744)	→	745
4₁(881)	→	882
4₁(1010)	→	1011
4₁(1785)	→	1786
4₁(1912)	→	1913
4₁(853)	→	854
4₁(1137)	→	1138
4₁(1477)	→	1478
4₁(2582)	→	2583
4₁(446)	→	447
4₁(2023)	→	2024
4₁(1475)	→	1476
4₁(1545)	→	1546
4₁(253)	→	254
4₁(531)	→	532
4₁(2192)	→	2193
4₁(1715)	→	1716
4₁(1006)	→	1007
4₂(1437)	→	1438
4₂(1515)	→	1516
4₂(1432)	→	1433
4₂(1536)	→	1537
4₂(1446)	→	1447
4₂(1735)	→	1736
4₂(1488)	→	1489
4₂(1360)	→	1361
4₂(2366)	→	2367
4₂(1414)	→	1415
4₂(1577)	→	1578
4₂(1497)	→	1498
4₂(2345)	→	2346
4₂(1538)	→	1539
4₂(1395)	→	1396
4₂(1504)	→	1505
4₂(1369)	→	1370
4₂(1517)	→	1518
4₂(1371)	→	1372
4₂(1405)	→	1406
4₂(3055)	→	3056
4₂(2420)	→	2421
4₂(3057)	→	3058
4₂(2417)	→	2418
4₂(1532)	→	1533
4₂(1490)	→	1491
4₂(2415)	→	2416
4₂(1692)	→	1693
4₂(1528)	→	1529
4₂(1644)	→	1645
4₂(1499)	→	1500
4₂(1665)	→	1666
4₂(1316)	→	1317
4₂(1457)	→	1458
4₂(1404)	→	1405
4₂(2933)	→	2934
4₂(1439)	→	1440
4₂(2342)	→	2343
4₂(1194)	→	1195
4₂(1357)	→	1358
4₂(1534)	→	1535
4₂(3062)	→	3063
4₂(1347)	→	1348
4₂(1435)	→	1436
4₂(1574)	→	1575
4₂(1659)	→	1660
4₂(1897)	→	1898
4₂(1521)	→	1522
4₂(2347)	→	2348
4₂(1697)	→	1698
4₂(1455)	→	1456
4₂(1205)	→	1206
4₂(1394)	→	1395
4₂(2690)	→	2691
4₂(2358)	→	2359
4₂(1424)	→	1425
4₂(1686)	→	1687
4₂(1402)	→	1403
4₂(1468)	→	1469
4₂(2344)	→	2345
4₂(3046)	→	3047
4₂(2295)	→	2296
4₂(1415)	→	1416
4₂(2698)	→	2699
4₂(3049)	→	3050
4₂(1730)	→	1731
4₂(1464)	→	1465
4₂(2384)	→	2385
4₂(2349)	→	2350
4₂(2351)	→	2352
4₂(1896)	→	1897
4₂(3023)	→	3024
4₂(1289)	→	1290
4₂(1519)	→	1520
4₂(1731)	→	1732
4₂(1510)	→	1511
4₂(1530)	→	1531
4₂(1649)	→	1650
4₂(1444)	→	1445
4₂(1267)	→	1268
4₂(1278)	→	1279
4₂(1242)	→	1243
4₂(1462)	→	1463
4₂(1473)	→	1474
4₂(2356)	→	2357
4₂(2364)	→	2365
4₂(1359)	→	1360
4₂(3048)	→	3049
4₂(1580)	→	1581
4₂(1495)	→	1496
4₂(1392)	→	1393
4₂(2936)	→	2937
4₂(3070)	→	3071
4₂(1453)	→	1454
4₂(1412)	→	1413
4₂(1372)	→	1373
4₂(2700)	→	2701
4₂(1350)	→	1351
4₂(1893)	→	1894
4₂(2395)	→	2396
4₂(1425)	→	1426
4₂(1434)	→	1435
4₂(3064)	→	3065
4₂(2934)	→	2935
4₂(1523)	→	1524
4₂(1466)	→	1467
4₂(1610)	→	1611
4₂(2937)	→	2938
4₂(1508)	→	1509
4₂(1670)	→	1671
4₂(1173)	→	1174
4₂(1422)	→	1423
4₂(2368)	→	2369
4₂(2393)	→	2394
4₂(1349)	→	1350
4₂(1448)	→	1449
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
2₂(1698)	→	1699
2₂(1729)	→	1730
2₂(1527)	→	1528
2₂(1281)	→	1282
2₂(1682)	→	1683
2₂(1393)	→	1394
2₂(2400)	→	2401
2₂(1655)	→	1656
2₂(3126)	→	3127
2₂(1176)	→	1177
2₂(1613)	→	1614
2₂(1494)	→	1495
2₂(1201)	→	1202
2₂(1687)	→	1688
2₂(3083)	→	3084
2₂(1391)	→	1392
2₂(3061)	→	3062
2₂(2399)	→	2400
2₂(1274)	→	1275
2₂(2945)	→	2946
2₂(1660)	→	1661
2₂(1514)	→	1515
2₂(1413)	→	1414
2₂(1169)	→	1170
2₂(1503)	→	1504
2₂(1587)	→	1588
2₂(1693)	→	1694
2₂(1285)	→	1286
2₂(2341)	→	2342
2₂(1263)	→	1264
2₂(1899)	→	1900
2₂(1358)	→	1359
2₂(2943)	→	2944
2₂(1270)	→	1271
2₂(1612)	→	1613
2₂(1645)	→	1646
2₂(3072)	→	3073
2₂(1368)	→	1369
2₂(2386)	→	2387
2₂(2372)	→	2373
2₂(2418)	→	2419
2₂(2343)	→	2344
2₂(1356)	→	1357
2₂(1666)	→	1667
2₂(2355)	→	2356
2₂(1671)	→	1672
2₂(2374)	→	2375
2₂(1401)	→	1402
2₂(1197)	→	1198
2₂(1431)	→	1432
2₂(1319)	→	1320
2₂(2785)	→	2786
2₂(3019)	→	3020
2₂(1452)	→	1453
2₂(1433)	→	1434
2₂(1312)	→	1313
2₂(1411)	→	1412
2₂(1650)	→	1651
2₂(1572)	→	1573
2₂(1611)	→	1612
2₂(3045)	→	3046
2₂(1423)	→	1424
2₂(1573)	→	1574
2₂(3026)	→	3027
2₂(1403)	→	1404
2₂(3047)	→	3048
2₂(1190)	→	1191
2₂(1443)	→	1444
2₂(1346)	→	1347
2₂(1421)	→	1422
2₂(1245)	→	1246
2₂(1348)	→	1349
2₂(1370)	→	1371
2₂(1238)	→	1239
2₂(1579)	→	1580
2₂(2940)	→	2941
2₂(2291)	→	2292
2₂(1292)	→	1293
2₂(2403)	→	2404
2₂(1589)	→	1590
2₂(1461)	→	1462
2₂(2387)	→	2388
2₂(1208)	→	1209
2₂(2932)	→	2933
2₂(2385)	→	2386
2₂(2298)	→	2299
2₂(1472)	→	1473

The automaton is closed under rewriting as it is compatible.