Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4964)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{6, 5, 4, 3, 2, 1}

transitions:

2207	→	1850
730	→	1029
730	→	1960
1067	→	5
1067	→	859
1067	→	629
1067	→	855
1067	→	590
1067	→	1100
1067	→	188
1067	→	821
1067	→	199
1067	→	1231
1067	→	259
1067	→	2295
1067	→	2376
1067	→	2324
854	→	846
2441	→	512
1659	→	1109
1659	→	775
1659	→	811
1659	→	742
1659	→	449
1659	→	138
1659	→	65
1659	→	217
1659	→	700
1659	→	2
1659	→	679
1659	→	689
239	→	188
239	→	269
239	→	853
3086	→	412
2042	→	1013
1301	→	335
1301	→	1950
1301	→	2075
793	→	1162
429	→	404
429	→	465
429	→	861
899	→	1
899	→	1099
899	→	810
899	→	729
899	→	749
899	→	2648
1525	→	2383
869	→	1262
869	→	1300
869	→	1377
869	→	1482
1287	→	1099
1287	→	810
1287	→	1
1287	→	729
1287	→	743
3078	→	2384
818	→	412
1859	→	1099
1859	→	810
1859	→	1
1859	→	729
1859	→	749
1859	→	2648
2722	→	1022
2956	→	729
1437	→	680
1437	→	1177
1437	→	879
1437	→	575
1437	→	1173
1437	→	795
1437	→	404
1437	→	492
1437	→	877
1437	→	450
1437	→	2384
1437	→	2414
315	→	1885
2558	→	2530
2921	→	811
745	→	729
1674	→	2241
1257	→	1099
1257	→	810
1257	→	1
1257	→	729
1257	→	743
2046	→	1013
830	→	822
589	→	15
1057	→	869
2714	→	17
3123	→	958
1762	→	629
860	→	846
860	→	2189
791	→	1290
791	→	1569
791	→	1860
791	→	1891
1117	→	1783
3039	→	2739
1156	→	2674
1156	→	2727
658	→	1942
98	→	17
794	→	784
897	→	1247
897	→	1292
897	→	1691
897	→	2354
897	→	2599
286	→	260
1989	→	973
2944	→	890
874	→	862
874	→	1617
880	→	862
1142	→	1131
1142	→	2271
809	→	784
2905	→	2453
2908	→	3075
387	→	2003
387	→	2565
1261	→	1248
1261	→	1988
1261	→	2106
1557	→	811
97	→	1990
3054	→	2979
2620	→	845
2995	→	2972
1546	→	335
1284	→	2651
1284	→	2963
743	→	729
743	→	2033
2728	→	89
1794	→	845
2468	→	404
561	→	513
561	→	916
448	→	404
448	→	490
448	→	783
448	→	873
2673	→	947
2673	→	2721
1473	→	1887
96	→	1936
2211	→	1131
2211	→	2257
3110	→	729
1209	→	1201
1209	→	1763
1140	→	743
1140	→	749
1140	→	739
1140	→	2046
1140	→	785
1140	→	406
1140	→	955
1140	→	900
1140	→	681
1140	→	939
1140	→	576
1140	→	2648
1140	→	2386
2396	→	2384
1784	→	845
701	→	679
701	→	1895
3147	→	335
3147	→	3160
655	→	1751
1386	→	1367
1008	→	981
2056	→	1022
811	→	1466
2040	→	1014
2461	→	2787
2461	→	2793
2461	→	2855
2461	→	2906
2461	→	2910
2461	→	3002
472	→	1567
472	→	1889
472	→	2690
2804	→	2384
511	→	466
511	→	88
511	→	6
511	→	475
511	→	1174
511	→	493
511	→	1178
511	→	2429
1107	→	1541
1107	→	2996
659	→	387
659	→	2065
1792	→	845
2217	→	9
2242	→	2225
668	→	1785
2574	→	2530
878	→	862
878	→	1619
1584	→	404
1172	→	785
491	→	466
638	→	412
1724	→	812
260	→	310
1953	→	947
2654	→	162
2054	→	1022
3091	→	3136
3091	→	3144
3091	→	3148
18	→	1
18	→	743
18	→	745
18	→	992
624	→	591
2528	→	591
2402	→	2384
1098	→	1059
1118	→	6
1118	→	511
1118	→	1174
1118	→	493
1118	→	1178
1118	→	2429
41	→	9
41	→	980
41	→	1535
3161	→	1021
3	→	87
3	→	160
3	→	238
3	→	430
3	→	715
3	→	738
583	→	267
1483	→	1473
1483	→	1674
988	→	387
1752	→	826
600	→	591
218	→	188
218	→	285
218	→	599
218	→	829
1888	→	900
1888	→	1921
2080	→	1061
1289	→	1278
2583	→	2803
405	→	584
405	→	652
2581	→	2820
626	→	591
2980	→	2436
1858	→	2210
1858	→	2216
1858	→	2249
1858	→	2273
1858	→	2288
1858	→	2423
1858	→	2427
2683	→	956
411	→	1258
411	→	1294
411	→	1649
1467	→	578
1340	→	1741
9	→	162
9	→	562
9	→	1007
9	→	1911
729	→	810
729	→	890
729	→	1099
3031	→	236
2437	→	860
2437	→	854
5	→	67
5	→	140
5	→	236
5	→	403
5	→	713
5	→	744
774	→	170
2002	→	1991
2911	→	89
2911	→	2920
2911	→	3036
1778	→	845
2538	→	2461
2538	→	3038
1999	→	2573
1999	→	2713
2794	→	335
2794	→	2949
2794	→	3010
671	→	661
2966	→	188
598	→	17
2695	→	973
1567	→	2419
2628	→	862
1918	→	920
199	→	188
199	→	590
199	→	821
199	→	855
2289	→	188
3003	→	2973
1764	→	837
2568	→	2530
1618	→	753
1646	→	778
1295	→	335
1295	→	2047
756	→	2682
1082	→	1059
889	→	4
889	→	1097
889	→	676
889	→	377
889	→	759
889	→	359
889	→	90
889	→	670
889	→	1081
889	→	139
889	→	1029
889	→	115
889	→	730
889	→	918
889	→	1902
889	→	2256
749	→	729
749	→	2045
90	→	377
90	→	379
90	→	676
90	→	765
90	→	1097
892	→	1909
892	→	2077
2821	→	2384
3137	→	259
673	→	661
473	→	387
473	→	1625
1770	→	837
1890	→	162
2819	→	2384
1800	→	845
2072	→	1037
2566	→	2530
938	→	917
3163	→	2972
380	→	1917
2689	→	956
1	→	40
1	→	114
1	→	198
1	→	414
1	→	688
1	→	748
2582	→	404
1902	→	918
2295	→	188
2907	→	404
542	→	513
3153	→	412
2460	→	2969
1026	→	987
1591	→	2621
1730	→	812
2652	→	575
2795	→	3168
922	→	1793
2614	→	845
2244	→	2225
739	→	729
1299	→	335
1299	→	1944
1299	→	2073
2113	→	2527
2113	→	2981
716	→	679
716	→	1901
1570	→	404
1489	→	1473
1489	→	1676
2122	→	2108
2074	→	1037
2256	→	90
2697	→	17
977	→	2529
755	→	1496
755	→	1525
316	→	1958
3145	→	335
3145	→	3154
1066	→	1264
1066	→	1306
1066	→	1383
1066	→	1488
940	→	1609
2190	→	1113
1626	→	767
2357	→	259
410	→	3004
2052	→	1022
2913	→	753
2856	→	1367
688	→	2208
688	→	2218
688	→	2255
688	→	2294
688	→	2323
688	→	2425
688	→	2828
1922	→	940
2540	→	2530
2424	→	465
2424	→	2629
197	→	3
197	→	1019
197	→	808
197	→	510
197	→	795
197	→	404
197	→	680
197	→	492
197	→	877
197	→	450
197	→	474
197	→	871
197	→	415
197	→	2384
197	→	2414
197	→	2426
197	→	2584
197	→	2404
197	→	2428
197	→	2829
197	→	2804
342	→	336
139	→	90
139	→	359
139	→	670
139	→	759
139	→	1081
428	→	2397
689	→	679
689	→	742
689	→	449
689	→	138
689	→	65
689	→	217
689	→	700
689	→	2
747	→	729
747	→	2041
2392	→	1556
1661	→	1651
2370	→	259
2370	→	2694
1376	→	1019
1376	→	808
1376	→	510
1376	→	795
1376	→	404
1376	→	3
1376	→	680
1376	→	492
1376	→	877
1376	→	450
1376	→	2384
1376	→	2414
677	→	661
677	→	3122
3085	→	3142
3085	→	3146
3085	→	3152
751	→	1037
796	→	784
687	→	196
687	→	1460
1676	→	2243
1750	→	824
1592	→	699
1592	→	2
1592	→	1059
1592	→	1098
675	→	661
1348	→	714
1348	→	846
1348	→	742
1348	→	449
1348	→	138
1348	→	65
1348	→	217
1348	→	700
1348	→	2
1348	→	860
1348	→	854
1503	→	1137
2997	→	2972
2250	→	90
309	→	260
91	→	767
91	→	947
91	→	2053
1157	→	317
783	→	1179
170	→	1777
2283	→	1177
2283	→	879
2283	→	575
2283	→	1173
2283	→	795
2283	→	404
2283	→	680
2283	→	492
2283	→	877
2283	→	450
2283	→	2384
2283	→	2414
760	→	751
994	→	981
161	→	90
161	→	341
161	→	674
161	→	763
161	→	1095
268	→	1
268	→	1099
268	→	810
268	→	729
268	→	743
268	→	745
268	→	749
268	→	380
268	→	2648
1896	→	918
2675	→	90
2906	→	3077
141	→	90
141	→	361
141	→	672
141	→	761
141	→	1083
493	→	466
493	→	1749
540	→	513
540	→	924
1732	→	811
844	→	791
844	→	1731
1937	→	90
2827	→	2384
1339	→	1831
2650	→	890
2650	→	2957
2730	→	412
949	→	1611
679	→	775
679	→	1049
679	→	1109
1084	→	1059
597	→	1366
597	→	1427
597	→	1472
597	→	1974
597	→	2452
597	→	2737
1610	→	683
171	→	3
171	→	1019
171	→	808
171	→	510
171	→	474
171	→	404
171	→	871
171	→	415
171	→	680
171	→	652
171	→	584
171	→	405
171	→	793
171	→	431
171	→	2122
171	→	2384
171	→	2426
171	→	2584
171	→	2404
171	→	2408
171	→	2385
171	→	2428
171	→	2829
171	→	2804
2550	→	2530
3098	→	40
6	→	8
6	→	89
6	→	187
6	→	428
6	→	678
6	→	746
2282	→	2795
2064	→	317
337	→	2119
773	→	1799
1256	→	2613
404	→	510
404	→	575
404	→	808
404	→	879
404	→	1019
792	→	2
792	→	1109
792	→	775
792	→	811
792	→	679
792	→	689
792	→	856
792	→	860
792	→	714
792	→	1110
792	→	701
1240	→	680
1240	→	1177
1240	→	879
1240	→	575
1240	→	1173
1240	→	795
1240	→	404
1240	→	492
1240	→	877
1240	→	450
1240	→	2384
1240	→	2414
2526	→	592
577	→	1320
2462	→	2041
2462	→	890
2462	→	729
2462	→	981
2462	→	748
2462	→	414
2462	→	114
2462	→	40
2462	→	198
2462	→	688
2462	→	1
2462	→	1008
2462	→	747
2462	→	992
88	→	9
88	→	539
88	→	1537
88	→	1903
2736	→	1037
3011	→	1037
982	→	1013
1186	→	90
2802	→	196
2802	→	3085
2747	→	262
1818	→	730
1282	→	3083
431	→	404
431	→	793
2720	→	17
2114	→	1060
2114	→	1007
2114	→	162
2114	→	541
2114	→	262
2114	→	746
2114	→	428
2114	→	89
2114	→	8
2114	→	187
2114	→	678
2114	→	6
2114	→	9
2114	→	991
2114	→	66
2114	→	1050
288	→	260
1293	→	335
237	→	188
237	→	287
237	→	625
237	→	833
237	→	845
764	→	751
336	→	631
336	→	1585
270	→	260
699	→	679
699	→	1723
2982	→	2972
1146	→	9
1180	→	1163
1242	→	1231
1346	→	2575
1346	→	2653
1346	→	2955
906	→	316
923	→	668
2351	→	1099
2351	→	810
2351	→	729
2351	→	2033
2351	→	743
2681	→	90
1036	→	888
117	→	90
117	→	335
117	→	660
117	→	750
117	→	1058
808	→	1177
2414	→	2384
2	→	65
2	→	138
2	→	217
2	→	449
2	→	700
2	→	742
2537	→	2842
2537	→	2869
2537	→	2904
2537	→	2908
2537	→	2965
2537	→	3030
872	→	862
1540	→	592
2919	→	811
979	→	817
954	→	412
1347	→	2567
1347	→	2605
4	→	42
4	→	116
4	→	215
4	→	447
4	→	698
4	→	728
1291	→	1278
2584	→	404
1178	→	1163
449	→	2413
1018	→	987
1945	→	947
1945	→	2051
2796	→	196
2796	→	3091
1174	→	1163
582	→	1791
1650	→	2235
1786	→	845
2970	→	89
2970	→	3109
843	→	1923
520	→	2001
520	→	2557
1538	→	592
188	→	308
188	→	629
188	→	835
188	→	859
1035	→	2539
1892	→	162
1108	→	6
1108	→	1060
1108	→	1007
1108	→	162
1108	→	541
1108	→	262
1108	→	9
1108	→	991
1108	→	66
1108	→	1050
66	→	9
66	→	541
66	→	991
66	→	1539
318	→	1
318	→	1099
318	→	810
318	→	729
318	→	743
1043	→	1761
1043	→	2197
1043	→	2836
114	→	2375
114	→	2583
114	→	2647
114	→	2666
16	→	2971
2209	→	1131
1461	→	576
2048	→	1021
913	→	582
766	→	751
2184	→	510
2837	→	2428
795	→	1173
887	→	1277
1491	→	1473
1491	→	1660
1692	→	1650
2006	→	17
2376	→	259
2382	→	335
2382	→	2672
2382	→	2735
925	→	917
1536	→	592
2576	→	404
3005	→	2972
3037	→	336
1201	→	1769
450	→	404
450	→	492
450	→	795
450	→	877
3084	→	2428
834	→	822
834	→	2121
2004	→	1991
1378	→	1367
1832	→	862
944	→	842
1526	→	404
2600	→	2590
2648	→	890
1044	→	888
1044	→	2176
2835	→	2428
1006	→	981
1632	→	770
1943	→	90
1184	→	90
991	→	2369
991	→	2381
991	→	2440
991	→	2467
2439	→	2428
2964	→	188
563	→	513
563	→	937
1983	→	973
3143	→	259
758	→	170
1861	→	1850
1861	→	2688
1207	→	266
1239	→	2801
1780	→	845
630	→	591
630	→	837
2691	→	729
2575	→	2818
216	→	188
216	→	259
216	→	623
216	→	831
216	→	857
1307	→	335
1307	→	1952
1307	→	2071
2909	→	404
362	→	336
1675	→	1651
1321	→	14
2788	→	259
2788	→	2967
189	→	973
2416	→	2384
2622	→	845
1259	→	1248
1384	→	1367
856	→	846
1910	→	918
115	→	90
115	→	4
828	→	658
952	→	1545
952	→	1547
2801	→	3162
2408	→	2384
1975	→	188
414	→	2403
905	→	1147
2076	→	1037
1886	→	575
17	→	1260
17	→	1298
17	→	1385
17	→	1490
2729	→	2943
3076	→	2384
1894	→	162
1894	→	2525
510	→	2619
1569	→	2395
836	→	822
1286	→	2551
1286	→	2719
1286	→	2729
1286	→	2918
714	→	679
714	→	1729
360	→	336
1583	→	2401
164	→	1631
2068	→	1033
1144	→	9
1129	→	1026
2420	→	2384
68	→	9
68	→	560
68	→	1005
870	→	4
870	→	730
870	→	115
870	→	381
870	→	2256
2404	→	2384
2234	→	1652
2324	→	1231
762	→	751
267	→	1779
413	→	2
413	→	1109
413	→	775
413	→	811
413	→	679
413	→	689
413	→	1110
413	→	701
413	→	796
413	→	809
413	→	716
832	→	822
858	→	846
2977	→	3044
2612	→	412
521	→	3
521	→	1019
521	→	808
521	→	510
521	→	795
521	→	404
521	→	680
521	→	492
521	→	877
521	→	450
521	→	2384
521	→	2414
1677	→	1651
2078	→	1052
2950	→	947
1904	→	917
340	→	264
2000	→	1098
2000	→	699
2000	→	742
2000	→	449
2000	→	138
2000	→	65
2000	→	217
2000	→	700
2000	→	2
2000	→	1082
1742	→	824
388	→	2
388	→	1109
388	→	775
388	→	811
388	→	679
388	→	689
388	→	714
388	→	846
388	→	860
388	→	854
388	→	1110
388	→	701
388	→	1098
388	→	699
388	→	1082
2630	→	862
2665	→	162
782	→	266
1620	→	753
2355	→	2342
378	→	336
1959	→	90
2219	→	9
1660	→	2224
3149	→	412
1285	→	2680
2968	→	973
2422	→	2384
2272	→	2258
2829	→	2428
2426	→	465
2426	→	2627
412	→	1130
412	→	1145
412	→	1185
412	→	1208
412	→	1230
412	→	1349
412	→	2834
852	→	736
2560	→	2530
1375	→	2559
1375	→	2696
2843	→	3099
2380	→	335
2410	→	2384
2536	→	3097
1050	→	2079
43	→	9
43	→	512
43	→	993
1480	→	2994
3092	→	412
1481	→	991
2852	→	2384
2852	→	2619
2852	→	1019
2852	→	808
2852	→	510
2852	→	877
2852	→	492
2852	→	680
2852	→	404
2852	→	795
2852	→	450
2852	→	2414
1568	→	404
961	→	411
2712	→	981
669	→	2
669	→	699
669	→	1059
669	→	1098
669	→	811
669	→	689
822	→	1645
317	→	2005
317	→	2057
317	→	2549
1912	→	917
1951	→	947
1951	→	2055
1265	→	1248
1265	→	1982
888	→	1288
888	→	1583
888	→	1849
888	→	1893
2066	→	2058
1857	→	2341
1857	→	2356
1857	→	2379
1857	→	2589
1857	→	2611
2398	→	2384
1350	→	1339
1350	→	1809
2034	→	1013
1924	→	575
403	→	2409
3169	→	2972
1961	→	957
1658	→	2377
1658	→	2581
1658	→	2649
1658	→	2664
447	→	2415
576	→	900
576	→	939
576	→	955
1612	→	734
682	→	2039
163	→	907
163	→	1743
2378	→	259
737	→	196
3155	→	1021
1263	→	1248
1263	→	1980
2606	→	162
2606	→	2711
864	→	883
992	→	981
992	→	1099
992	→	810
992	→	1008
992	→	1
992	→	729
992	→	747
475	→	466
1981	→	973
2870	→	512
1810	→	2912
2958	→	956
2467	→	2826
2120	→	2108
430	→	2407
1061	→	2067
415	→	404
415	→	474
415	→	871
415	→	795
415	→	3
415	→	492
415	→	877
415	→	450
415	→	2384
415	→	2414
1096	→	1059
3100	→	2532
2236	→	2225
2552	→	2530
2598	→	1239
2266	→	1014
2667	→	162
1744	→	825
1024	→	1119
1542	→	591
196	→	2421
898	→	1141
898	→	1143
898	→	1183
898	→	1200
898	→	1241
898	→	1338
898	→	2438
2₁(2121)	→	2122
2₁(471)	→	472
2₁(765)	→	766
2₁(3152)	→	3153
2₁(2107)	→	2108
2₁(339)	→	340
2₁(2106)	→	2107
2₁(1013)	→	1014
2₁(1885)	→	1886
2₁(1749)	→	1750
2₁(1488)	→	1489
2₁(196)	→	197
2₁(1490)	→	1491
2₁(910)	→	911
2₁(2119)	→	2120
2₁(1567)	→	1568
2₁(842)	→	843
2₁(447)	→	448
2₁(912)	→	913
2₁(410)	→	411
2₁(761)	→	762
2₁(1472)	→	1473
2₁(1741)	→	1742
2₁(587)	→	588
2₁(684)	→	685
2₁(2113)	→	2114
2₁(1349)	→	1350
2₁(2651)	→	2652
2₁(654)	→	655
2₁(679)	→	680
2₁(763)	→	764
2₁(666)	→	667
2₁(885)	→	886
2₁(2795)	→	2796
2₁(1368)	→	1369
2₁(1052)	→	1053
2₁(786)	→	787
2₁(2906)	→	2907
2₁(908)	→	909
2₁(586)	→	587
2₁(166)	→	167
2₁(779)	→	780
2₁(2423)	→	2424
2₁(1100)	→	1101
2₁(2611)	→	2612
2₁(1655)	→	1656
2₁(513)	→	514
2₁(585)	→	586
2₁(2467)	→	2468
2₁(404)	→	405
2₁(904)	→	905
2₁(168)	→	169
2₁(338)	→	339
2₁(2077)	→	2078
2₁(1812)	→	1813
2₁(1813)	→	1814
2₁(835)	→	836
2₁(449)	→	450
2₁(1014)	→	1015
2₁(1474)	→	1475
2₁(2075)	→	2076
2₁(1743)	→	1744
2₁(2189)	→	2190
2₁(2425)	→	2426
2₁(767)	→	768
2₁(759)	→	760
2₁(16)	→	17
2₁(403)	→	404
2₁(2071)	→	2072
2₁(2908)	→	2909
2₁(840)	→	841
2₁(750)	→	751
2₁(1101)	→	1102
2₁(1480)	→	1481
2₁(1995)	→	1996
2₁(1923)	→	1924
2₁(850)	→	851
2₁(1691)	→	1692
2₁(1107)	→	1108
2₁(1589)	→	1590
2₁(754)	→	755
2₁(1112)	→	1113
2₁(1253)	→	1254
2₁(1476)	→	1477
2₁(430)	→	431
2₁(1649)	→	1650
2₁(2039)	→	2040
2₁(1657)	→	1658
2₁(683)	→	684
2₁(1041)	→	1042
2₁(788)	→	789
2₁(1283)	→	1284
2₁(1816)	→	1817
2₁(1051)	→	1052
2₁(1477)	→	1478
2₁(976)	→	977
2₁(833)	→	834
2₁(336)	→	337
2₁(978)	→	979
2₁(2073)	→	2074
2₁(686)	→	687
2₁(1063)	→	1064
2₁(2581)	→	2582
2₁(1338)	→	1339
2₁(868)	→	869
2₁(2969)	→	2970
2₁(1482)	→	1483
2₁(3010)	→	3011
2₁(826)	→	827
2₁(414)	→	415
2₁(2179)	→	2180
2₁(776)	→	777
2₁(1583)	→	1584
2₁(1653)	→	1654
2₁(2575)	→	2576
2₁(1055)	→	1056
2₁(864)	→	865
2₁(1475)	→	1476
2₁(2801)	→	2802
2₁(984)	→	985
2₁(428)	→	429
2₁(1569)	→	1570
2₁(865)	→	866
2₁(781)	→	782
2₁(3148)	→	3149
2₁(823)	→	824
2₁(1473)	→	1474
2₁(2583)	→	2584
2₁(314)	→	315
2₁(2735)	→	2736
2₁(584)	→	585
2₁(264)	→	265
2₁(1017)	→	1018
2₁(824)	→	825
2₁(1525)	→	1526
2₁(653)	→	654
2₁(821)	→	822
2₁(829)	→	830
2₁(1345)	→	1346
2₁(973)	→	974
2₁(162)	→	163
2₁(164)	→	165
2₁(953)	→	954
2₁(790)	→	791
2₁(838)	→	839
2₁(951)	→	952
2₁(831)	→	832
0₂(2599)	→	2600
0₂(2737)	→	2738
0₂(2534)	→	2535
0₂(2978)	→	2979
0₂(2537)	→	2538
0₂(1139)	→	1140
0₂(1502)	→	1503
0₂(2845)	→	2846
0₂(2596)	→	2597
0₂(1171)	→	1172
0₂(2233)	→	2234
0₂(2461)	→	2462
0₂(1156)	→	1157
0₂(2385)	→	2386
0₂(2589)	→	2590
0₂(2391)	→	2392
0₂(2535)	→	2536
0₂(1430)	→	1431
0₂(2458)	→	2459
0₂(1128)	→	1129
0₂(2206)	→	2207
4₂(2539)	→	2540
4₂(2436)	→	2437
4₂(1120)	→	1121
4₂(2225)	→	2226
4₂(2430)	→	2431
4₂(1125)	→	1126
4₂(1231)	→	1232
4₂(2592)	→	2593
4₂(1241)	→	1242
4₂(2274)	→	2275
4₂(2273)	→	2274
4₂(2559)	→	2560
4₂(2850)	→	2851
4₂(1550)	→	1551
4₂(2323)	→	2324
4₂(2565)	→	2566
4₂(1163)	→	1164
4₂(2348)	→	2349
4₂(2573)	→	2574
4₂(2745)	→	2746
4₂(1136)	→	1137
4₂(2388)	→	2389
4₂(1168)	→	1169
4₂(1122)	→	1123
4₂(2979)	→	2980
4₂(2341)	→	2342
4₂(2549)	→	2550
4₂(1150)	→	1151
4₂(2230)	→	2231
4₂(2536)	→	2537
4₂(1555)	→	1556
4₂(1148)	→	1149
4₂(1133)	→	1134
4₂(2264)	→	2265
4₂(2851)	→	2852
4₂(2975)	→	2976
4₂(1554)	→	1555
4₂(3038)	→	3039
4₂(1131)	→	1132
4₂(2198)	→	2199
4₂(2738)	→	2739
4₂(2354)	→	2355
4₂(2200)	→	2201
4₂(1153)	→	1154
4₂(2551)	→	2552
4₂(2203)	→	2204
4₂(2567)	→	2568
4₂(2529)	→	2530
4₂(1436)	→	1437
4₂(2557)	→	2558
4₂(1230)	→	1231
4₂(2227)	→	2228
4₂(1435)	→	1436
4₂(1548)	→	1549
4₂(1165)	→	1166
1₂(2343)	→	2344
1₂(2279)	→	2280
1₂(1134)	→	1135
1₂(2228)	→	2229
1₂(1236)	→	1237
1₂(1123)	→	1124
1₂(2977)	→	2978
1₂(2201)	→	2202
1₂(2262)	→	2263
1₂(2594)	→	2595
1₂(1166)	→	1167
1₂(2741)	→	2742
1₂(1549)	→	1550
1₂(1556)	→	1557
1₂(1151)	→	1152
1₂(1552)	→	1553
1₂(2386)	→	2387
1₂(2432)	→	2433
1₂(1551)	→	1552
4₃(3050)	→	3051
4₃(3047)	→	3048
4₃(3045)	→	3046
4₁(2963)	→	2964
4₁(1831)	→	1832
4₁(1375)	→	1376
4₁(3136)	→	3137
4₁(1035)	→	1036
4₁(941)	→	942
4₁(751)	→	752
4₁(1785)	→	1786
4₁(1982)	→	1983
4₁(2369)	→	2370
4₁(1279)	→	1280
4₁(2377)	→	2378
4₁(93)	→	94
4₁(467)	→	468
4₁(1260)	→	1261
4₁(377)	→	378
4₁(867)	→	868
4₁(1277)	→	1278
4₁(1201)	→	1202
4₁(1039)	→	1040
4₁(1999)	→	2000
4₁(974)	→	975
4₁(1374)	→	1375
4₁(1631)	→	1632
4₁(9)	→	10
4₁(1286)	→	1287
4₁(731)	→	732
4₁(1347)	→	1348
4₁(775)	→	776
4₁(1061)	→	1062
4₁(1290)	→	1291
4₁(1791)	→	1792
4₁(778)	→	779
4₁(1106)	→	1107
4₁(11)	→	12
4₁(236)	→	237
4₁(217)	→	218
4₁(520)	→	521
4₁(861)	→	862
4₁(2294)	→	2295
4₁(14)	→	15
4₁(1761)	→	1762
4₁(2288)	→	2289
4₁(1793)	→	1794
4₁(849)	→	850
4₁(1980)	→	1981
4₁(215)	→	216
4₁(1099)	→	1100
4₁(2627)	→	2628
4₁(169)	→	170
4₁(947)	→	948
4₁(1288)	→	1289
4₁(851)	→	852
4₁(1208)	→	1209
4₁(661)	→	662
4₁(341)	→	342
4₁(769)	→	770
4₁(1988)	→	1989
4₁(3036)	→	3037
4₁(1466)	→	1467
4₁(1799)	→	1800
4₁(1777)	→	1778
4₁(2787)	→	2788
4₁(519)	→	520
4₁(879)	→	880
4₁(2965)	→	2966
4₁(1341)	→	1342
4₁(198)	→	199
4₁(637)	→	638
4₁(2619)	→	2620
4₁(1247)	→	1248
4₁(901)	→	902
4₁(2356)	→	2357
4₁(1264)	→	1265
4₁(387)	→	388
4₁(187)	→	188
4₁(877)	→	878
4₁(1998)	→	1999
4₁(892)	→	893
4₁(2177)	→	2178
4₁(1110)	→	1111
4₁(2112)	→	2113
4₁(1779)	→	1780
4₁(907)	→	908
4₁(2621)	→	2622
4₁(873)	→	874
4₁(920)	→	921
4₁(1852)	→	1853
4₁(188)	→	189
4₁(310)	→	311
4₁(2694)	→	2695
4₁(1815)	→	1816
4₁(3097)	→	3098
4₁(2613)	→	2614
4₁(1974)	→	1975
4₁(940)	→	941
4₁(265)	→	266
4₁(2967)	→	2968
4₁(317)	→	318
4₁(632)	→	633
4₁(359)	→	360
4₁(408)	→	409
4₁(596)	→	597
4₁(577)	→	578
4₁(1590)	→	1591
4₁(977)	→	978
4₁(636)	→	637
4₁(238)	→	239
4₁(361)	→	362
4₁(871)	→	872
4₁(1262)	→	1263
4₁(667)	→	668
4₁(1809)	→	1810
4₁(3142)	→	3143
4₁(827)	→	828
4₁(97)	→	98
4₁(2629)	→	2630
4₁(987)	→	988
4₁(1258)	→	1259
4₁(578)	→	579
4₁(1022)	→	1023
4₁(2375)	→	2376
4₁(335)	→	336
4₁(1254)	→	1255
4₁(1783)	→	1784
4₁(1200)	→	1201
4₀(3)	→	5
4₀(6)	→	5
4₀(5)	→	5
4₀(4)	→	5
4₀(2)	→	5
4₀(1)	→	5
5₃(3049)	→	3050
5₃(3044)	→	3045
3₃(3051)	→	3052
3₃(3046)	→	3047
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
2₂(2826)	→	2827
2₂(2415)	→	2416
2₂(2453)	→	2454
2₂(1496)	→	1497
2₂(2904)	→	2905
2₂(2836)	→	2837
2₂(2407)	→	2408
2₂(2438)	→	2439
2₂(2746)	→	2747
2₂(1500)	→	1501
2₂(2834)	→	2835
2₂(2996)	→	2997
2₂(1170)	→	1171
2₂(2740)	→	2741
2₂(3168)	→	3169
2₂(2257)	→	2258
2₂(3083)	→	3084
2₂(2427)	→	2428
2₂(1239)	→	1240
2₂(1127)	→	1128
2₂(3077)	→	3078
2₂(3004)	→	3005
2₂(2739)	→	2740
2₂(1498)	→	1499
2₂(2454)	→	2455
2₂(2397)	→	2398
2₂(2395)	→	2396
2₂(2456)	→	2457
2₂(2259)	→	2260
2₂(2205)	→	2206
2₂(2828)	→	2829
2₂(2261)	→	2262
2₂(3075)	→	3076
2₂(2844)	→	2845
2₂(3162)	→	3163
2₂(2994)	→	2995
2₂(2390)	→	2391
2₂(2455)	→	2456
2₂(2419)	→	2420
2₂(2460)	→	2461
2₂(1499)	→	1500
2₂(2232)	→	2233
2₂(2263)	→	2264
2₂(2820)	→	2821
2₂(1155)	→	1156
2₂(2383)	→	2384
2₂(2347)	→	2348
2₂(2403)	→	2404
2₂(1497)	→	1498
2₂(2452)	→	2453
2₂(2981)	→	2982
2₂(2457)	→	2458
2₂(2434)	→	2435
2₂(2384)	→	2385
2₂(2803)	→	2804
2₂(2421)	→	2422
2₂(2971)	→	2972
2₂(2409)	→	2410
2₂(1138)	→	1139
2₂(1429)	→	1430
2₂(2271)	→	2272
2₂(2282)	→	2283
2₂(2818)	→	2819
2₂(2413)	→	2414
2₂(2401)	→	2402
2₂(1501)	→	1502
2₃(3052)	→	3053
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
5₁(170)	→	171
5₁(2109)	→	2110
5₁(3122)	→	3123
5₁(822)	→	823
5₁(87)	→	88
5₁(1143)	→	1144
5₁(866)	→	867
5₁(1952)	→	1953
5₁(812)	→	813
5₁(42)	→	43
5₁(846)	→	847
5₁(1030)	→	1031
5₁(753)	→	754
5₁(1591)	→	1592
5₁(512)	→	513
5₁(1366)	→	1367
5₁(515)	→	516
5₁(599)	→	600
5₁(1385)	→	1386
5₁(8)	→	9
5₁(490)	→	491
5₁(1020)	→	1021
5₁(919)	→	920
5₁(2949)	→	2950
5₁(948)	→	949
5₁(582)	→	583
5₁(1281)	→	1282
5₁(192)	→	193
5₁(2059)	→	2060
5₁(2696)	→	2697
5₁(2672)	→	2673
5₁(734)	→	735
5₁(629)	→	630
5₁(1256)	→	1257
5₁(1344)	→	1345
5₁(407)	→	408
5₁(1205)	→	1206
5₁(730)	→	731
5₁(2719)	→	2720
5₁(2047)	→	2048
5₁(682)	→	683
5₁(465)	→	466
5₁(1993)	→	1994
5₁(510)	→	511
5₁(3160)	→	3161
5₁(770)	→	771
5₁(2063)	→	2064
5₁(957)	→	958
5₁(1377)	→	1378
5₁(2713)	→	2714
5₁(657)	→	658
5₁(789)	→	790
5₁(2062)	→	2063
5₁(986)	→	987
5₁(539)	→	540
5₁(1339)	→	1340
5₁(90)	→	91
5₁(2666)	→	2667
5₁(13)	→	14
5₁(1340)	→	1341
5₁(652)	→	653
5₁(1917)	→	1918
5₁(1023)	→	1024
5₁(1763)	→	1764
5₁(623)	→	624
5₁(900)	→	901
5₁(474)	→	475
5₁(1990)	→	1991
5₁(470)	→	471
5₁(2855)	→	2856
5₁(685)	→	686
5₁(625)	→	626
5₁(1609)	→	1610
5₁(92)	→	93
5₁(67)	→	68
5₁(1944)	→	1945
5₁(1060)	→	1061
5₁(2079)	→	2080
5₁(982)	→	983
5₁(468)	→	469
5₁(1617)	→	1618
5₁(492)	→	493
5₁(848)	→	849
5₁(3154)	→	3155
5₁(817)	→	818
5₁(1889)	→	1890
5₁(894)	→	895
5₁(1769)	→	1770
5₁(2218)	→	2219
5₁(267)	→	268
5₁(814)	→	815
5₁(384)	→	385
5₁(40)	→	41
5₁(541)	→	542
5₁(518)	→	519
5₁(1373)	→	1374
5₁(1117)	→	1118
5₁(1250)	→	1251
5₁(1541)	→	1542
5₁(922)	→	923
5₁(165)	→	166
5₁(1034)	→	1035
5₁(2653)	→	2654
5₁(1114)	→	1115
5₁(261)	→	262
5₁(902)	→	903
5₁(1103)	→	1104
5₁(65)	→	66
5₁(1656)	→	1657
5₁(664)	→	665
5₁(909)	→	910
5₁(943)	→	944
5₁(592)	→	593
5₁(1059)	→	1060
5₁(195)	→	196
5₁(1625)	→	1626
5₁(163)	→	164
5₁(2664)	→	2665
5₁(1033)	→	1034
5₁(560)	→	561
5₁(752)	→	753
5₁(579)	→	580
5₁(1855)	→	1856
5₁(656)	→	657
5₁(1031)	→	1032
5₁(1015)	→	1016
5₁(2111)	→	2112
5₁(960)	→	961
5₁(1367)	→	1368
5₁(895)	→	896
5₁(2060)	→	2061
5₁(1383)	→	1384
5₁(1850)	→	1851
5₁(2005)	→	2006
5₁(2527)	→	2528
5₁(949)	→	950
5₁(863)	→	864
5₁(668)	→	669
5₁(1587)	→	1588
5₁(593)	→	594
5₁(2003)	→	2004
5₁(883)	→	884
5₁(1016)	→	1017
5₁(890)	→	891
5₁(1950)	→	1951
5₁(1053)	→	1054
5₁(2605)	→	2606
5₁(1997)	→	1998
5₁(773)	→	774
5₁(1049)	→	1050
5₁(312)	→	313
5₁(1342)	→	1343
5₁(1893)	→	1894
5₁(1891)	→	1892
5₁(2181)	→	2182
5₁(386)	→	387
5₁(1854)	→	1855
5₁(1145)	→	1146
5₁(2912)	→	2913
5₁(466)	→	467
5₁(1619)	→	1620
5₁(635)	→	636
5₁(732)	→	733
5₁(2869)	→	2870
5₁(1370)	→	1371
5₁(2440)	→	2441
5₁(1320)	→	1321
5₁(2216)	→	2217
5₁(1811)	→	1812
5₁(590)	→	591
5₁(1814)	→	1815
5₁(768)	→	769
5₁(2001)	→	2002
5₁(1105)	→	1106
5₁(562)	→	563
3₁(1300)	→	1301
3₁(138)	→	139
3₁(674)	→	675
3₁(2674)	→	2675
3₁(517)	→	518
3₁(472)	→	473
3₁(262)	→	263
3₁(3146)	→	3147
3₁(1185)	→	1186
3₁(1204)	→	1205
3₁(2053)	→	2054
3₁(1371)	→	1372
3₁(263)	→	264
3₁(2110)	→	2111
3₁(1183)	→	1184
3₁(1346)	→	1347
3₁(1537)	→	1538
3₁(1723)	→	1724
3₁(1064)	→	1065
3₁(2065)	→	2066
3₁(903)	→	904
3₁(1585)	→	1586
3₁(2721)	→	2722
3₁(1252)	→	1253
3₁(189)	→	190
3₁(266)	→	267
3₁(888)	→	889
3₁(772)	→	773
3₁(2379)	→	2380
3₁(2051)	→	2052
3₁(1280)	→	1281
3₁(383)	→	384
3₁(959)	→	960
3₁(1539)	→	1540
3₁(1298)	→	1299
3₁(1856)	→	1857
3₁(1104)	→	1105
3₁(2525)	→	2526
3₁(1936)	→	1937
3₁(2183)	→	2184
3₁(672)	→	673
3₁(2793)	→	2794
3₁(1372)	→	1373
3₁(862)	→	863
3₁(311)	→	312
3₁(94)	→	95
3₁(1535)	→	1536
3₁(381)	→	382
3₁(1958)	→	1959
3₁(1278)	→	1279
3₁(1294)	→	1295
3₁(1895)	→	1896
3₁(670)	→	671
3₁(896)	→	897
3₁(1113)	→	1114
3₁(736)	→	737
3₁(816)	→	817
3₁(1909)	→	1910
3₁(190)	→	191
3₁(655)	→	656
3₁(581)	→	582
3₁(1065)	→	1066
3₁(114)	→	115
3₁(191)	→	192
3₁(194)	→	195
3₁(140)	→	141
3₁(580)	→	581
3₁(811)	→	812
3₁(269)	→	270
3₁(1479)	→	1480
3₁(921)	→	922
3₁(2680)	→	2681
3₁(1203)	→	1204
3₁(2055)	→	2056
3₁(1960)	→	1961
3₁(676)	→	677
3₁(591)	→	592
3₁(777)	→	778
3₁(308)	→	309
3₁(1942)	→	1943
3₁(1306)	→	1307
3₁(887)	→	888
3₁(2249)	→	2250
3₁(2688)	→	2689
3₁(2057)	→	2058
3₁(956)	→	957
3₁(1255)	→	1256
3₁(89)	→	90
3₁(2682)	→	2683
3₁(2957)	→	2958
3₁(1056)	→	1057
3₁(1292)	→	1293
3₁(1901)	→	1902
3₁(1729)	→	1730
3₁(729)	→	730
3₁(1248)	→	1249
3₁(1062)	→	1063
3₁(2255)	→	2256
3₁(1116)	→	1117
3₁(287)	→	288
3₁(1021)	→	1022
3₁(116)	→	117
3₁(955)	→	956
3₁(1658)	→	1659
3₁(662)	→	663
3₁(917)	→	918
3₁(1545)	→	1546
3₁(2381)	→	2382
3₁(259)	→	260
3₁(10)	→	11
3₁(1251)	→	1252
3₁(285)	→	286
3₁(660)	→	661
3₁(975)	→	976
3₁(1810)	→	1811
3₁(2729)	→	2730
3₁(663)	→	664
3₁(1586)	→	1587
3₁(2180)	→	2181
3₁(1202)	→	1203
3₁(15)	→	16
3₁(382)	→	383
3₁(1645)	→	1646
3₁(791)	→	792
3₁(1019)	→	1020
3₁(516)	→	517
3₁(380)	→	381
3₁(409)	→	410
3₁(160)	→	161
3₁(3144)	→	3145
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
1₁(810)	→	811
1₁(1676)	→	1677
1₁(916)	→	917
1₁(1674)	→	1675
1₁(1994)	→	1995
1₁(1650)	→	1651
1₁(1851)	→	1852
1₁(859)	→	860
1₁(771)	→	772
1₁(385)	→	386
1₁(855)	→	856
1₁(2176)	→	2177
1₁(469)	→	470
1₁(1660)	→	1661
1₁(841)	→	842
1₁(2058)	→	2059
1₁(1029)	→	1030
1₁(1611)	→	1612
1₁(1058)	→	1059
1₁(2108)	→	2109
1₁(845)	→	846
1₁(1095)	→	1096
1₁(313)	→	314
1₁(783)	→	784
1₁(1751)	→	1752
1₁(1903)	→	1904
1₁(937)	→	938
1₁(1343)	→	1344
1₁(12)	→	13
1₁(1050)	→	1051
1₁(733)	→	734
1₁(837)	→	838
1₁(193)	→	194
1₁(167)	→	168
1₁(1282)	→	1283
1₁(1911)	→	1912
1₁(808)	→	809
1₁(795)	→	796
1₁(1083)	→	1084
1₁(898)	→	899
1₁(698)	→	699
1₁(1111)	→	1112
1₁(2918)	→	2919
1₁(942)	→	943
1₁(1206)	→	1207
1₁(1102)	→	1103
1₁(813)	→	814
1₁(1858)	→	1859
1₁(1109)	→	1110
1₁(406)	→	407
1₁(2920)	→	2921
1₁(958)	→	959
1₁(631)	→	632
1₁(1043)	→	1044
1₁(857)	→	858
1₁(1249)	→	1250
1₁(1097)	→	1098
1₁(985)	→	986
1₁(983)	→	984
1₁(634)	→	635
1₁(688)	→	689
1₁(825)	→	826
1₁(678)	→	679
1₁(700)	→	701
1₁(1081)	→	1082
1₁(91)	→	92
1₁(633)	→	634
1₁(1996)	→	1997
1₁(1731)	→	1732
1₁(757)	→	758
1₁(1853)	→	1854
1₁(576)	→	577
1₁(891)	→	892
1₁(715)	→	716
1₁(1024)	→	1025
1₁(793)	→	794
1₁(2178)	→	2179
1₁(713)	→	714
1₁(924)	→	925
1₁(905)	→	906
1₁(260)	→	261
1₁(886)	→	887
1₁(893)	→	894
1₁(853)	→	854
1₁(412)	→	413
0₃(3053)	→	3054
0₁(337)	→	338
0₁(3109)	→	3110
0₁(3030)	→	3031
0₁(1651)	→	1652
0₁(1040)	→	1041
0₁(1860)	→	1861
0₁(2045)	→	2046
0₁(735)	→	736
0₁(1460)	→	1461
0₁(815)	→	816
0₁(1038)	→	1039
0₁(1066)	→	1067
0₁(17)	→	18
0₁(1817)	→	1818
0₁(1115)	→	1116
0₁(1992)	→	1993
0₁(2955)	→	2956
0₁(597)	→	598
0₁(780)	→	781
0₁(1478)	→	1479
0₁(665)	→	666
0₁(980)	→	981
0₁(3085)	→	3086
0₁(1369)	→	1370
0₁(411)	→	412
0₁(950)	→	951
0₁(1007)	→	1008
0₁(514)	→	515
0₁(1588)	→	1589
0₁(2182)	→	2183
0₁(1037)	→	1038
0₁(1005)	→	1006
0₁(748)	→	749
0₁(738)	→	739
0₁(785)	→	786
0₁(1991)	→	1992
0₁(680)	→	681
0₁(2061)	→	2062
0₁(575)	→	576
0₁(2649)	→	2650
0₁(1284)	→	1285
0₁(96)	→	97
0₁(847)	→	848
0₁(588)	→	589
0₁(1032)	→	1033
0₁(2067)	→	2068
0₁(316)	→	317
0₁(594)	→	595
0₁(1285)	→	1286
0₁(755)	→	756
0₁(952)	→	953
0₁(843)	→	844
0₁(3091)	→	3092
0₁(658)	→	659
0₁(1054)	→	1055
0₁(1042)	→	1043
0₁(869)	→	870
0₁(405)	→	406
0₁(991)	→	992
0₁(746)	→	747
0₁(2690)	→	2691
0₁(897)	→	898
0₁(2033)	→	2034
0₁(742)	→	743
0₁(2711)	→	2712
0₁(1857)	→	1858
0₁(993)	→	994
0₁(681)	→	682
0₁(784)	→	785
0₁(2910)	→	2911
0₁(756)	→	757
0₁(918)	→	919
0₁(2647)	→	2648
0₁(2041)	→	2042
0₁(1654)	→	1655
0₁(1921)	→	1922
0₁(379)	→	380
0₁(744)	→	745
0₁(911)	→	912
0₁(2943)	→	2944
0₁(315)	→	316
0₁(1652)	→	1653
0₁(787)	→	788
0₁(1849)	→	1850
0₁(95)	→	96
0₁(2727)	→	2728
0₁(1887)	→	1888
0₁(939)	→	940
0₁(884)	→	885
0₁(981)	→	982
0₁(1025)	→	1026
0₁(728)	→	729
0₁(595)	→	596
0₁(839)	→	840
3₂(1126)	→	1127
3₂(1432)	→	1433
3₂(2275)	→	2276
3₂(2389)	→	2390
3₂(1169)	→	1170
3₂(2345)	→	2346
3₂(1234)	→	1235
3₂(2231)	→	2232
3₂(2974)	→	2975
3₂(3099)	→	3100
3₂(1232)	→	1233
3₂(1164)	→	1165
3₂(2342)	→	2343
3₂(2972)	→	2973
3₂(2597)	→	2598
3₂(1132)	→	1133
3₂(2531)	→	2532
3₂(2743)	→	2744
3₂(1237)	→	1238
3₂(1154)	→	1155
3₂(3002)	→	3003
3₂(1547)	→	1548
3₂(2349)	→	2350
3₂(2848)	→	2849
3₂(1233)	→	1234
3₂(2277)	→	2278
3₂(2847)	→	2848
3₂(1433)	→	1434
3₂(2280)	→	2281
3₂(2346)	→	2347
3₂(1121)	→	1122
3₂(2590)	→	2591
3₂(1149)	→	1150
3₂(2459)	→	2460
3₂(2435)	→	2436
3₂(2276)	→	2277
3₂(2226)	→	2227
3₂(1137)	→	1138
3₂(2199)	→	2200
3₂(2204)	→	2205
1₃(3048)	→	3049
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
5₂(1141)	→	1142
5₂(2843)	→	2844
5₂(1553)	→	1554
5₂(1162)	→	1163
5₂(2278)	→	2279
5₂(2973)	→	2974
5₂(2202)	→	2203
5₂(2595)	→	2596
5₂(2429)	→	2430
5₂(2431)	→	2432
5₂(2593)	→	2594
5₂(2742)	→	2743
5₂(1235)	→	1236
5₂(2235)	→	2236
5₂(2744)	→	2745
5₂(1428)	→	1429
5₂(2241)	→	2242
5₂(1152)	→	1153
5₂(2229)	→	2230
5₂(2260)	→	2261
5₂(2530)	→	2531
5₂(2258)	→	2259
5₂(1427)	→	1428
5₂(2591)	→	2592
5₂(1179)	→	1180
5₂(1431)	→	1432
5₂(1167)	→	1168
5₂(2842)	→	2843
5₂(1119)	→	1120
5₂(1147)	→	1148
5₂(2428)	→	2429
5₂(1135)	→	1136
5₂(2208)	→	2209
5₂(2243)	→	2244
5₂(1124)	→	1125
5₂(2265)	→	2266
5₂(2849)	→	2850
5₂(2224)	→	2225
5₂(1434)	→	1435
5₂(2532)	→	2533
5₂(2210)	→	2211
5₂(1238)	→	1239
5₂(2846)	→	2847
5₂(2433)	→	2434
5₂(2281)	→	2282
5₂(1173)	→	1174
5₂(1177)	→	1178
5₂(2197)	→	2198
5₂(2387)	→	2388
5₂(2533)	→	2534
5₂(2976)	→	2977
5₂(2344)	→	2345
5₂(1130)	→	1131
5₂(2350)	→	2351

The automaton is closed under rewriting as it is compatible.