Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4374)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

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

1.1 Bounds

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

final states:

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

transitions:

1380	→	740
322	→	682
322	→	883
322	→	1069
2042	→	591
867	→	1031
867	→	1057
867	→	2163
329	→	1071
329	→	1788
2421	→	1990
1287	→	1279
2166	→	851
2166	→	2167
2166	→	2589
2150	→	1286
2150	→	862
2150	→	765
731	→	722
731	→	732
731	→	1377
1859	→	1850
1573	→	845
2138	→	773
1579	→	851
1579	→	1584
1335	→	1379
835	→	330
835	→	1566
685	→	845
1751	→	1032
1751	→	1769
745	→	728
1674	→	943
454	→	1270
454	→	1523
454	→	1597
830	→	1020
1057	→	2085
1529	→	1719
1529	→	1744
1529	→	2041
1875	→	213
1056	→	1043
1056	→	1084
271	→	712
1551	→	319
2152	→	2141
1418	→	1395
2268	→	1755
2443	→	90
1109	→	809
1089	→	1072
794	→	773
794	→	1558
98	→	1409
1624	→	453
214	→	166
214	→	496
214	→	366
214	→	120
214	→	43
214	→	165
214	→	388
214	→	4
214	→	323
897	→	890
2525	→	1850
2349	→	570
880	→	870
1842	→	269
1842	→	1956
1842	→	1962
1842	→	1964
1142	→	2396
1142	→	2450
809	→	1652
10	→	828
2229	→	912
1653	→	1634
387	→	322
387	→	656
387	→	879
2247	→	951
2247	→	2470
1998	→	2279
1998	→	2458
2062	→	734
97	→	1088
97	→	1808
1557	→	319
1248	→	1705
1248	→	2006
1248	→	2196
1248	→	2228
1864	→	2410
1864	→	2426
2427	→	90
1284	→	1713
1284	→	1742
1284	→	2039
1867	→	213
1885	→	951
1479	→	861
1479	→	633
1479	→	631
1479	→	90
1479	→	479
1479	→	368
1479	→	144
1479	→	8
1479	→	215
1479	→	432
1479	→	6
1479	→	304
1479	→	164
2363	→	754
886	→	1110
303	→	17
641	→	1582
1704	→	90
882	→	870
728	→	1135
1977	→	638
2457	→	739
2056	→	591
811	→	6
811	→	861
811	→	633
811	→	631
811	→	90
811	→	304
811	→	164
2590	→	684
2040	→	591
2461	→	746
956	→	2141
1909	→	2291
1909	→	2293
1909	→	2318
2070	→	746
119	→	90
2126	→	323
2399	→	1990
1249	→	569
1249	→	539
1249	→	259
1249	→	4
1249	→	166
1249	→	195
1249	→	1755
1249	→	1722
1249	→	1772
2132	→	773
145	→	90
145	→	764
145	→	6
145	→	756
145	→	570
145	→	121
659	→	636
2570	→	1990
1916	→	1901
461	→	1145
461	→	1858
1575	→	845
299	→	1176
878	→	3
878	→	478
878	→	747
878	→	2137
878	→	577
878	→	1973
1887	→	1877
1327	→	1315
1532	→	453
1825	→	259
2191	→	236
2191	→	1069
2191	→	682
2191	→	452
2191	→	321
2191	→	142
2191	→	67
2191	→	213
2191	→	430
2191	→	5
2191	→	883
2191	→	322
2191	→	1070
585	→	1004
585	→	1625
585	→	1633
585	→	2000
260	→	1170
260	→	5
1589	→	862
550	→	1326
2054	→	591
2235	→	912
18	→	1
18	→	922
18	→	924
18	→	389
18	→	828
18	→	10
18	→	415
18	→	912
18	→	451
18	→	431
18	→	550
18	→	1224
18	→	2096
18	→	2088
18	→	2104
18	→	2235
18	→	2102
18	→	2465
2586	→	90
547	→	991
547	→	1631
547	→	1644
547	→	2016
624	→	1237
2086	→	746
2556	→	453
643	→	1053
643	→	1361
643	→	1750
1577	→	845
41	→	1675
41	→	1972
41	→	2157
2588	→	90
2545	→	2595
2545	→	2599
3	→	87
3	→	163
3	→	192
3	→	347
3	→	412
3	→	494
1362	→	1351
2088	→	746
1727	→	2466
1003	→	90
691	→	98
1565	→	830
2156	→	453
2154	→	2141
213	→	2103
1789	→	1755
2320	→	2569
2320	→	2585
626	→	1264
2313	→	1850
1359	→	1864
919	→	1371
2140	→	277
9	→	234
9	→	597
9	→	812
729	→	1
729	→	924
729	→	922
729	→	10
729	→	389
729	→	415
729	→	550
729	→	912
729	→	2235
729	→	2102
729	→	957
729	→	2465
1706	→	90
1714	→	166
1809	→	1755
2459	→	746
331	→	4
331	→	214
331	→	193
331	→	195
331	→	738
331	→	540
331	→	712
331	→	2180
331	→	1755
331	→	1722
331	→	1772
5	→	67
5	→	142
5	→	213
5	→	321
5	→	430
5	→	452
584	→	1184
584	→	1931
515	→	453
515	→	593
515	→	799
1999	→	1170
1999	→	1069
1999	→	682
1999	→	658
1999	→	5
1999	→	322
1999	→	881
1999	→	367
1999	→	260
642	→	1886
592	→	578
592	→	721
1000	→	2069
1567	→	684
1454	→	759
1764	→	236
1764	→	1069
1764	→	682
1764	→	883
1764	→	322
1764	→	1070
241	→	1898
2429	→	90
1618	→	712
891	→	16
2197	→	453
765	→	1286
1134	→	234
1639	→	857
175	→	1
175	→	924
175	→	912
175	→	389
175	→	451
175	→	551
175	→	1222
175	→	1224
175	→	2088
2374	→	2591
1768	→	1756
2311	→	1850
1866	→	2418
1866	→	2442
90	→	319
90	→	633
90	→	851
90	→	861
90	→	1576
193	→	166
1965	→	570
2318	→	2571
2318	→	2587
99	→	5
99	→	883
99	→	322
99	→	348
99	→	367
99	→	260
397	→	17
397	→	1276
2471	→	2142
1238	→	572
1770	→	1756
495	→	453
495	→	1112
713	→	1611
2007	→	1990
2072	→	746
2373	→	2509
2373	→	2522
1132	→	234
2343	→	17
2280	→	494
2280	→	2340
2280	→	2342
2280	→	2348
1403	→	1727
1403	→	1802
1403	→	1843
1403	→	2055
1403	→	2474
2523	→	259
1530	→	216
1530	→	892
1530	→	862
1530	→	765
1	→	41
1	→	89
1	→	232
1	→	349
1	→	450
1	→	477
1817	→	259
877	→	1210
1957	→	89
1957	→	2063
305	→	296
1299	→	2071
165	→	2101
1081	→	883
1081	→	5
1081	→	682
1081	→	322
1081	→	236
1081	→	1070
2074	→	746
977	→	10
755	→	3
755	→	730
755	→	578
755	→	801
755	→	453
755	→	495
755	→	590
755	→	596
1267	→	598
2190	→	2246
2190	→	2281
2190	→	2472
570	→	756
570	→	764
570	→	1215
1626	→	453
2357	→	2476
965	→	828
965	→	10
778	→	2116
1338	→	2020
1721	→	2464
1111	→	1106
1412	→	1395
477	→	1929
1713	→	2462
1319	→	1673
1478	→	1703
1478	→	2008
1478	→	2181
1478	→	2236
1722	→	166
1052	→	924
1052	→	912
1052	→	1
1052	→	389
1052	→	451
1052	→	1222
1052	→	2088
548	→	5
548	→	367
548	→	260
1645	→	1634
1130	→	298
747	→	1564
590	→	578
390	→	703
390	→	928
44	→	9
884	→	870
1283	→	1876
1283	→	2267
1283	→	2273
1213	→	2226
480	→	453
480	→	577
480	→	772
480	→	1617
1376	→	734
1194	→	515
1194	→	3
1194	→	813
1194	→	591
1194	→	2054
796	→	773
796	→	1381
634	→	624
2564	→	1990
1676	→	956
2592	→	746
2451	→	90
261	→	516
1772	→	1755
330	→	1417
1598	→	1592
1070	→	236
297	→	1212
993	→	1303
235	→	803
235	→	1129
920	→	955
920	→	1250
920	→	1548
1030	→	833
556	→	1394
233	→	166
91	→	605
91	→	684
91	→	1268
91	→	1990
91	→	1698
91	→	2019
2465	→	746
1005	→	90
1353	→	1375
1971	→	577
1971	→	2131
2533	→	213
868	→	396
268	→	5
268	→	883
268	→	682
268	→	322
268	→	236
268	→	1070
1766	→	1756
2365	→	608
1410	→	1395
1214	→	547
540	→	738
540	→	569
540	→	539
540	→	259
540	→	496
540	→	366
540	→	120
540	→	43
540	→	165
2319	→	213
1926	→	259
1339	→	98
389	→	746
389	→	924
779	→	173
911	→	710
911	→	1114
121	→	90
121	→	1572
1382	→	741
1610	→	886
277	→	1151
277	→	2312
810	→	1002
810	→	1623
810	→	1646
810	→	2014
1477	→	2240
2572	→	1990
6	→	8
6	→	144
6	→	215
6	→	368
6	→	432
6	→	479
2282	→	885
2282	→	2354
2282	→	2468
2548	→	1877
2064	→	739
1193	→	1974
1193	→	2073
1193	→	2139
1193	→	2155
1865	→	213
1240	→	1468
921	→	2
921	→	812
921	→	234
921	→	9
921	→	42
921	→	2141
921	→	956
921	→	1676
1051	→	1915
1051	→	1927
1456	→	767
88	→	9
1351	→	1590
1351	→	1609
455	→	905
1282	→	2165
1282	→	2555
1282	→	2563
431	→	389
431	→	1221
1041	→	924
1041	→	912
1041	→	389
1041	→	451
1041	→	1222
1041	→	2088
1811	→	1755
522	→	1266
522	→	1411
522	→	1470
522	→	1531
1585	→	862
174	→	1195
174	→	1451
174	→	1900
1364	→	1351
1181	→	214
2158	→	319
433	→	389
1146	→	1136
2021	→	90
657	→	636
2274	→	259
1192	→	2153
1192	→	2161
350	→	322
350	→	635
350	→	869
1180	→	1849
1180	→	1866
1180	→	2376
1647	→	1634
2009	→	1990
2015	→	1990
1596	→	728
143	→	90
143	→	295
143	→	623
143	→	1574
923	→	913
1899	→	1877
999	→	1810
999	→	1824
1014	→	1754
1014	→	1816
2	→	65
2	→	118
2	→	194
2	→	386
2	→	414
2	→	514
863	→	1455
2411	→	1990
4	→	43
4	→	120
4	→	165
4	→	366
4	→	388
4	→	496
232	→	2087
604	→	173
2019	→	1990
827	→	727
557	→	174
850	→	396
1222	→	551
1404	→	730
1404	→	578
1404	→	801
1404	→	453
1404	→	494
1404	→	347
1404	→	163
1404	→	87
1404	→	192
1404	→	412
1404	→	3
1404	→	495
1404	→	590
1404	→	596
478	→	453
478	→	589
478	→	793
478	→	3
904	→	834
1001	→	883
1001	→	322
1001	→	5
1001	→	348
369	→	322
754	→	1055
754	→	1133
754	→	1363
754	→	1796
802	→	773
820	→	643
2453	→	90
1587	→	862
1015	→	1841
1015	→	2075
66	→	9
2341	→	89
2341	→	2456
2594	→	1990
1452	→	757
1043	→	1086
1043	→	1313
1043	→	1334
862	→	892
862	→	1976
1224	→	551
2477	→	845
2475	→	684
2531	→	1850
348	→	322
1872	→	2412
1872	→	2428
1692	→	10
1962	→	2326
800	→	773
925	→	913
1698	→	90
1743	→	1032
1743	→	1765
497	→	453
497	→	591
497	→	795
497	→	1104
1143	→	1794
1143	→	1818
1963	→	17
1856	→	2398
1856	→	2452
596	→	578
596	→	730
2327	→	1877
1216	→	296
2241	→	912
1378	→	734
1247	→	1925
1247	→	1954
1559	→	831
2600	→	90
736	→	1006
1632	→	453
1712	→	1021
2463	→	746
2162	→	319
2094	→	746
1873	→	213
2554	→	89
2554	→	2561
2237	→	912
1085	→	1073
1080	→	1872
934	→	414
710	→	974
710	→	976
710	→	1239
710	→	1550
42	→	9
42	→	2
42	→	2141
42	→	956
42	→	1676
1179	→	2295
1179	→	2320
1581	→	852
630	→	329
216	→	166
1321	→	367
1321	→	5
1321	→	260
453	→	595
453	→	801
453	→	2179
2375	→	1755
2375	→	195
2375	→	1722
2375	→	1772
637	→	1493
1196	→	1185
1494	→	1474
1795	→	1755
709	→	942
1910	→	569
1910	→	539
1910	→	259
1910	→	166
1910	→	323
1910	→	214
1745	→	1032
1745	→	1767
278	→	6
278	→	861
278	→	633
278	→	90
278	→	764
278	→	756
278	→	570
278	→	121
278	→	623
278	→	683
278	→	261
278	→	659
278	→	295
278	→	143
278	→	1990
278	→	1698
278	→	2019
1083	→	1073
1083	→	1164
763	→	643
763	→	1131
952	→	924
952	→	389
952	→	431
952	→	957
952	→	2104
586	→	4
586	→	569
586	→	539
586	→	259
586	→	166
586	→	195
586	→	1755
586	→	1722
586	→	1772
1975	→	452
1372	→	730
414	→	1721
414	→	1771
414	→	2053
1774	→	1755
2076	→	746
771	→	174
1720	→	166
17	→	1042
17	→	1350
17	→	1773
683	→	636
2160	→	319
2342	→	2547
1549	→	319
718	→	330
1583	→	851
1583	→	1588
164	→	90
164	→	304
164	→	631
2168	→	862
1144	→	213
1148	→	1136
242	→	17
1874	→	2420
1874	→	2444
68	→	9
870	→	885
462	→	4
462	→	214
1928	→	259
267	→	1147
2210	→	453
413	→	389
413	→	1223
858	→	16
215	→	2093
2377	→	453
320	→	296
320	→	821
1087	→	1073
1087	→	1166
1469	→	773
2397	→	1990
521	→	1556
521	→	2151
1054	→	1043
1054	→	1082
1360	→	924
1360	→	922
1360	→	10
1360	→	1
1360	→	389
1360	→	415
1360	→	2465
722	→	2061
523	→	3
523	→	515
523	→	813
523	→	591
523	→	2054
2292	→	8
2292	→	2356
2292	→	2366
1058	→	166
1281	→	2524
1281	→	2545
1271	→	626
259	→	1697
259	→	2018
259	→	2209
259	→	2234
2355	→	578
2546	→	213
711	→	5
711	→	367
711	→	260
711	→	236
711	→	1070
1165	→	392
2017	→	1990
92	→	1453
1285	→	214
451	→	389
451	→	912
1955	→	1932
2102	→	746
2473	→	319
195	→	166
2294	→	1850
1171	→	392
1113	→	1105
2115	→	746
852	→	898
852	→	2364
1251	→	1240
1016	→	496
1016	→	366
1016	→	120
1016	→	4
1016	→	586
1016	→	323
1016	→	214
1320	→	1689
1320	→	1691
1320	→	1970
1320	→	2159
367	→	322
367	→	658
367	→	881
1908	→	2530
1908	→	2532
1908	→	2553
611	→	329
144	→	1874
144	→	2310
594	→	578
1269	→	607
1930	→	259
2296	→	1850
396	→	1578
1152	→	1136
1558	→	1711
194	→	2095
2104	→	746
1211	→	1185
1265	→	602
1857	→	1014
1973	→	577
1973	→	2137
1844	→	234
2180	→	712
632	→	624
1797	→	1755
576	→	276
1167	→	392
1612	→	888
1304	→	685
166	→	259
166	→	269
166	→	539
166	→	549
166	→	569
166	→	388
166	→	4
2413	→	1990
737	→	584
1803	→	1755
992	→	1580
992	→	1586
2510	→	1755
975	→	956
2419	→	1990
2164	→	684
644	→	4
644	→	214
644	→	216
644	→	892
644	→	862
644	→	765
1719	→	2460
2096	→	746
2467	→	746
1300	→	367
1300	→	5
1300	→	260
192	→	2114
415	→	389
415	→	922
415	→	477
415	→	349
415	→	89
415	→	41
415	→	232
415	→	450
415	→	1
415	→	2096
1941	→	813
1819	→	259
2598	→	90
2445	→	90
2562	→	453
2001	→	1990
2321	→	213
2532	→	2593
2532	→	2597
1690	→	956
2227	→	912
1115	→	885
545	→	1290
545	→	1989
2469	→	773
1728	→	166
2596	→	1990
4₁(1080)	→	1081
4₁(260)	→	261
4₁(1471)	→	1472
4₁(2372)	→	2373
4₁(95)	→	96
4₁(625)	→	626
4₁(756)	→	757
4₁(1212)	→	1213
4₁(2452)	→	2453
4₁(600)	→	601
4₁(638)	→	639
4₁(543)	→	544
4₁(817)	→	818
4₁(2163)	→	2164
4₁(753)	→	754
4₁(540)	→	541
4₁(263)	→	264
4₁(749)	→	750
4₁(569)	→	570
4₁(1281)	→	1282
4₁(277)	→	278
4₁(912)	→	913
4₁(1050)	→	1051
4₁(2585)	→	2586
4₁(461)	→	462
4₁(2165)	→	2166
4₁(1354)	→	1355
4₁(1578)	→	1579
4₁(2589)	→	2590
4₁(2161)	→	2162
4₁(1566)	→	1567
4₁(777)	→	778
4₁(1336)	→	1337
4₁(597)	→	598
4₁(1976)	→	1977
4₁(761)	→	762
4₁(1359)	→	1360
4₁(656)	→	657
4₁(728)	→	729
4₁(2020)	→	2021
4₁(901)	→	902
4₁(1634)	→	1635
4₁(2450)	→	2451
4₁(872)	→	873
4₁(682)	→	683
4₁(997)	→	998
4₁(2357)	→	2358
4₁(913)	→	914
4₁(1964)	→	1965
4₁(1635)	→	1636
4₁(2157)	→	2158
4₁(2587)	→	2588
4₁(1592)	→	1593
4₁(886)	→	887
4₁(1526)	→	1527
4₁(1550)	→	1551
4₁(856)	→	857
4₁(1076)	→	1077
4₁(2426)	→	2427
4₁(1270)	→	1271
4₁(1451)	→	1452
4₁(857)	→	858
4₁(2444)	→	2445
4₁(834)	→	835
4₁(120)	→	121
4₁(637)	→	638
4₁(750)	→	751
4₁(1974)	→	1975
4₁(635)	→	636
4₁(118)	→	119
4₁(2348)	→	2349
4₁(144)	→	145
4₁(392)	→	393
4₁(1398)	→	1399
4₁(2599)	→	2600
4₁(2159)	→	2160
4₁(992)	→	993
4₁(1266)	→	1267
4₁(609)	→	610
4₁(573)	→	574
4₁(1326)	→	1327
4₁(712)	→	713
4₁(762)	→	763
4₁(460)	→	461
4₁(902)	→	903
4₁(1276)	→	1277
4₁(173)	→	174
4₁(163)	→	164
4₁(2361)	→	2362
4₁(2291)	→	2292
4₁(1286)	→	1287
4₁(1073)	→	1074
4₁(2428)	→	2429
4₁(1002)	→	1003
4₁(849)	→	850
4₁(853)	→	854
4₁(90)	→	91
4₁(774)	→	775
4₁(922)	→	923
4₁(1180)	→	1181
4₁(1703)	→	1704
4₁(991)	→	992
4₁(2442)	→	2443
4₁(845)	→	846
4₁(744)	→	745
4₁(768)	→	769
4₁(298)	→	299
4₁(1004)	→	1005
4₁(1246)	→	1247
4₁(760)	→	761
4₁(2368)	→	2369
4₁(704)	→	705
4₁(456)	→	457
4₁(866)	→	867
4₁(640)	→	641
4₁(89)	→	90
4₁(629)	→	630
4₁(1278)	→	1279
4₁(658)	→	659
4₁(1291)	→	1292
4₁(583)	→	584
4₁(1697)	→	1698
4₁(605)	→	606
4₁(723)	→	724
4₁(2371)	→	2372
4₁(2553)	→	2554
4₁(574)	→	575
4₁(267)	→	268
4₁(1705)	→	1706
4₁(2474)	→	2475
4₁(1556)	→	1557
4₁(628)	→	629
4₁(769)	→	770
4₁(876)	→	877
4₁(1357)	→	1358
4₁(917)	→	918
4₁(2472)	→	2473
4₁(553)	→	554
4₁(1290)	→	1291
4₁(726)	→	727
4₁(865)	→	866
4₁(1179)	→	1180
4₁(1402)	→	1403
4₁(1548)	→	1549
4₁(2356)	→	2357
4₁(142)	→	143
4₁(1279)	→	1280
4₁(1582)	→	1583
4₁(821)	→	822
4₁(924)	→	925
4₁(803)	→	804
4₁(1186)	→	1187
4₁(1314)	→	1315
4₁(2597)	→	2598
4₁(1399)	→	1400
5₂(1932)	→	1933
5₂(2120)	→	2121
5₂(1884)	→	1885
5₂(2530)	→	2531
5₂(1905)	→	1906
5₂(1856)	→	1857
5₂(2524)	→	2525
5₂(1769)	→	1770
5₂(1767)	→	1768
5₂(1762)	→	1763
5₂(1991)	→	1992
5₂(1902)	→	1903
5₂(2293)	→	2294
5₂(1765)	→	1766
5₂(1995)	→	1996
5₂(1755)	→	1756
5₂(1035)	→	1036
5₂(1938)	→	1939
5₂(1849)	→	1850
5₂(2295)	→	2296
5₂(2312)	→	2313
5₂(2310)	→	2311
5₂(1878)	→	1879
5₂(1992)	→	1993
5₂(1858)	→	1859
1₂(2470)	→	2471
1₂(2145)	→	2146
1₂(963)	→	964
1₂(1852)	→	1853
1₂(958)	→	959
1₂(1851)	→	1852
1₂(2144)	→	2145
1₂(961)	→	962
1₂(2141)	→	2142
1₂(1915)	→	1916
1₂(1934)	→	1935
1₂(945)	→	946
1₂(1027)	→	1028
1₂(948)	→	949
1₂(1935)	→	1936
1₂(1022)	→	1023
1₂(2119)	→	2120
1₂(1013)	→	1014
1₂(950)	→	951
1₂(2148)	→	2149
1₂(1993)	→	1994
1₂(1997)	→	1998
1₂(1760)	→	1761
1₂(1040)	→	1041
1₂(1853)	→	1854
1₂(1900)	→	1901
1₂(1882)	→	1883
1₂(1008)	→	1009
4₂(1020)	→	1021
4₂(1989)	→	1990
4₂(1756)	→	1757
4₂(2123)	→	2124
4₂(1933)	→	1934
4₂(2008)	→	2009
4₂(2595)	→	2596
4₂(2016)	→	2017
4₂(2396)	→	2397
4₂(2569)	→	2570
4₂(1909)	→	1910
4₂(1880)	→	1881
4₂(2118)	→	2119
4₂(2410)	→	2411
4₂(2014)	→	2015
4₂(1026)	→	1027
4₂(1006)	→	1007
4₂(2563)	→	2564
4₂(1908)	→	1909
4₂(2593)	→	2594
4₂(2018)	→	2019
4₂(1021)	→	1022
4₂(2124)	→	2125
4₂(1763)	→	1764
4₂(2420)	→	2421
4₂(2146)	→	2147
4₂(2117)	→	2118
4₂(1007)	→	1008
4₂(1759)	→	1760
4₂(2000)	→	2001
4₂(2122)	→	2123
4₂(2418)	→	2419
4₂(2412)	→	2413
4₂(1012)	→	1013
4₂(1904)	→	1905
4₂(1990)	→	1991
4₂(2398)	→	2399
4₂(1039)	→	1040
4₂(1711)	→	1712
4₂(2571)	→	2572
4₂(2006)	→	2007
2₁(192)	→	193
2₁(1088)	→	1089
2₁(213)	→	214
2₁(322)	→	323
2₁(716)	→	717
2₁(165)	→	166
2₁(1637)	→	1638
2₁(1104)	→	1105
2₁(330)	→	331
2₁(1353)	→	1354
2₁(1277)	→	1278
2₁(1929)	→	1930
2₁(1210)	→	1211
2₁(818)	→	819
2₁(1586)	→	1587
2₁(2279)	→	2280
2₁(327)	→	328
2₁(1317)	→	1318
2₁(2362)	→	2363
2₁(551)	→	552
2₁(747)	→	748
2₁(689)	→	690
2₁(1177)	→	1178
2₁(2189)	→	2190
2₁(778)	→	779
2₁(1136)	→	1137
2₁(2167)	→	2168
2₁(861)	→	862
2₁(1245)	→	1246
2₁(715)	→	716
2₁(1299)	→	1300
2₁(389)	→	390
2₁(1112)	→	1113
2₁(826)	→	827
2₁(1727)	→	1728
2₁(847)	→	848
2₁(1042)	→	1043
2₁(885)	→	886
2₁(906)	→	907
2₁(915)	→	916
2₁(2374)	→	2375
2₁(194)	→	195
2₁(1927)	→	1928
2₁(215)	→	216
2₁(1071)	→	1072
2₁(1617)	→	1618
2₁(1047)	→	1048
2₁(2340)	→	2341
2₁(270)	→	271
2₁(910)	→	911
2₁(2370)	→	2371
2₁(170)	→	171
2₁(556)	→	557
2₁(1609)	→	1610
2₁(232)	→	233
2₁(300)	→	301
2₁(908)	→	909
2₁(1048)	→	1049
2₁(1129)	→	1130
2₁(519)	→	520
2₁(1588)	→	1589
2₁(2522)	→	2523
2₁(707)	→	708
2₁(1396)	→	1397
2₁(1000)	→	1001
2₁(1721)	→	1722
2₁(1925)	→	1926
2₁(539)	→	540
2₁(1584)	→	1585
2₁(1184)	→	1185
2₁(705)	→	706
2₁(892)	→	893
2₁(893)	→	894
2₁(10)	→	11
2₁(932)	→	933
2₁(2360)	→	2361
2₁(98)	→	99
2₁(1195)	→	1196
2₁(602)	→	603
2₁(297)	→	298
2₁(804)	→	805
2₁(1141)	→	1142
2₁(1190)	→	1191
2₁(395)	→	396
2₁(1824)	→	1825
2₁(717)	→	718
2₁(1057)	→	1058
2₁(546)	→	547
2₁(1315)	→	1316
2₁(1193)	→	1194
2₁(1816)	→	1817
2₁(2273)	→	2274
2₁(823)	→	824
2₁(302)	→	303
2₁(636)	→	637
2₁(171)	→	172
2₁(764)	→	765
2₁(15)	→	16
2₁(1713)	→	1714
2₁(1055)	→	1056
2₁(608)	→	609
2₁(1818)	→	1819
2₁(1719)	→	1720
2₁(627)	→	628
2₁(824)	→	825
2₁(1527)	→	1528
2₁(1297)	→	1298
2₁(455)	→	456
2₁(458)	→	459
2₁(894)	→	895
2₁(1956)	→	1957
2₁(2179)	→	2180
2₁(1841)	→	1842
2₁(2187)	→	2188
2₁(1335)	→	1336
2₁(1472)	→	1473
2₁(582)	→	583
2₁(722)	→	723
2₁(2185)	→	2186
2₁(522)	→	523
2₁(1053)	→	1054
2₁(610)	→	611
5₀(3)	→	5
5₀(6)	→	5
5₀(5)	→	5
5₀(4)	→	5
5₀(2)	→	5
5₀(1)	→	5
4₀(2)	→	6
4₀(6)	→	6
4₀(4)	→	6
4₀(1)	→	6
4₀(3)	→	6
4₀(5)	→	6
0₂(2149)	→	2150
0₂(951)	→	952
0₂(2326)	→	2327
0₂(964)	→	965
0₂(1876)	→	1877
0₂(1886)	→	1887
0₂(1994)	→	1995
0₂(1936)	→	1937
0₂(1898)	→	1899
0₂(1758)	→	1759
0₂(2125)	→	2126
0₂(1010)	→	1011
0₂(1033)	→	1034
0₂(1023)	→	1024
0₂(946)	→	947
0₂(1014)	→	1015
0₂(1024)	→	1025
0₂(1881)	→	1882
0₂(960)	→	961
0₂(2547)	→	2548
0₂(2143)	→	2144
0₂(956)	→	957
0₂(1854)	→	1855
0₂(947)	→	948
0₂(943)	→	944
0₂(959)	→	960
0₂(1009)	→	1010
0₂(1028)	→	1029
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
3₁(87)	→	88
3₁(1401)	→	1402
3₁(1597)	→	1598
3₁(626)	→	627
3₁(1319)	→	1320
3₁(1591)	→	1592
3₁(1493)	→	1494
3₁(1356)	→	1357
3₁(599)	→	600
3₁(8)	→	9
3₁(624)	→	625
3₁(1164)	→	1165
3₁(870)	→	871
3₁(391)	→	392
3₁(1178)	→	1179
3₁(871)	→	872
3₁(172)	→	173
3₁(864)	→	865
3₁(94)	→	95
3₁(1594)	→	1595
3₁(304)	→	305
3₁(896)	→	897
3₁(575)	→	576
3₁(236)	→	237
3₁(775)	→	776
3₁(295)	→	296
3₁(43)	→	44
3₁(709)	→	710
3₁(1045)	→	1046
3₁(2367)	→	2368
3₁(1078)	→	1079
3₁(41)	→	42
3₁(166)	→	167
3₁(1455)	→	1456
3₁(67)	→	68
3₁(2369)	→	2370
3₁(1843)	→	1844
3₁(848)	→	849
3₁(735)	→	736
3₁(453)	→	454
3₁(1215)	→	1216
3₁(996)	→	997
3₁(1397)	→	1398
3₁(1590)	→	1591
3₁(319)	→	320
3₁(541)	→	542
3₁(521)	→	522
3₁(1280)	→	1281
3₁(261)	→	262
3₁(805)	→	806
3₁(724)	→	725
3₁(813)	→	814
3₁(65)	→	66
3₁(1337)	→	1338
3₁(1473)	→	1474
3₁(752)	→	753
3₁(579)	→	580
3₁(776)	→	777
3₁(759)	→	760
3₁(874)	→	875
3₁(1400)	→	1401
3₁(1043)	→	1044
3₁(713)	→	714
3₁(2190)	→	2191
3₁(1192)	→	1193
3₁(773)	→	774
3₁(920)	→	921
3₁(1355)	→	1356
3₁(748)	→	749
3₁(1049)	→	1050
3₁(1170)	→	1171
3₁(725)	→	726
3₁(743)	→	744
3₁(1166)	→	1167
3₁(265)	→	266
3₁(751)	→	752
3₁(1320)	→	1321
3₁(1131)	→	1132
3₁(1074)	→	1075
3₁(2182)	→	2183
3₁(1133)	→	1134
3₁(710)	→	711
3₁(459)	→	460
3₁(1242)	→	1243
3₁(639)	→	640
3₁(168)	→	169
3₁(742)	→	743
3₁(766)	→	767
0₁(549)	→	550
0₁(1075)	→	1076
0₁(601)	→	602
0₁(1611)	→	1612
0₁(274)	→	275
0₁(995)	→	996
0₁(393)	→	394
0₁(572)	→	573
0₁(2240)	→	2241
0₁(262)	→	263
0₁(1283)	→	1284
0₁(919)	→	920
0₁(2236)	→	2237
0₁(606)	→	607
0₁(2071)	→	2072
0₁(1644)	→	1645
0₁(2184)	→	2185
0₁(93)	→	94
0₁(643)	→	644
0₁(1636)	→	1637
0₁(2234)	→	2235
0₁(1646)	→	1647
0₁(2373)	→	2374
0₁(851)	→	852
0₁(903)	→	904
0₁(432)	→	433
0₁(2069)	→	2070
0₁(888)	→	889
0₁(1221)	→	1222
0₁(2358)	→	2359
0₁(687)	→	688
0₁(603)	→	604
0₁(772)	→	773
0₁(2466)	→	2467
0₁(999)	→	1000
0₁(2087)	→	2088
0₁(2114)	→	2115
0₁(929)	→	930
0₁(12)	→	13
0₁(1044)	→	1045
0₁(1468)	→	1469
0₁(799)	→	800
0₁(1529)	→	1530
0₁(1595)	→	1596
0₁(994)	→	995
0₁(1237)	→	1238
0₁(930)	→	931
0₁(550)	→	551
0₁(2095)	→	2096
0₁(97)	→	98
0₁(1381)	→	1382
0₁(1962)	→	1963
0₁(1140)	→	1141
0₁(92)	→	93
0₁(388)	→	389
0₁(238)	→	239
0₁(2101)	→	2102
0₁(1633)	→	1634
0₁(1379)	→	1380
0₁(2137)	→	2138
0₁(571)	→	572
0₁(2458)	→	2459
0₁(741)	→	742
0₁(518)	→	519
0₁(9)	→	10
0₁(1106)	→	1107
0₁(1652)	→	1653
0₁(2468)	→	2469
0₁(1417)	→	1418
0₁(1284)	→	1285
0₁(2228)	→	2229
0₁(740)	→	741
0₁(1403)	→	1404
0₁(846)	→	847
0₁(167)	→	168
0₁(854)	→	855
0₁(642)	→	643
0₁(1313)	→	1314
0₁(1409)	→	1410
0₁(2464)	→	2465
0₁(241)	→	242
0₁(793)	→	794
0₁(2591)	→	2592
0₁(2131)	→	2132
0₁(239)	→	240
0₁(887)	→	888
0₁(1143)	→	1144
0₁(1580)	→	1581
0₁(1474)	→	1475
0₁(852)	→	853
0₁(867)	→	868
0₁(1564)	→	1565
0₁(240)	→	241
0₁(770)	→	771
0₁(2073)	→	2074
0₁(905)	→	906
0₁(2462)	→	2463
0₁(2226)	→	2227
0₁(2103)	→	2104
0₁(430)	→	431
0₁(1411)	→	1412
0₁(1523)	→	1524
0₁(795)	→	796
0₁(806)	→	807
0₁(2188)	→	2189
0₁(1295)	→	1296
0₁(909)	→	910
0₁(1108)	→	1109
0₁(1264)	→	1265
0₁(739)	→	740
0₁(1223)	→	1224
0₁(801)	→	802
0₁(326)	→	327
0₁(1394)	→	1395
0₁(825)	→	826
0₁(2093)	→	2094
0₁(754)	→	755
0₁(272)	→	273
0₁(13)	→	14
0₁(2075)	→	2076
0₁(1189)	→	1190
0₁(17)	→	18
0₁(900)	→	901
0₁(2342)	→	2343
0₁(329)	→	330
0₁(914)	→	915
0₁(875)	→	876
0₁(2085)	→	2086
0₁(703)	→	704
0₁(1268)	→	1269
0₁(1691)	→	1692
0₁(414)	→	415
0₁(2460)	→	2461
0₁(814)	→	815
0₁(976)	→	977
0₁(412)	→	413
0₁(829)	→	830
0₁(450)	→	451
3₀(3)	→	2
3₀(5)	→	2
3₀(2)	→	2
3₀(4)	→	2
3₀(1)	→	2
3₀(6)	→	2
1₀(2)	→	3
1₀(4)	→	3
1₀(3)	→	3
1₀(6)	→	3
1₀(1)	→	3
1₀(5)	→	3
5₁(810)	→	811
5₁(1375)	→	1376
5₁(916)	→	917
5₁(1072)	→	1073
5₁(832)	→	833
5₁(237)	→	238
5₁(758)	→	759
5₁(1874)	→	1875
5₁(266)	→	267
5₁(2183)	→	2184
5₁(1574)	→	1575
5₁(1377)	→	1378
5₁(2476)	→	2477
5₁(1338)	→	1339
5₁(684)	→	685
5₁(2139)	→	2140
5₁(855)	→	856
5₁(1046)	→	1047
5₁(1213)	→	1214
5₁(276)	→	277
5₁(2545)	→	2546
5₁(890)	→	891
5₁(169)	→	170
5₁(368)	→	369
5₁(1478)	→	1479
5₁(321)	→	322
5₁(1079)	→	1080
5₁(809)	→	810
5₁(1084)	→	1085
5₁(390)	→	391
5₁(235)	→	236
5₁(234)	→	235
5₁(1151)	→	1152
5₁(454)	→	455
5₁(1866)	→	1867
5₁(1176)	→	1177
5₁(733)	→	734
5₁(366)	→	367
5₁(1135)	→	1136
5₁(1638)	→	1639
5₁(578)	→	579
5₁(580)	→	581
5₁(1282)	→	1283
5₁(271)	→	272
5₁(641)	→	642
5₁(1241)	→	1242
5₁(1576)	→	1577
5₁(767)	→	768
5₁(898)	→	899
5₁(1293)	→	1294
5₁(349)	→	350
5₁(2061)	→	2062
5₁(734)	→	735
5₁(1191)	→	1192
5₁(2318)	→	2319
5₁(1086)	→	1087
5₁(1185)	→	1186
5₁(1248)	→	1249
5₁(544)	→	545
5₁(1292)	→	1293
5₁(1558)	→	1559
5₁(386)	→	387
5₁(328)	→	329
5₁(1470)	→	1471
5₁(585)	→	586
5₁(1145)	→	1146
5₁(833)	→	834
5₁(2320)	→	2321
5₁(1477)	→	1478
5₁(296)	→	297
5₁(545)	→	546
5₁(1082)	→	1083
5₁(542)	→	543
5₁(347)	→	348
5₁(688)	→	689
5₁(1593)	→	1594
5₁(552)	→	553
5₁(457)	→	458
5₁(1110)	→	1111
5₁(1872)	→	1873
5₁(727)	→	728
5₁(396)	→	397
5₁(520)	→	521
5₁(1864)	→	1865
5₁(830)	→	831
5₁(1142)	→	1143
5₁(736)	→	737
5₁(1303)	→	1304
5₁(1147)	→	1148
5₁(1453)	→	1454
5₁(685)	→	686
5₁(895)	→	896
5₁(873)	→	874
5₁(1572)	→	1573
5₁(275)	→	276
5₁(259)	→	260
5₁(2532)	→	2533
5₁(547)	→	548
5₁(1358)	→	1359
5₁(1069)	→	1070
5₁(1243)	→	1244
5₁(1105)	→	1106
5₁(714)	→	715
5₁(1296)	→	1297
1₁(516)	→	517
1₁(1395)	→	1396
1₁(2196)	→	2197
1₁(570)	→	571
1₁(1188)	→	1189
1₁(581)	→	582
1₁(11)	→	12
1₁(819)	→	820
1₁(1316)	→	1317
1₁(299)	→	300
1₁(708)	→	709
1₁(815)	→	816
1₁(879)	→	880
1₁(862)	→	863
1₁(517)	→	518
1₁(1371)	→	1372
1₁(1361)	→	1362
1₁(931)	→	932
1₁(831)	→	832
1₁(1239)	→	1240
1₁(324)	→	325
1₁(686)	→	687
1₁(1114)	→	1115
1₁(16)	→	17
1₁(822)	→	823
1₁(2155)	→	2156
1₁(1528)	→	1529
1₁(2376)	→	2377
1₁(591)	→	592
1₁(1334)	→	1335
1₁(1351)	→	1352
1₁(1247)	→	1248
1₁(1318)	→	1319
1₁(807)	→	808
1₁(2555)	→	2556
1₁(494)	→	495
1₁(2063)	→	2064
1₁(514)	→	515
1₁(2456)	→	2457
1₁(1970)	→	1971
1₁(264)	→	265
1₁(1240)	→	1241
1₁(1631)	→	1632
1₁(730)	→	731
1₁(933)	→	934
1₁(623)	→	624
1₁(877)	→	878
1₁(1107)	→	1108
1₁(479)	→	480
1₁(738)	→	739
1₁(1525)	→	1526
1₁(607)	→	608
1₁(269)	→	270
1₁(96)	→	97
1₁(706)	→	707
1₁(598)	→	599
1₁(1051)	→	1052
1₁(477)	→	478
1₁(14)	→	15
1₁(452)	→	453
1₁(273)	→	274
1₁(633)	→	634
1₁(998)	→	999
1₁(1625)	→	1626
1₁(2561)	→	2562
1₁(1476)	→	1477
1₁(1972)	→	1973
1₁(869)	→	870
1₁(2181)	→	2182
1₁(91)	→	92
1₁(1138)	→	1139
1₁(2359)	→	2360
1₁(828)	→	829
1₁(746)	→	747
1₁(757)	→	758
1₁(1139)	→	1140
1₁(863)	→	864
1₁(2186)	→	2187
1₁(2209)	→	2210
1₁(889)	→	890
1₁(631)	→	632
1₁(1524)	→	1525
1₁(394)	→	395
1₁(993)	→	994
1₁(883)	→	884
1₁(1077)	→	1078
1₁(816)	→	817
1₁(2055)	→	2056
1₁(928)	→	929
1₁(2039)	→	2040
1₁(1244)	→	1245
1₁(918)	→	919
1₁(325)	→	326
1₁(1623)	→	1624
1₁(1187)	→	1188
1₁(2281)	→	2282
1₁(593)	→	594
1₁(1298)	→	1299
1₁(2354)	→	2355
1₁(1363)	→	1364
1₁(554)	→	555
1₁(174)	→	175
1₁(1294)	→	1295
1₁(2041)	→	2042
1₁(721)	→	722
1₁(577)	→	578
1₁(2366)	→	2367
1₁(496)	→	497
1₁(301)	→	302
1₁(1350)	→	1351
1₁(899)	→	900
1₁(881)	→	882
1₁(1137)	→	1138
1₁(555)	→	556
1₁(1352)	→	1353
1₁(584)	→	585
1₁(323)	→	324
1₁(812)	→	813
1₁(1475)	→	1476
1₁(2053)	→	2054
1₁(808)	→	809
1₁(589)	→	590
1₁(1250)	→	1251
1₁(907)	→	908
1₁(2364)	→	2365
1₁(595)	→	596
1₁(690)	→	691
1₁(765)	→	766
1₁(1531)	→	1532
1₁(732)	→	733
2₂(1773)	→	1774
2₂(1754)	→	1755
2₂(1794)	→	1795
2₂(1037)	→	1038
2₂(1802)	→	1803
2₂(1850)	→	1851
2₂(1771)	→	1772
2₂(1996)	→	1997
2₂(1940)	→	1941
2₂(1883)	→	1884
2₂(2509)	→	2510
2₂(2267)	→	2268
2₂(957)	→	958
2₂(2116)	→	2117
2₂(1954)	→	1955
2₂(1029)	→	1030
2₂(1788)	→	1789
2₂(944)	→	945
2₂(1796)	→	1797
2₂(1808)	→	1809
2₂(949)	→	950
2₂(962)	→	963
2₂(1031)	→	1032
2₂(1742)	→	1743
2₂(1036)	→	1037
2₂(1998)	→	1999
2₂(1744)	→	1745
2₂(1903)	→	1904
2₂(1750)	→	1751
2₂(2147)	→	2148
2₂(1810)	→	1811
2₂(1015)	→	1016
2₂(1877)	→	1878
2₂(1855)	→	1856
2₂(1906)	→	1907
2₂(1931)	→	1932
2₂(1937)	→	1938
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
3₂(2121)	→	2122
3₂(1025)	→	1026
3₂(1939)	→	1940
3₂(955)	→	956
3₂(1034)	→	1035
3₂(1011)	→	1012
3₂(1761)	→	1762
3₂(1757)	→	1758
3₂(2246)	→	2247
3₂(942)	→	943
3₂(1879)	→	1880
3₂(2151)	→	2152
3₂(1038)	→	1039
3₂(1673)	→	1674
3₂(1675)	→	1676
3₂(1032)	→	1033
3₂(1907)	→	1908
3₂(2153)	→	2154
3₂(974)	→	975
3₂(1689)	→	1690
3₂(2142)	→	2143
3₂(1901)	→	1902

The automaton is closed under rewriting as it is compatible.