Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4487)

The rewrite relation of the following TRS is considered.

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

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:

272	→	2280
2645	→	821
2645	→	2677
1839	→	884
2441	→	1111
854	→	2950
2868	→	635
2868	→	2984
314	→	264
314	→	635
2618	→	2875
871	→	862
2625	→	731
364	→	2091
2818	→	115
3006	→	123
2501	→	2490
899	→	891
869	→	401
1287	→	2948
205	→	1058
205	→	1072
205	→	1108
205	→	1169
205	→	1361
205	→	1463
205	→	1574
2759	→	1763
2393	→	115
486	→	878
835	→	822
2983	→	1011
2338	→	9
2979	→	2286
789	→	913
1057	→	10
1057	→	1145
1057	→	1973
2367	→	1111
750	→	741
1406	→	1396
1406	→	1893
1845	→	885
1845	→	2034
1905	→	1897
2340	→	9
2605	→	635
2605	→	2714
860	→	341
967	→	1732
2629	→	197
2641	→	821
2443	→	1111
2443	→	2736
1156	→	2446
1109	→	1081
794	→	1480
794	→	2117
2769	→	1081
2773	→	9
897	→	674
1475	→	493
1475	→	538
1475	→	331
1475	→	146
1475	→	85
1475	→	225
1475	→	444
1475	→	2
1475	→	521
1142	→	1123
1288	→	2506
1288	→	2622
1288	→	2644
2518	→	2821
1166	→	2744
2297	→	10
2297	→	2394
2297	→	2687
273	→	3
273	→	952
273	→	682
273	→	680
273	→	9
273	→	874
273	→	86
273	→	187
273	→	678
273	→	872
273	→	64
273	→	116
273	→	2987
742	→	1759
2509	→	264
2385	→	1111
1966	→	811
1966	→	652
1966	→	356
1966	→	707
1966	→	264
1966	→	540
1966	→	263
1966	→	165
1966	→	8
1966	→	242
1966	→	446
1966	→	5
1966	→	650
1966	→	807
1966	→	332
2116	→	995
2317	→	1081
2394	→	2742
1733	→	1716
294	→	264
294	→	646
294	→	697
294	→	786
294	→	716
294	→	891
294	→	540
294	→	263
294	→	165
294	→	8
294	→	242
294	→	446
294	→	5
294	→	912
294	→	648
294	→	809
294	→	312
1250	→	2263
2507	→	264
2603	→	635
2603	→	2712
374	→	2689
933	→	1482
933	→	2119
1073	→	9
2647	→	821
2647	→	2679
882	→	674
1972	→	1958
1593	→	1575
2146	→	2302
2146	→	2339
2146	→	2366
2146	→	2400
2146	→	2573
2146	→	2579
2146	→	2608
2146	→	2636
628	→	779
628	→	1431
1008	→	996
2858	→	17
706	→	5
706	→	811
706	→	652
706	→	356
706	→	716
706	→	264
706	→	891
706	→	912
706	→	648
706	→	809
706	→	312
502	→	1
502	→	852
502	→	393
502	→	197
502	→	226
502	→	665
502	→	836
502	→	559
502	→	663
502	→	579
502	→	245
502	→	603
502	→	262
502	→	613
502	→	884
502	→	2490
502	→	2627
502	→	2501
502	→	2882
1625	→	2616
1625	→	2708
1625	→	2980
145	→	115
145	→	740
145	→	832
145	→	890
145	→	995
2866	→	635
2866	→	2982
461	→	484
461	→	620
461	→	1503
461	→	1562
122	→	1035
2242	→	1028
2574	→	404
1825	→	123
491	→	341
491	→	1393
1724	→	2318
1724	→	2335
1724	→	2384
1724	→	2392
1724	→	2567
1724	→	2606
1724	→	2634
18	→	1
18	→	226
18	→	953
18	→	224
18	→	2286
18	→	942
18	→	834
18	→	115
18	→	2639
365	→	1
365	→	665
365	→	852
365	→	393
365	→	197
365	→	836
365	→	732
365	→	559
365	→	581
365	→	245
365	→	603
365	→	262
365	→	613
365	→	955
365	→	884
365	→	954
365	→	2490
365	→	195
365	→	2503
365	→	2627
365	→	2501
365	→	822
365	→	835
365	→	2880
365	→	2882
978	→	1201
226	→	197
226	→	1755
1118	→	2748
643	→	123
2588	→	2750
3	→	61
3	→	167
3	→	223
3	→	291
3	→	458
3	→	556
1362	→	404
1483	→	1466
653	→	636
812	→	787
2684	→	937
1289	→	852
1289	→	393
1289	→	197
1289	→	520
1289	→	293
1289	→	125
1289	→	37
1289	→	261
1289	→	425
1289	→	1
1289	→	226
626	→	193
406	→	1246
1119	→	2442
1119	→	2772
1119	→	2799
1119	→	2815
1119	→	2847
1119	→	2859
1119	→	2867
1119	→	2915
2980	→	2988
2980	→	2990
2678	→	921
411	→	122
919	→	2
919	→	493
919	→	485
919	→	1392
9	→	682
9	→	876
9	→	952
647	→	636
2437	→	1111
5	→	8
5	→	165
5	→	242
5	→	263
5	→	446
5	→	540
147	→	115
147	→	749
147	→	898
147	→	1005
147	→	522
147	→	311
147	→	144
147	→	63
147	→	196
147	→	427
147	→	4
147	→	863
147	→	1111
147	→	2453
1200	→	948
2703	→	197
341	→	1263
341	→	1548
341	→	1715
37	→	2294
1778	→	1760
642	→	1212
642	→	1433
642	→	1455
642	→	2314
642	→	2360
642	→	2372
2685	→	2768
2685	→	2805
2685	→	2807
2685	→	2817
2281	→	1036
1076	→	2288
1071	→	9
1055	→	1036
2289	→	1036
2627	→	197
2672	→	2661
2568	→	404
1252	→	952
1252	→	682
1252	→	680
1252	→	3
1252	→	9
1252	→	874
1252	→	86
1252	→	1936
1252	→	1938
891	→	1848
2409	→	1111
2505	→	264
1220	→	341
2615	→	194
2361	→	9
243	→	197
756	→	741
2707	→	995
1929	→	2440
889	→	400
3002	→	2975
2311	→	1044
193	→	1525
445	→	404
2989	→	1081
1890	→	921
224	→	197
2520	→	665
2520	→	836
2520	→	333
2520	→	245
2520	→	559
2520	→	1
2520	→	732
2520	→	581
2520	→	603
2520	→	2490
2520	→	2503
2520	→	1755
2520	→	2880
2520	→	226
2520	→	195
2949	→	2934
62	→	9
2373	→	1111
2566	→	404
1599	→	393
2613	→	194
1341	→	2700
2118	→	995
2470	→	1111
1034	→	819
1758	→	837
2057	→	2650
2059	→	2685
2969	→	197
1	→	37
1	→	125
1	→	261
1	→	293
1	→	425
1	→	520
1936	→	936
40	→	9
40	→	667
40	→	861
123	→	1056
123	→	1076
123	→	1095
123	→	1147
123	→	1367
123	→	1461
123	→	1592
1077	→	9
1077	→	676
1077	→	394
1077	→	3
1077	→	870
1077	→	38
1077	→	2287
2749	→	9
2676	→	2661
1430	→	561
2701	→	2690
2295	→	1036
1902	→	2618
1902	→	2710
1443	→	630
1010	→	996
1010	→	1405
1019	→	4
1019	→	1009
1019	→	911
1019	→	755
1019	→	898
1019	→	115
1019	→	494
1019	→	749
1019	→	1005
1019	→	147
1019	→	1111
1019	→	2453
1026	→	819
1591	→	1575
877	→	862
877	→	935
936	→	2103
2614	→	2879
2472	→	117
739	→	6
739	→	971
739	→	426
739	→	731
739	→	198
739	→	445
739	→	2489
739	→	1476
739	→	1010
739	→	194
739	→	2613
2846	→	404
977	→	271
901	→	891
833	→	822
1004	→	996
1004	→	1403
332	→	264
332	→	650
332	→	707
332	→	807
601	→	559
601	→	654
969	→	1943
1626	→	1009
1626	→	911
1626	→	755
1626	→	898
1626	→	115
1626	→	4
1626	→	494
1626	→	749
1626	→	1005
1626	→	147
1626	→	1111
1626	→	2453
2682	→	927
1317	→	665
1317	→	852
1317	→	393
1317	→	197
1317	→	836
1317	→	732
1317	→	520
1317	→	293
1317	→	125
1317	→	37
1317	→	261
1317	→	425
1317	→	1
1317	→	559
1317	→	581
1317	→	245
1317	→	603
1317	→	2490
1317	→	1755
1317	→	226
1317	→	195
1317	→	2503
1317	→	2880
490	→	1359
490	→	1380
490	→	1598
490	→	1824
490	→	2162
1922	→	927
2037	→	957
334	→	962
334	→	2956
1938	→	936
2860	→	17
2424	→	1963
197	→	333
197	→	393
197	→	612
197	→	852
342	→	1
342	→	852
342	→	393
342	→	197
342	→	226
342	→	665
342	→	836
342	→	559
342	→	663
342	→	579
342	→	245
342	→	603
2918	→	1620
2918	→	2931
428	→	404
428	→	600
426	→	404
426	→	580
1342	→	852
1342	→	393
1342	→	197
1342	→	1
1342	→	953
1342	→	224
1342	→	2286
1342	→	942
1342	→	834
1342	→	115
1342	→	2639
1213	→	1957
1213	→	2722
2503	→	2490
677	→	668
402	→	2
402	→	493
402	→	521
402	→	837
402	→	539
402	→	943
402	→	523
402	→	485
402	→	1392
402	→	1758
970	→	6
970	→	602
970	→	578
970	→	404
970	→	459
970	→	2576
2395	→	116
748	→	738
2978	→	3005
2800	→	1081
1366	→	404
2972	→	2992
634	→	501
2451	→	1111
261	→	2500
261	→	2612
261	→	2704
2711	→	995
38	→	9
38	→	676
38	→	870
38	→	680
38	→	3
38	→	874
38	→	86
38	→	1938
2717	→	1011
86	→	9
86	→	680
86	→	874
2951	→	922
675	→	401
2715	→	1011
1729	→	1716
556	→	2341
556	→	2345
556	→	2402
556	→	2425
556	→	2575
556	→	2610
556	→	2638
2916	→	115
662	→	2
662	→	493
662	→	521
1157	→	875
1157	→	877
1157	→	2104
1402	→	852
1402	→	393
1402	→	197
1402	→	520
1402	→	293
1402	→	125
1402	→	37
1402	→	261
1402	→	425
1402	→	1
1402	→	226
2214	→	933
2609	→	635
2609	→	2718
1766	→	665
1766	→	852
1766	→	393
1766	→	197
1766	→	836
1766	→	559
1766	→	520
1766	→	293
1766	→	125
1766	→	37
1766	→	261
1766	→	425
1766	→	1
1766	→	663
1766	→	579
1766	→	245
1766	→	603
2348	→	1081
619	→	92
1170	→	1111
912	→	891
912	→	1046
1214	→	2471
493	→	1937
1944	→	935
2319	→	1081
540	→	2448
2688	→	943
2155	→	2139
1310	→	1676
1358	→	396
788	→	2210
2698	→	2885
2698	→	2919
679	→	668
2092	→	197
810	→	787
810	→	2065
1855	→	16
1855	→	1921
1477	→	1466
6	→	39
6	→	114
6	→	244
6	→	313
6	→	403
6	→	492
1075	→	9
2653	→	893
2798	→	1081
1053	→	226
1053	→	1
2499	→	1936
2499	→	1938
1256	→	1308
1256	→	1333
1256	→	2052
404	→	460
404	→	602
404	→	1391
116	→	187
116	→	1283
116	→	952
116	→	682
116	→	678
116	→	3
116	→	9
116	→	872
116	→	64
116	→	676
116	→	394
116	→	870
116	→	38
116	→	2287
116	→	1112
116	→	2295
2735	→	1038
2985	→	1011
468	→	364
1456	→	635
741	→	1027
1853	→	493
1853	→	538
1853	→	331
1853	→	146
1853	→	85
1853	→	225
1853	→	444
1853	→	2
1853	→	485
1853	→	1392
2743	→	1036
1438	→	2510
1438	→	2640
2745	→	9
2637	→	115
1092	→	1081
1824	→	2278
394	→	627
124	→	2
124	→	557
124	→	875
124	→	877
124	→	539
124	→	521
124	→	837
124	→	1756
522	→	2454
1585	→	1575
2987	→	9
1364	→	404
2153	→	2139
292	→	264
613	→	883
613	→	1844
613	→	2624
1168	→	877
1168	→	871
1168	→	493
1168	→	85
1168	→	225
1168	→	444
1168	→	538
1168	→	331
1168	→	146
1168	→	2
1168	→	875
1168	→	557
1168	→	2104
565	→	363
368	→	1631
2932	→	914
1146	→	1123
2035	→	1025
264	→	356
264	→	366
264	→	652
264	→	718
264	→	811
538	→	2452
2287	→	1036
2287	→	116
2287	→	2987
831	→	822
2403	→	115
204	→	1054
3008	→	1036
2611	→	635
2611	→	2720
717	→	698
2713	→	1011
951	→	5
951	→	811
951	→	652
951	→	356
951	→	707
951	→	264
951	→	650
951	→	807
951	→	332
853	→	1429
2816	→	115
873	→	862
2723	→	1027
2248	→	1030
2981	→	8
808	→	787
808	→	2067
2	→	85
2	→	146
2	→	225
2	→	331
2	→	444
2	→	538
863	→	2101
2161	→	2139
787	→	926
2919	→	3003
11	→	87
11	→	1442
4	→	63
4	→	144
4	→	196
4	→	311
4	→	427
4	→	522
941	→	674
1291	→	336
2379	→	1111
2705	→	995
1392	→	485
1018	→	1074
1018	→	1091
1018	→	1110
1018	→	1143
1018	→	1365
1018	→	1459
1018	→	1590
1018	→	2590
1504	→	461
876	→	2438
2874	→	197
3004	→	197
827	→	499
557	→	493
557	→	85
557	→	225
557	→	444
557	→	538
557	→	331
557	→	146
557	→	2
843	→	364
501	→	1070
501	→	1080
501	→	1121
501	→	1158
501	→	1363
501	→	1457
501	→	1584
1222	→	1215
1404	→	1396
520	→	2469
2709	→	995
580	→	2502
580	→	2614
580	→	2706
425	→	2626
959	→	1465
754	→	741
2721	→	1011
820	→	4
820	→	920
820	→	1009
820	→	911
820	→	755
820	→	900
820	→	751
820	→	115
820	→	821
820	→	1007
820	→	166
820	→	367
820	→	147
820	→	494
820	→	890
820	→	740
820	→	756
820	→	832
820	→	995
820	→	145
820	→	2455
2453	→	1111
1535	→	971
1535	→	426
1535	→	492
1535	→	313
1535	→	114
1535	→	39
1535	→	244
1535	→	403
1535	→	6
1535	→	731
1535	→	198
1535	→	2489
1535	→	1476
1535	→	1010
1535	→	194
1535	→	2613
2876	→	197
1390	→	955
1390	→	884
2991	→	1111
2147	→	1009
2147	→	911
2147	→	755
2147	→	898
2147	→	115
2147	→	4
2147	→	494
2147	→	749
2147	→	1005
2147	→	147
2147	→	1111
2147	→	2453
1059	→	10
1059	→	1141
1059	→	1979
2957	→	927
795	→	4
795	→	1009
795	→	911
795	→	755
795	→	898
795	→	115
795	→	494
795	→	749
795	→	1005
795	→	147
795	→	1111
795	→	2453
1334	→	2652
1045	→	226
1045	→	224
1045	→	953
1045	→	395
1045	→	2286
1045	→	942
1045	→	834
1045	→	115
1045	→	838
1045	→	2639
93	→	17
93	→	1856
2346	→	1081
2884	→	197
2607	→	635
2607	→	2716
357	→	1011
925	→	888
738	→	1854
2576	→	404
3005	→	3007
581	→	559
581	→	852
581	→	393
581	→	197
581	→	520
581	→	293
581	→	125
581	→	37
581	→	261
581	→	425
581	→	1
581	→	245
2619	→	194
559	→	836
2810	→	115
1901	→	2600
1458	→	635
1458	→	1618
1458	→	2152
1533	→	2671
708	→	698
708	→	1904
2639	→	115
335	→	2917
1432	→	616
2617	→	194
944	→	2683
2315	→	1081
1543	→	1526
1543	→	1838
1623	→	2970
2264	→	1036
1006	→	996
1006	→	1777
1632	→	1621
1401	→	2316
1401	→	2320
1401	→	2378
1401	→	2386
1401	→	2565
1401	→	2604
1401	→	2632
1943	→	2436
2914	→	115
1980	→	1958
2387	→	115
2439	→	1111
2771	→	9
934	→	2
934	→	493
934	→	943
934	→	523
1563	→	744
1563	→	2077
1765	→	2504
1765	→	2620
1765	→	2642
126	→	115
126	→	830
960	→	1255
960	→	1542
960	→	1728
885	→	2036
719	→	698
64	→	9
64	→	678
64	→	872
2163	→	2138
681	→	668
1122	→	1971
1122	→	2241
1316	→	2702
579	→	559
579	→	663
2621	→	197
752	→	741
1756	→	837
1541	→	1526
2737	→	1038
2655	→	16
2655	→	2681
115	→	755
115	→	834
115	→	911
115	→	942
115	→	1009
115	→	2286
1090	→	953
1090	→	852
1090	→	393
1090	→	197
1090	→	395
1090	→	224
1090	→	2286
1090	→	942
1090	→	834
1090	→	115
1090	→	2639
2623	→	197
198	→	731
198	→	971
198	→	426
198	→	2489
198	→	1476
198	→	194
198	→	2613
1128	→	784
245	→	197
245	→	1757
1725	→	262
1725	→	613
1725	→	884
1725	→	2490
1725	→	2627
1725	→	2501
1725	→	2882
683	→	668
683	→	978
1894	→	923
2651	→	821
945	→	1190
1569	→	743
2342	→	9
2699	→	971
2699	→	426
2699	→	731
2699	→	198
2699	→	1010
651	→	636
1549	→	197
1583	→	115
1439	→	490
1502	→	1261
2068	→	964
1144	→	1122
2447	→	1111
168	→	115
168	→	753
168	→	828
168	→	902
168	→	1003
2401	→	115
2643	→	821
1464	→	635
1464	→	2138
666	→	655
664	→	655
462	→	1501
206	→	3
206	→	952
206	→	682
206	→	680
206	→	9
206	→	874
206	→	86
206	→	676
206	→	394
206	→	870
206	→	38
206	→	1936
206	→	1938
206	→	2287
2279	→	1036
1847	→	894
492	→	2450
1474	→	2508
1474	→	2628
1474	→	2646
2286	→	2986
2670	→	485
2612	→	2881
1266	→	1256
1368	→	404
2519	→	2873
521	→	493
521	→	1935
1682	→	366
2078	→	194
2920	→	194
1360	→	404
2848	→	404
829	→	822
523	→	493
523	→	1846
340	→	2933
2880	→	197
2806	→	9
1445	→	9
1264	→	1256
2601	→	9
1120	→	873
1120	→	877
1120	→	493
1120	→	979
1120	→	85
1120	→	225
1120	→	444
1120	→	538
1120	→	331
1120	→	146
1120	→	2
1120	→	871
1120	→	875
1120	→	557
1120	→	2104
1120	→	539
1120	→	981
953	→	1357
649	→	636
1002	→	204
932	→	1444
92	→	2675
358	→	813
1028	→	2247
1903	→	493
1903	→	2
1903	→	943
1903	→	523
375	→	1
375	→	852
375	→	393
375	→	197
375	→	953
375	→	224
375	→	2286
375	→	942
375	→	834
375	→	115
375	→	2639
541	→	493
2426	→	1111
2102	→	121
195	→	1
195	→	333
195	→	612
195	→	226
195	→	836
195	→	559
195	→	245
195	→	665
195	→	603
903	→	891
1251	→	2296
1251	→	2337
1251	→	2347
1251	→	2408
1251	→	2561
1251	→	2602
1251	→	2630
2560	→	1118
367	→	920
367	→	1290
367	→	1009
367	→	911
367	→	755
367	→	900
367	→	751
367	→	4
367	→	115
367	→	821
367	→	1007
367	→	166
367	→	1111
367	→	2449
1481	→	1466
1930	→	935
961	→	6
961	→	971
961	→	426
961	→	731
961	→	198
961	→	1010
2686	→	37
1716	→	1889
785	→	272
785	→	1929
2591	→	2580
194	→	1476
194	→	2115
194	→	2489
2104	→	862
603	→	559
603	→	665
1211	→	981
1857	→	16
1857	→	1895
2066	→	964
2449	→	1111
875	→	862
2631	→	115
447	→	404
447	→	558
447	→	1919
1167	→	2444
1167	→	2770
1167	→	2797
1167	→	2809
1167	→	2845
1167	→	2857
1167	→	2865
1167	→	2913
166	→	115
166	→	751
166	→	821
166	→	900
166	→	1007
984	→	784
1920	→	928
737	→	2660
539	→	493
2886	→	197
2719	→	1011
2882	→	197
1123	→	1221
2060	→	602
2060	→	578
2060	→	6
2060	→	404
2060	→	459
2060	→	2576
2822	→	92
2822	→	2968
996	→	1568
2336	→	9
2589	→	1762
262	→	197
262	→	226
262	→	37
262	→	261
262	→	425
262	→	520
262	→	293
262	→	125
262	→	1
2455	→	1111
312	→	264
312	→	648
312	→	716
312	→	809
2120	→	995
1096	→	1081
1460	→	635
1460	→	2154
1381	→	2553
661	→	1265
661	→	1540
661	→	1730
2633	→	115
1262	→	92
2616	→	2883
2808	→	1111
2943	→	485
2943	→	1392
2635	→	115
1462	→	635
1462	→	2160
2445	→	1111
2445	→	2734
2562	→	404
1960	→	2414
459	→	404
459	→	578
1731	→	1716
2321	→	9
1534	→	2654
2680	→	921
963	→	1020
1974	→	1958
2₁(1031)	→	1032
2₁(911)	→	912
2₁(1457)	→	1458
2₁(293)	→	294
2₁(1287)	→	1288
2₁(187)	→	188
2₁(2504)	→	2505
2₁(487)	→	488
2₁(1897)	→	1898
2₁(1579)	→	1580
2₁(200)	→	201
2₁(291)	→	292
2₁(313)	→	314
2₁(1047)	→	1048
2₁(928)	→	929
2₁(263)	→	264
2₁(1285)	→	1286
2₁(10)	→	11
2₁(1316)	→	1317
2₁(703)	→	704
2₁(2213)	→	2214
2₁(190)	→	191
2₁(2867)	→	2868
2₁(562)	→	563
2₁(895)	→	896
2₁(466)	→	467
2₁(887)	→	888
2₁(410)	→	411
2₁(1578)	→	1579
2₁(671)	→	672
2₁(2162)	→	2163
2₁(962)	→	963
2₁(1048)	→	1049
2₁(1221)	→	1222
2₁(633)	→	634
2₁(1435)	→	1436
2₁(1024)	→	1025
2₁(398)	→	399
2₁(1214)	→	1215
2₁(91)	→	92
2₁(2606)	→	2607
2₁(2873)	→	2874
2₁(1263)	→	1264
2₁(786)	→	787
2₁(791)	→	792
2₁(913)	→	914
2₁(2054)	→	2055
2₁(1461)	→	1462
2₁(1455)	→	1456
2₁(2654)	→	2655
2₁(807)	→	808
2₁(401)	→	402
2₁(1676)	→	1677
2₁(964)	→	965
2₁(338)	→	339
2₁(2077)	→	2078
2₁(462)	→	463
2₁(1844)	→	1845
2₁(2865)	→	2866
2₁(2506)	→	2507
2₁(814)	→	815
2₁(1459)	→	1460
2₁(733)	→	734
2₁(120)	→	121
2₁(1846)	→	1847
2₁(841)	→	842
2₁(497)	→	498
2₁(890)	→	891
2₁(1854)	→	1855
2₁(357)	→	358
2₁(955)	→	956
2₁(1265)	→	1266
2₁(2604)	→	2605
2₁(780)	→	781
2₁(1255)	→	1256
2₁(364)	→	365
2₁(2608)	→	2609
2₁(340)	→	341
2₁(1259)	→	1260
2₁(705)	→	706
2₁(496)	→	497
2₁(1622)	→	1623
2₁(1463)	→	1464
2₁(902)	→	903
2₁(809)	→	810
2₁(1396)	→	1397
2₁(1529)	→	1530
2₁(87)	→	88
2₁(311)	→	312
2₁(2247)	→	2248
2₁(2931)	→	2932
2₁(620)	→	621
2₁(1127)	→	1128
2₁(12)	→	13
2₁(900)	→	901
2₁(92)	→	93
2₁(1677)	→	1678
2₁(13)	→	14
2₁(1856)	→	1857
2₁(1001)	→	1002
2₁(1246)	→	1247
2₁(2210)	→	2211
2₁(660)	→	661
2₁(395)	→	396
2₁(893)	→	894
2₁(884)	→	885
2₁(1468)	→	1469
2₁(267)	→	268
2₁(813)	→	814
2₁(746)	→	747
2₁(975)	→	976
2₁(628)	→	629
2₁(737)	→	738
2₁(1357)	→	1358
2₁(2610)	→	2611
2₁(996)	→	997
2₁(1533)	→	1534
2₁(1021)	→	1022
2₁(331)	→	332
2₁(781)	→	782
2₁(1473)	→	1474
2₁(811)	→	812
2₁(2508)	→	2509
2₁(2052)	→	2053
2₁(489)	→	490
2₁(270)	→	271
2₁(1217)	→	1218
2₁(655)	→	656
2₁(898)	→	899
2₁(1397)	→	1398
2₁(333)	→	334
2₁(2602)	→	2603
2₁(1029)	→	1030
2₁(1309)	→	1310
1₂(2513)	→	2514
1₂(2939)	→	2940
1₂(2940)	→	2941
1₂(1119)	→	1120
1₂(2423)	→	2424
1₂(1167)	→	1168
1₂(2588)	→	2589
1₂(1199)	→	1200
1₂(2498)	→	2499
1₂(1156)	→	1157
1₂(2511)	→	2512
1₂(1210)	→	1211
1₂(2974)	→	2975
1₂(2972)	→	2973
2₂(2664)	→	2665
2₂(1196)	→	1197
2₂(2948)	→	2949
2₂(2660)	→	2661
2₂(2512)	→	2513
2₂(2933)	→	2934
2₂(1037)	→	1038
2₂(2510)	→	2511
2₂(2493)	→	2494
2₂(2671)	→	2672
2₂(2734)	→	2735
2₂(1039)	→	1040
2₂(2420)	→	2421
2₂(2751)	→	2752
2₂(2693)	→	2694
2₂(2519)	→	2520
2₂(2304)	→	2305
2₂(2736)	→	2737
2₂(1207)	→	1208
2₂(1088)	→	1089
2₂(2753)	→	2754
2₂(2942)	→	2943
2₂(2661)	→	2662
2₂(2309)	→	2310
2₂(1389)	→	1390
2₂(1164)	→	1165
2₂(2754)	→	2755
2₂(2675)	→	2676
2₂(2586)	→	2587
2₂(1153)	→	1154
2₂(1387)	→	1388
2₂(1040)	→	1041
2₂(1087)	→	1088
2₂(2305)	→	2306
2₂(1082)	→	1083
2₂(2559)	→	2560
2₂(2310)	→	2311
2₂(1083)	→	1084
2₂(1116)	→	1117
2₂(1383)	→	1384
3₂(2490)	→	2491
3₂(2517)	→	2518
3₂(2935)	→	2936
3₂(1205)	→	1206
3₂(1086)	→	1087
3₂(1162)	→	1163
3₂(1388)	→	1389
3₂(2941)	→	2942
3₂(1084)	→	1085
3₂(2579)	→	2580
3₂(2666)	→	2667
3₂(1380)	→	1381
3₂(1114)	→	1115
3₂(1151)	→	1152
3₂(1381)	→	1382
3₂(2418)	→	2419
3₂(2698)	→	2699
3₂(1194)	→	1195
3₂(2976)	→	2977
3₂(2306)	→	2307
3₂(2590)	→	2591
3₂(2308)	→	2309
4₃(2999)	→	3000
4₃(3000)	→	3001
4₃(2994)	→	2995
4₃(2993)	→	2994
1₁(1760)	→	1761
1₁(616)	→	617
1₁(618)	→	619
1₁(2652)	→	2653
1₁(1251)	→	1252
1₁(870)	→	871
1₁(1943)	→	1944
1₁(540)	→	541
1₁(1971)	→	1972
1₁(876)	→	877
1₁(1962)	→	1963
1₁(2718)	→	2719
1₁(1929)	→	1930
1₁(842)	→	843
1₁(356)	→	357
1₁(856)	→	857
1₁(874)	→	875
1₁(1470)	→	1471
1₁(868)	→	869
1₁(2152)	→	2153
1₁(1973)	→	1974
1₁(1718)	→	1719
1₁(978)	→	979
1₁(2714)	→	2715
1₁(2980)	→	2981
1₁(1310)	→	1311
1₁(492)	→	493
1₁(520)	→	521
1₁(861)	→	862
1₁(942)	→	943
1₁(1761)	→	1762
1₁(1391)	→	1392
1₁(1724)	→	1725
1₁(1979)	→	1980
1₁(2685)	→	2686
1₁(924)	→	925
1₁(642)	→	643
1₁(191)	→	192
1₁(2716)	→	2717
1₁(490)	→	491
1₁(947)	→	948
1₁(1401)	→	1402
1₁(888)	→	889
1₁(556)	→	557
1₁(484)	→	485
1₁(358)	→	359
1₁(1018)	→	1019
1₁(1901)	→	1902
1₁(2857)	→	2858
1₁(872)	→	873
1₁(123)	→	124
1₁(2146)	→	2147
1₁(2984)	→	2985
1₁(892)	→	893
1₁(2859)	→	2860
1₁(945)	→	946
1₁(932)	→	933
1₁(938)	→	939
1₁(732)	→	733
1₁(2103)	→	2104
1₁(2160)	→	2161
1₁(2138)	→	2139
1₁(1755)	→	1756
1₁(657)	→	658
1₁(823)	→	824
1₁(560)	→	561
1₁(1957)	→	1958
1₁(980)	→	981
1₁(2982)	→	2983
1₁(2687)	→	2688
1₁(1960)	→	1961
1₁(937)	→	938
1₁(2720)	→	2721
1₁(205)	→	206
1₁(894)	→	895
1₁(2712)	→	2713
1₁(1757)	→	1758
1₁(855)	→	856
1₁(538)	→	539
1₁(501)	→	502
1₁(1308)	→	1309
1₁(522)	→	523
1₁(1218)	→	1219
1₁(836)	→	837
1₁(1429)	→	1430
1₁(2154)	→	2155
1₁(1528)	→	1529
1₁(624)	→	625
2₀(3)	→	5
2₀(6)	→	5
2₀(5)	→	5
2₀(4)	→	5
2₀(2)	→	5
2₀(1)	→	5
0₃(2997)	→	2998
1₃(3001)	→	3002
3₀(2)	→	6
3₀(6)	→	6
3₀(4)	→	6
3₀(1)	→	6
3₀(3)	→	6
3₀(5)	→	6
5₂(2469)	→	2470
5₂(1150)	→	1151
5₂(2663)	→	2664
5₂(2440)	→	2441
5₂(1193)	→	1194
5₂(2438)	→	2439
5₂(1161)	→	1162
5₂(2491)	→	2492
5₂(1081)	→	1082
5₂(2417)	→	2418
5₂(2750)	→	2751
5₂(2450)	→	2451
5₂(1085)	→	1086
5₂(2696)	→	2697
5₂(1113)	→	1114
5₂(1043)	→	1044
5₂(2515)	→	2516
5₂(2307)	→	2308
5₂(1036)	→	1037
5₂(2495)	→	2496
5₂(2581)	→	2582
5₂(2414)	→	2415
5₂(2516)	→	2517
5₂(1190)	→	1191
5₂(2938)	→	2939
5₂(2366)	→	2367
5₂(2454)	→	2455
5₂(2807)	→	2808
5₂(1147)	→	1148
5₂(1044)	→	1045
5₂(1201)	→	1202
5₂(2554)	→	2555
5₂(2444)	→	2445
5₂(2975)	→	2976
5₂(1158)	→	1159
5₂(1089)	→	1090
5₂(2303)	→	2304
5₂(2442)	→	2443
5₂(2584)	→	2585
5₂(1204)	→	1205
5₂(2757)	→	2758
5₂(2372)	→	2373
5₂(2425)	→	2426
5₂(2436)	→	2437
5₂(2758)	→	2759
5₂(1169)	→	1170
5₂(2990)	→	2991
5₂(2668)	→	2669
5₂(2492)	→	2493
5₂(2452)	→	2453
5₂(2408)	→	2409
5₂(2580)	→	2581
5₂(2557)	→	2558
5₂(2384)	→	2385
5₂(2378)	→	2379
5₂(2934)	→	2935
5₂(2446)	→	2447
5₂(2448)	→	2449
5₂(2553)	→	2554
5₂(1110)	→	1111
5₂(2662)	→	2663
3₃(2996)	→	2997
5₀(1)	→	4
5₀(6)	→	4
5₀(3)	→	4
5₀(5)	→	4
5₀(2)	→	4
5₀(4)	→	4
5₁(822)	→	823
5₁(1143)	→	1144
5₁(125)	→	126
5₁(866)	→	867
5₁(939)	→	940
5₁(17)	→	18
5₁(704)	→	705
5₁(753)	→	754
5₁(1730)	→	1731
5₁(404)	→	405
5₁(1501)	→	1502
5₁(1058)	→	1059
5₁(614)	→	615
5₁(1020)	→	1021
5₁(1052)	→	1053
5₁(1728)	→	1729
5₁(1334)	→	1335
5₁(336)	→	337
5₁(192)	→	193
5₁(2241)	→	2242
5₁(740)	→	741
5₁(1313)	→	1314
5₁(2386)	→	2387
5₁(1260)	→	1261
5₁(1248)	→	1249
5₁(2646)	→	2647
5₁(498)	→	499
5₁(629)	→	630
5₁(500)	→	501
5₁(408)	→	409
5₁(1680)	→	1681
5₁(493)	→	494
5₁(117)	→	118
5₁(369)	→	370
5₁(2650)	→	2651
5₁(564)	→	565
5₁(202)	→	203
5₁(896)	→	897
5₁(146)	→	147
5₁(198)	→	199
5₁(2708)	→	2709
5₁(865)	→	866
5₁(373)	→	374
5₁(1257)	→	1258
5₁(1442)	→	1443
5₁(782)	→	783
5₁(1340)	→	1341
5₁(738)	→	739
5₁(360)	→	361
5₁(1023)	→	1024
5₁(2817)	→	2818
5₁(815)	→	816
5₁(936)	→	937
5₁(1576)	→	1577
5₁(917)	→	918
5₁(1017)	→	1018
5₁(2644)	→	2645
5₁(862)	→	863
5₁(1717)	→	1718
5₁(559)	→	560
5₁(2706)	→	2707
5₁(1056)	→	1057
5₁(167)	→	168
5₁(1121)	→	1122
5₁(2296)	→	2297
5₁(89)	→	90
5₁(2212)	→	2213
5₁(334)	→	335
5₁(2117)	→	2118
5₁(1681)	→	1682
5₁(9)	→	10
5₁(631)	→	632
5₁(817)	→	818
5₁(271)	→	272
5₁(1338)	→	1339
5₁(1393)	→	1394
5₁(16)	→	17
5₁(2815)	→	2816
5₁(788)	→	789
5₁(2642)	→	2643
5₁(2809)	→	2810
5₁(165)	→	166
5₁(1723)	→	1724
5₁(1027)	→	1028
5₁(701)	→	702
5₁(1965)	→	1966
5₁(755)	→	756
5₁(879)	→	880
5₁(1336)	→	1337
5₁(2722)	→	2723
5₁(2119)	→	2120
5₁(1028)	→	1029
5₁(958)	→	959
5₁(891)	→	892
5₁(670)	→	671
5₁(1398)	→	1399
5₁(2710)	→	2711
5₁(2640)	→	2641
5₁(819)	→	820
5₁(640)	→	641
5₁(998)	→	999
5₁(1212)	→	1213
5₁(2145)	→	2146
5₁(787)	→	788
5₁(367)	→	368
5₁(2917)	→	2918
5₁(2115)	→	2116
5₁(144)	→	145
5₁(1715)	→	1716
5₁(114)	→	115
5₁(627)	→	628
5₁(1400)	→	1401
5₁(2704)	→	2705
5₁(863)	→	864
5₁(2683)	→	2684
5₁(361)	→	362
5₁(668)	→	669
5₁(1051)	→	1052
5₁(2402)	→	2403
5₁(1312)	→	1313
5₁(405)	→	406
5₁(1534)	→	1535
5₁(880)	→	881
5₁(923)	→	924
5₁(1851)	→	1852
5₁(1333)	→	1334
5₁(199)	→	200
5₁(885)	→	886
5₁(1678)	→	1679
5₁(999)	→	1000
5₁(366)	→	367
5₁(950)	→	951
5₁(268)	→	269
5₁(783)	→	784
5₁(1124)	→	1125
5₁(265)	→	266
5₁(852)	→	853
5₁(1619)	→	1620
5₁(1219)	→	1220
5₁(1581)	→	1582
5₁(1580)	→	1581
5₁(1283)	→	1284
5₁(751)	→	752
5₁(674)	→	675
5₁(981)	→	982
5₁(1618)	→	1619
5₁(818)	→	819
5₁(2400)	→	2401
5₁(641)	→	642
5₁(1732)	→	1733
5₁(2392)	→	2393
5₁(371)	→	372
5₁(749)	→	750
5₁(838)	→	839
4₁(2143)	→	2144
4₁(1339)	→	1340
4₁(1033)	→	1034
4₁(393)	→	394
4₁(2058)	→	2059
4₁(948)	→	949
4₁(2600)	→	2601
4₁(1050)	→	1051
4₁(2053)	→	2054
4₁(935)	→	936
4₁(368)	→	369
4₁(121)	→	122
4₁(1937)	→	1938
4₁(779)	→	780
4₁(927)	→	928
4₁(1072)	→	1073
4₁(2059)	→	2060
4₁(407)	→	408
4₁(2065)	→	2066
4₁(1721)	→	1722
4₁(2986)	→	2987
4₁(1444)	→	1445
4₁(335)	→	336
4₁(2144)	→	2145
4₁(669)	→	670
4₁(1141)	→	1142
4₁(2360)	→	2361
4₁(485)	→	486
4₁(1935)	→	1936
4₁(2748)	→	2749
4₁(1016)	→	1017
4₁(2320)	→	2321
4₁(1961)	→	1962
4₁(396)	→	397
4₁(1958)	→	1959
4₁(2339)	→	2340
4₁(792)	→	793
4₁(1777)	→	1778
4₁(2805)	→	2806
4₁(1577)	→	1578
4₁(61)	→	62
4₁(1722)	→	1723
4₁(463)	→	464
4₁(1919)	→	1920
4₁(968)	→	969
4₁(1256)	→	1257
4₁(983)	→	984
4₁(1959)	→	1960
4₁(969)	→	970
4₁(667)	→	668
4₁(916)	→	917
4₁(2211)	→	2212
4₁(2335)	→	2336
4₁(1335)	→	1336
4₁(1247)	→	1248
4₁(1070)	→	1071
4₁(676)	→	677
4₁(1213)	→	1214
4₁(854)	→	855
4₁(1850)	→	1851
4₁(2471)	→	2472
4₁(1963)	→	1964
4₁(499)	→	500
4₁(1964)	→	1965
4₁(85)	→	86
4₁(1341)	→	1342
4₁(943)	→	944
4₁(793)	→	794
4₁(1145)	→	1146
4₁(1720)	→	1721
4₁(613)	→	614
4₁(1582)	→	1583
4₁(63)	→	64
4₁(1015)	→	1016
4₁(2141)	→	2142
4₁(201)	→	202
4₁(1759)	→	1760
4₁(1623)	→	1624
4₁(944)	→	945
4₁(784)	→	785
4₁(2394)	→	2395
4₁(2341)	→	2342
4₁(940)	→	941
4₁(2067)	→	2068
4₁(1893)	→	1894
4₁(886)	→	887
4₁(3005)	→	3006
4₁(1022)	→	1023
4₁(372)	→	373
4₁(1848)	→	1849
4₁(37)	→	38
4₁(1399)	→	1400
4₁(700)	→	701
4₁(374)	→	375
4₁(1122)	→	1123
4₁(2772)	→	2773
4₁(122)	→	123
4₁(918)	→	919
4₁(949)	→	950
4₁(878)	→	879
4₁(116)	→	117
4₁(264)	→	265
4₁(1290)	→	1291
4₁(461)	→	462
4₁(8)	→	9
4₁(1852)	→	1853
4₁(1250)	→	1251
4₁(2744)	→	2745
4₁(1076)	→	1077
4₁(946)	→	947
4₁(825)	→	826
4₁(406)	→	407
4₁(1074)	→	1075
4₁(979)	→	980
4₁(1624)	→	1625
4₁(115)	→	116
4₁(272)	→	273
4₁(826)	→	827
4₁(963)	→	964
4₁(39)	→	40
4₁(747)	→	748
4₁(914)	→	915
4₁(922)	→	923
4₁(1013)	→	1014
4₁(1123)	→	1124
4₁(15)	→	16
4₁(678)	→	679
4₁(680)	→	681
4₁(1575)	→	1576
4₁(2337)	→	2338
4₁(2770)	→	2771
4₁(204)	→	205
4₁(682)	→	683
4₁(1824)	→	1825
4₁(1896)	→	1897
4₁(1904)	→	1905
1₀(3)	→	2
1₀(5)	→	2
1₀(2)	→	2
1₀(4)	→	2
1₀(1)	→	2
1₀(6)	→	2
4₀(2)	→	3
4₀(4)	→	3
4₀(3)	→	3
4₀(6)	→	3
4₀(1)	→	3
4₀(5)	→	3
0₁(816)	→	817
0₁(1311)	→	1312
0₁(1621)	→	1622
0₁(745)	→	746
0₁(832)	→	833
0₁(821)	→	822
0₁(225)	→	226
0₁(1548)	→	1549
0₁(2632)	→	2633
0₁(1562)	→	1563
0₁(1574)	→	1575
0₁(1598)	→	1599
0₁(933)	→	934
0₁(615)	→	616
0₁(1030)	→	1031
0₁(1403)	→	1404
0₁(1584)	→	1585
0₁(2636)	→	2637
0₁(399)	→	400
0₁(731)	→	732
0₁(790)	→	791
0₁(652)	→	653
0₁(1216)	→	1217
0₁(650)	→	651
0₁(1025)	→	1026
0₁(834)	→	835
0₁(1590)	→	1591
0₁(2139)	→	2140
0₁(1625)	→	1626
0₁(1469)	→	1470
0₁(2628)	→	2629
0₁(3003)	→	3004
0₁(394)	→	395
0₁(1046)	→	1047
0₁(622)	→	623
0₁(957)	→	958
0₁(2056)	→	2057
0₁(966)	→	967
0₁(1716)	→	1717
0₁(2034)	→	2035
0₁(952)	→	953
0₁(1530)	→	1531
0₁(1592)	→	1593
0₁(2950)	→	2951
0₁(636)	→	637
0₁(648)	→	649
0₁(189)	→	190
0₁(828)	→	829
0₁(223)	→	224
0₁(409)	→	410
0₁(974)	→	975
0₁(837)	→	838
0₁(1762)	→	1763
0₁(578)	→	579
0₁(2630)	→	2631
0₁(580)	→	581
0₁(2915)	→	2916
0₁(976)	→	977
0₁(954)	→	955
0₁(1542)	→	1543
0₁(1631)	→	1632
0₁(1395)	→	1396
0₁(612)	→	613
0₁(1902)	→	1903
0₁(2913)	→	2914
0₁(1540)	→	1541
0₁(734)	→	735
0₁(2883)	→	2884
0₁(656)	→	657
0₁(261)	→	262
0₁(359)	→	360
0₁(600)	→	601
0₁(1011)	→	1012
0₁(203)	→	204
0₁(1049)	→	1050
0₁(654)	→	655
0₁(242)	→	243
0₁(196)	→	197
0₁(14)	→	15
0₁(1838)	→	1839
0₁(119)	→	120
0₁(2638)	→	2639
0₁(744)	→	745
0₁(794)	→	795
0₁(2626)	→	2627
0₁(2634)	→	2635
0₁(663)	→	664
0₁(921)	→	922
0₁(1315)	→	1316
0₁(1431)	→	1432
0₁(883)	→	884
0₁(857)	→	858
0₁(1249)	→	1250
0₁(1337)	→	1338
0₁(2821)	→	2822
0₁(1527)	→	1528
0₁(840)	→	841
0₁(673)	→	674
0₁(743)	→	744
0₁(1126)	→	1127
0₁(269)	→	270
0₁(2036)	→	2037
0₁(11)	→	12
0₁(2875)	→	2876
0₁(702)	→	703
0₁(244)	→	245
0₁(1679)	→	1680
0₁(2881)	→	2882
0₁(1620)	→	1621
0₁(953)	→	954
0₁(2879)	→	2880
0₁(1467)	→	1468
0₁(602)	→	603
0₁(464)	→	465
0₁(2620)	→	2621
0₁(1900)	→	1901
0₁(646)	→	647
0₁(830)	→	831
0₁(1466)	→	1467
0₁(956)	→	957
0₁(370)	→	371
0₁(2885)	→	2886
0₁(1261)	→	1262
0₁(1525)	→	1526
0₁(194)	→	195
0₁(617)	→	618
0₁(495)	→	496
0₁(931)	→	932
0₁(789)	→	790
0₁(465)	→	466
0₁(635)	→	636
0₁(1437)	→	1438
0₁(558)	→	559
0₁(658)	→	659
0₁(363)	→	364
0₁(1471)	→	1472
0₁(2622)	→	2623
0₁(665)	→	666
0₁(1405)	→	1406
0₁(959)	→	960
2₃(2998)	→	2999
3₁(2573)	→	2574
3₁(403)	→	404
3₁(337)	→	338
3₁(2616)	→	2617
3₁(1359)	→	1360
3₁(1365)	→	1366
3₁(266)	→	267
3₁(699)	→	700
3₁(1472)	→	1473
3₁(929)	→	930
3₁(930)	→	931
3₁(362)	→	363
3₁(735)	→	736
3₁(1009)	→	1010
3₁(915)	→	916
3₁(1361)	→	1362
3₁(2968)	→	2969
3₁(1014)	→	1015
3₁(965)	→	966
3₁(867)	→	868
3₁(488)	→	489
3₁(1288)	→	1289
3₁(736)	→	737
3₁(2091)	→	2092
3₁(397)	→	398
3₁(960)	→	961
3₁(1215)	→	1216
3₁(188)	→	189
3₁(2142)	→	2143
3₁(2845)	→	2846
3₁(859)	→	860
3₁(1763)	→	1764
3₁(88)	→	89
3₁(1465)	→	1466
3₁(486)	→	487
3₁(1898)	→	1899
3₁(1003)	→	1004
3₁(2567)	→	2568
3₁(1438)	→	1439
3₁(494)	→	495
3₁(2612)	→	2613
3₁(444)	→	445
3₁(341)	→	342
3₁(1764)	→	1765
3₁(718)	→	719
3₁(1007)	→	1008
3₁(625)	→	626
3₁(716)	→	717
3₁(638)	→	639
3₁(2681)	→	2682
3₁(561)	→	562
3₁(2677)	→	2678
3₁(2140)	→	2141
3₁(1005)	→	1006
3₁(460)	→	461
3₁(1895)	→	1896
3₁(623)	→	624
3₁(920)	→	921
3₁(2919)	→	2920
3₁(858)	→	859
3₁(971)	→	972
3₁(2057)	→	2058
3₁(427)	→	428
3₁(1434)	→	1435
3₁(2565)	→	2566
3₁(1480)	→	1481
3₁(2679)	→	2680
3₁(1503)	→	1504
3₁(1482)	→	1483
3₁(1284)	→	1285
3₁(1719)	→	1720
3₁(1286)	→	1287
3₁(1032)	→	1033
3₁(1532)	→	1533
3₁(458)	→	459
3₁(2614)	→	2615
3₁(1889)	→	1890
3₁(2624)	→	2625
3₁(90)	→	91
3₁(1899)	→	1900
3₁(193)	→	194
3₁(967)	→	968
3₁(563)	→	564
3₁(824)	→	825
3₁(972)	→	973
3₁(1568)	→	1569
3₁(2561)	→	2562
3₁(425)	→	426
3₁(1476)	→	1477
3₁(118)	→	119
3₁(2956)	→	2957
3₁(632)	→	633
3₁(400)	→	401
3₁(1125)	→	1126
3₁(639)	→	640
3₁(1436)	→	1437
3₁(1474)	→	1475
3₁(697)	→	698
3₁(997)	→	998
3₁(1526)	→	1527
3₁(661)	→	662
3₁(1314)	→	1315
3₁(2702)	→	2703
3₁(2575)	→	2576
3₁(742)	→	743
3₁(1367)	→	1368
3₁(1433)	→	1434
3₁(339)	→	340
3₁(707)	→	708
3₁(864)	→	865
3₁(982)	→	983
3₁(741)	→	742
3₁(926)	→	927
3₁(2055)	→	2056
3₁(1258)	→	1259
3₁(637)	→	638
3₁(2847)	→	2848
3₁(197)	→	198
3₁(2618)	→	2619
3₁(1363)	→	1364
3₁(1765)	→	1766
3₁(1012)	→	1013
3₁(672)	→	673
3₁(621)	→	622
3₁(995)	→	996
3₁(1921)	→	1922
3₁(659)	→	660
3₁(881)	→	882
3₁(853)	→	854
3₁(698)	→	699
3₁(2101)	→	2102
3₁(1849)	→	1850
3₁(446)	→	447
3₁(1394)	→	1395
3₁(1000)	→	1001
3₁(973)	→	974
3₁(630)	→	631
3₁(1531)	→	1532
3₁(467)	→	468
3₁(839)	→	840
4₂(1192)	→	1193
4₂(2973)	→	2974
4₂(1203)	→	1204
4₂(2345)	→	2346
4₂(2756)	→	2757
4₂(2799)	→	2800
4₂(2286)	→	2287
4₂(2689)	→	2690
4₂(2988)	→	2989
4₂(2415)	→	2416
4₂(1166)	→	1167
4₂(1118)	→	1119
4₂(2665)	→	2666
4₂(2587)	→	2588
4₂(2556)	→	2557
4₂(1160)	→	1161
4₂(1165)	→	1166
4₂(2977)	→	2978
4₂(1198)	→	1199
4₂(2347)	→	2348
4₂(2555)	→	2556
4₂(1148)	→	1149
4₂(2669)	→	2670
4₂(1095)	→	1096
4₂(1191)	→	1192
4₂(2316)	→	2317
4₂(1208)	→	1209
4₂(2742)	→	2743
4₂(1091)	→	1092
4₂(2288)	→	2289
4₂(2421)	→	2422
4₂(2302)	→	2303
4₂(1080)	→	1081
4₂(2422)	→	2423
4₂(2971)	→	2972
4₂(1154)	→	1155
4₂(2970)	→	2971
4₂(1111)	→	1112
4₂(1042)	→	1043
4₂(1202)	→	1203
4₂(2768)	→	2769
4₂(2278)	→	2279
4₂(2294)	→	2295
4₂(2797)	→	2798
4₂(2667)	→	2668
4₂(2494)	→	2495
4₂(2280)	→	2281
4₂(2314)	→	2315
4₂(2497)	→	2498
4₂(1054)	→	1055
4₂(1112)	→	1113
4₂(1149)	→	1150
4₂(1108)	→	1109
4₂(2582)	→	2583
4₂(2416)	→	2417
4₂(1117)	→	1118
4₂(2700)	→	2701
4₂(2318)	→	2319
4₂(2263)	→	2264
4₂(1209)	→	1210
4₂(1159)	→	1160
4₂(1382)	→	1383
4₂(1035)	→	1036
4₂(2583)	→	2584
4₂(1384)	→	1385
4₂(2937)	→	2938
4₂(3007)	→	3008
4₂(1155)	→	1156
4₂(1197)	→	1198
4₂(2978)	→	2979
5₃(2995)	→	2996
5₃(2992)	→	2993
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
0₂(2755)	→	2756
0₂(2692)	→	2693
0₂(1163)	→	1164
0₂(2691)	→	2692
0₂(2419)	→	2420
0₂(1195)	→	1196
0₂(2697)	→	2698
0₂(1041)	→	1042
0₂(2694)	→	2695
0₂(1115)	→	1116
0₂(2585)	→	2586
0₂(2489)	→	2490
0₂(1152)	→	1153
0₂(2695)	→	2696
0₂(1385)	→	1386
0₂(2496)	→	2497
0₂(1038)	→	1039
0₂(1206)	→	1207
0₂(2936)	→	2937
0₂(2558)	→	2559
0₂(2514)	→	2515
0₂(2500)	→	2501
0₂(2752)	→	2753
0₂(2502)	→	2503
0₂(2518)	→	2519
0₂(1386)	→	1387
0₂(2690)	→	2691

The automaton is closed under rewriting as it is compatible.