Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3856)

The rewrite relation of the following TRS is considered.

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

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

1(1(0(0(x1))))	→	4(4(2(5(5(4(2(4(3(2(x1))))))))))	(55)
3(1(3(5(x1))))	→	1(5(4(2(4(4(2(4(2(2(x1))))))))))	(56)
5(1(0(0(0(x1)))))	→	5(5(4(3(3(1(2(4(3(1(x1))))))))))	(57)
5(2(0(0(0(x1)))))	→	5(3(1(5(5(4(2(3(1(0(x1))))))))))	(58)
3(2(0(4(1(x1)))))	→	4(1(2(4(4(3(2(3(3(1(x1))))))))))	(59)
3(4(5(5(2(x1)))))	→	3(4(2(3(2(4(4(3(1(0(x1))))))))))	(60)
0(5(2(5(4(x1)))))	→	0(2(5(4(3(2(2(4(4(2(x1))))))))))	(61)
0(3(1(3(0(0(x1))))))	→	0(2(2(2(3(3(1(2(1(2(x1))))))))))	(62)
5(1(1(1(1(1(x1))))))	→	5(1(1(3(3(4(2(3(2(2(x1))))))))))	(63)
5(1(4(3(0(2(x1))))))	→	5(4(1(2(1(3(2(4(3(2(x1))))))))))	(64)
2(0(1(5(0(4(x1))))))	→	2(2(5(4(2(2(3(2(0(1(x1))))))))))	(65)
2(1(0(0(1(4(x1))))))	→	2(5(3(4(2(2(4(1(0(4(x1))))))))))	(66)
3(4(0(1(1(5(x1))))))	→	2(4(1(2(4(4(4(1(2(5(x1))))))))))	(67)
4(1(3(0(0(0(0(x1)))))))	→	2(2(5(5(5(1(1(2(1(0(x1))))))))))	(68)
3(1(0(0(1(0(0(x1)))))))	→	1(5(3(0(4(4(3(3(0(2(x1))))))))))	(69)
4(1(1(0(2(0(0(x1)))))))	→	1(4(4(4(4(4(0(2(2(5(x1))))))))))	(70)
3(4(0(3(5(0(0(x1)))))))	→	3(1(3(2(2(2(5(3(0(2(x1))))))))))	(71)
0(3(1(3(5(0(0(x1)))))))	→	0(2(2(2(4(5(3(2(5(5(x1))))))))))	(72)
4(0(0(0(0(1(0(x1)))))))	→	2(4(5(5(1(4(1(5(4(2(x1))))))))))	(73)
0(0(4(1(5(1(0(x1)))))))	→	0(5(3(4(2(0(4(2(2(2(x1))))))))))	(74)
0(0(4(4(5(2(0(x1)))))))	→	0(0(4(5(4(1(2(4(3(2(x1))))))))))	(75)
3(1(0(1(0(3(0(x1)))))))	→	3(3(0(3(5(4(2(1(4(0(x1))))))))))	(76)
4(1(5(2(0(5(0(x1)))))))	→	4(1(2(4(0(4(4(2(2(0(x1))))))))))	(77)
3(4(0(4(0(5(0(x1)))))))	→	3(4(1(2(1(2(5(3(5(0(x1))))))))))	(78)
5(2(0(0(1(5(0(x1)))))))	→	5(4(0(1(2(1(2(4(1(2(x1))))))))))	(79)
4(4(1(0(3(5(0(x1)))))))	→	4(2(1(5(5(2(4(2(1(2(x1))))))))))	(80)
4(4(5(0(3(5(0(x1)))))))	→	1(1(3(4(2(2(2(1(1(1(x1))))))))))	(81)
2(3(4(3(5(5(0(x1)))))))	→	2(3(3(4(2(0(3(3(3(2(x1))))))))))	(82)
4(5(5(3(4(0(1(x1)))))))	→	4(5(5(3(5(4(1(2(2(2(x1))))))))))	(83)
0(3(5(0(0(2(1(x1)))))))	→	0(3(3(0(2(1(3(0(2(2(x1))))))))))	(84)
4(0(0(0(3(2(1(x1)))))))	→	4(5(2(3(4(1(3(2(1(2(x1))))))))))	(85)
5(0(0(0(5(2(1(x1)))))))	→	5(2(5(0(3(0(5(5(0(1(x1))))))))))	(86)
0(3(5(5(0(4(1(x1)))))))	→	0(2(4(0(1(0(3(4(2(1(x1))))))))))	(87)
4(0(0(1(3(0(2(x1)))))))	→	2(3(3(3(5(1(1(4(0(2(x1))))))))))	(88)
5(4(5(2(5(0(2(x1)))))))	→	5(4(2(2(4(0(2(2(1(5(x1))))))))))	(89)
4(0(0(0(0(1(2(x1)))))))	→	2(2(1(2(2(5(5(4(1(2(x1))))))))))	(90)
2(1(0(0(0(3(2(x1)))))))	→	2(5(4(3(4(4(0(4(0(2(x1))))))))))	(91)
4(5(4(0(0(0(3(x1)))))))	→	2(3(0(0(3(1(2(4(4(3(x1))))))))))	(92)
3(3(4(5(0(0(3(x1)))))))	→	1(2(5(3(4(2(2(5(2(4(x1))))))))))	(93)
4(1(0(4(3(0(3(x1)))))))	→	2(5(1(0(3(4(2(4(2(4(x1))))))))))	(94)
0(0(0(5(5(2(3(x1)))))))	→	0(5(3(5(4(2(1(1(3(4(x1))))))))))	(95)
5(1(4(3(4(3(3(x1)))))))	→	5(4(1(1(2(4(4(3(4(4(x1))))))))))	(96)
3(4(5(0(4(3(4(x1)))))))	→	4(1(2(4(3(4(1(4(3(4(x1))))))))))	(97)
1(5(5(0(0(0(5(x1)))))))	→	0(2(3(3(5(2(2(3(2(5(x1))))))))))	(98)
4(4(1(1(0(0(5(x1)))))))	→	4(2(3(3(3(0(3(0(5(5(x1))))))))))	(99)
2(1(5(5(0(0(5(x1)))))))	→	2(2(5(1(4(1(5(5(5(5(x1))))))))))	(100)
4(1(5(2(1(0(5(x1)))))))	→	4(4(2(3(1(5(5(5(0(5(x1))))))))))	(101)
4(1(5(2(0(1(5(x1)))))))	→	1(5(5(4(2(4(2(1(0(5(x1))))))))))	(102)
5(4(1(0(1(1(5(x1)))))))	→	0(3(4(2(1(4(0(1(2(5(x1))))))))))	(103)
1(4(1(5(2(1(5(x1)))))))	→	3(4(2(2(0(5(4(2(5(5(x1))))))))))	(104)
4(4(1(3(5(2(5(x1)))))))	→	4(1(2(1(2(1(3(4(2(5(x1))))))))))	(105)
1(0(0(5(2(3(5(x1)))))))	→	3(5(5(4(3(4(1(2(4(3(x1))))))))))	(106)
4(1(0(5(4(3(5(x1)))))))	→	2(4(2(0(5(4(1(2(3(2(x1))))))))))	(107)
4(5(0(0(5(4(5(x1)))))))	→	2(0(4(0(1(5(3(1(5(5(x1))))))))))	(108)

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:

272	→	224
1182	→	1167
1405	→	932
1405	→	894
1405	→	3
1405	→	445
1405	→	455
1405	→	1829
1405	→	166
1405	→	1602
854	→	834
871	→	1235
871	→	1251
1602	→	166
329	→	319
429	→	403
429	→	788
1895	→	1020
494	→	445
1940	→	158
818	→	797
1437	→	658
1579	→	833
1608	→	868
1335	→	874
1335	→	939
1335	→	888
1335	→	471
1335	→	157
1335	→	8
1335	→	223
1335	→	551
1335	→	6
1335	→	924
1335	→	883
2216	→	448
2216	→	1308
89	→	1476
745	→	604
2046	→	402
1441	→	9
1106	→	2306
356	→	325
860	→	834
967	→	975
1117	→	87
1117	→	1894
794	→	1201
794	→	1974
1624	→	894
10	→	746
10	→	1020
2297	→	874
1261	→	967
401	→	166
537	→	510
537	→	853
537	→	873
537	→	444
537	→	206
537	→	67
537	→	269
537	→	536
537	→	5
1248	→	1236
1733	→	962
2240	→	933
294	→	1165
294	→	1247
294	→	1284
1431	→	650
1046	→	2002
1046	→	2045
1250	→	1236
1479	→	901
1237	→	1543
2069	→	512
2069	→	2148
1409	→	1396
1409	→	1726
96	→	6
96	→	287
96	→	874
96	→	885
96	→	159
96	→	296
96	→	226
96	→	889
96	→	1167
96	→	1182
303	→	6
303	→	874
303	→	939
303	→	924
303	→	883
303	→	296
303	→	287
303	→	885
303	→	159
303	→	226
2185	→	448
2185	→	2225
2185	→	2237
1435	→	658
933	→	1615
1209	→	1202
1544	→	799
326	→	1050
326	→	1128
326	→	1278
326	→	1408
882	→	2176
1363	→	1972
1363	→	2158
1363	→	2323
136	→	88
136	→	380
136	→	658
136	→	769
167	→	5
167	→	966
167	→	633
167	→	859
167	→	510
167	→	833
167	→	535
167	→	705
167	→	851
167	→	521
167	→	855
167	→	554
167	→	1424
167	→	1396
167	→	2095
167	→	2155
998	→	1
998	→	823
998	→	428
998	→	158
998	→	815
998	→	209
998	→	569
998	→	817
998	→	189
998	→	225
998	→	1670
998	→	1564
998	→	1443
1757	→	1917
1757	→	1941
1757	→	2096
1757	→	2162
472	→	445
511	→	597
511	→	944
511	→	999
2132	→	350
659	→	754
1916	→	9
1575	→	833
1532	→	754
585	→	94
705	→	1541
2097	→	1396
18	→	1
18	→	169
18	→	738
1103	→	2029
1103	→	2256
1103	→	2268
226	→	296
226	→	287
226	→	874
226	→	888
226	→	471
226	→	157
226	→	8
226	→	223
226	→	551
226	→	6
226	→	885
226	→	159
41	→	9
41	→	87
41	→	328
1577	→	833
3	→	85
3	→	208
3	→	271
3	→	473
3	→	553
3	→	882
1411	→	1396
2063	→	224
1104	→	287
1104	→	874
1104	→	888
1104	→	471
1104	→	157
1104	→	8
1104	→	223
1104	→	551
1104	→	6
1104	→	885
1104	→	159
1246	→	1236
988	→	1633
1727	→	954
2271	→	1770
1565	→	828
1634	→	894
225	→	569
225	→	1307
1114	→	1958
1995	→	318
2149	→	771
1074	→	1038
1074	→	1428
1074	→	1434
187	→	158
187	→	796
134	→	88
411	→	4
411	→	578
411	→	347
411	→	115
411	→	404
411	→	695
411	→	9
411	→	66
411	→	328
411	→	824
411	→	570
411	→	818
411	→	87
411	→	41
411	→	822
411	→	835
411	→	318
411	→	1995
9	→	135
9	→	347
9	→	349
9	→	578
5	→	67
5	→	206
5	→	269
5	→	444
5	→	536
5	→	873
209	→	158
209	→	815
209	→	1599
2030	→	117
2030	→	2066
95	→	1270
95	→	1745
95	→	1779
1778	→	823
1778	→	428
1778	→	158
1778	→	884
1778	→	454
1778	→	168
1778	→	40
1778	→	233
1778	→	509
1778	→	1
1778	→	815
1778	→	209
1778	→	1670
1778	→	1564
1778	→	1443
1932	→	87
1932	→	2298
1567	→	828
1918	→	9
319	→	2150
1328	→	1537
1328	→	1751
997	→	1631
1618	→	702
692	→	1660
2179	→	896
381	→	373
325	→	1570
1446	→	2198
1446	→	2206
1095	→	1896
889	→	874
1965	→	224
445	→	894
445	→	923
445	→	932
445	→	1442
224	→	685
224	→	694
224	→	704
713	→	861
938	→	399
1601	→	1994
1448	→	2117
1599	→	1996
1530	→	747
2118	→	686
2118	→	2186
2118	→	2227
2118	→	2235
1758	→	966
1758	→	633
1758	→	510
1758	→	873
1758	→	444
1758	→	206
1758	→	67
1758	→	269
1758	→	536
1758	→	5
1758	→	855
1758	→	554
1758	→	521
1758	→	705
1758	→	833
1758	→	535
1758	→	167
1	→	40
1	→	168
1	→	233
1	→	454
1	→	509
1	→	884
826	→	867
1308	→	448
1308	→	2223
1308	→	2254
1443	→	1564
1443	→	1670
2291	→	874
1019	→	997
1026	→	656
1957	→	287
922	→	576
840	→	400
1298	→	1285
1663	→	933
1837	→	1925
1837	→	1931
1837	→	2296
1004	→	700
895	→	915
2067	→	512
2067	→	2133
1838	→	1448
1626	→	894
1626	→	1648
1626	→	1668
570	→	1749
965	→	408
770	→	762
410	→	1208
410	→	1576
2228	→	924
1173	→	1956
1173	→	2004
1173	→	2043
1934	→	158
1661	→	702
1283	→	397
1213	→	1202
1376	→	296
1376	→	287
1376	→	874
1376	→	888
1376	→	471
1376	→	157
1376	→	8
1376	→	223
1376	→	551
1376	→	6
1376	→	885
1376	→	159
1376	→	226
2084	→	1396
1616	→	877
2044	→	402
1700	→	2152
1366	→	1358
2314	→	2215
634	→	628
634	→	953
634	→	960
634	→	1029
687	→	1566
323	→	2012
612	→	302
536	→	1923
536	→	2290
881	→	831
1750	→	978
86	→	9
816	→	797
253	→	224
1503	→	738
1669	→	933
518	→	1210
518	→	1574
512	→	983
2238	→	933
760	→	702
760	→	1900
2222	→	924
2305	→	1020
924	→	939
1127	→	1119
1127	→	1502
1277	→	10
702	→	1177
702	→	1249
702	→	1297
552	→	510
552	→	627
552	→	857
251	→	224
251	→	967
251	→	2
251	→	270
2005	→	318
1926	→	1106
2224	→	924
2003	→	318
824	→	797
824	→	1365
207	→	158
207	→	402
207	→	821
2155	→	833
1310	→	224
1610	→	875
1984	→	924
2193	→	448
2199	→	894
6	→	8
6	→	157
6	→	223
6	→	471
6	→	551
6	→	888
554	→	510
554	→	855
302	→	1625
519	→	6
519	→	874
519	→	939
519	→	924
519	→	883
1240	→	870
116	→	88
1571	→	833
1051	→	1038
1051	→	1426
1051	→	1432
577	→	3
577	→	932
577	→	894
577	→	445
577	→	455
577	→	686
577	→	494
577	→	448
577	→	1829
577	→	166
577	→	1602
577	→	1308
982	→	604
982	→	1769
2061	→	402
455	→	445
1041	→	1438
1701	→	1902
1701	→	1933
1701	→	2037
1701	→	2083
288	→	1179
1131	→	1119
1131	→	1519
1279	→	10
1047	→	169
1047	→	1
1047	→	738
1364	→	932
1364	→	894
1364	→	3
1364	→	445
1364	→	455
1364	→	1829
1364	→	166
1364	→	1602
2153	→	833
2134	→	771
270	→	224
776	→	759
657	→	576
665	→	326
350	→	712
831	→	1656
2022	→	1727
1180	→	1167
1242	→	1236
1337	→	1328
1647	→	302
2263	→	224
951	→	1048
951	→	1126
951	→	1276
951	→	1406
803	→	325
1036	→	576
2	→	65
2	→	188
2	→	252
2	→	493
2	→	520
2	→	892
1746	→	975
872	→	452
686	→	1607
4	→	42
4	→	186
4	→	250
4	→	491
4	→	534
4	→	886
232	→	166
118	→	88
118	→	372
118	→	761
118	→	1531
1178	→	1166
449	→	2178
449	→	2200
1018	→	1105
1018	→	1116
1018	→	1843
1174	→	874
1174	→	1020
1174	→	6
1174	→	746
1174	→	10
1174	→	887
400	→	1241
604	→	1268
604	→	1309
1594	→	865
1655	→	924
2036	→	117
2036	→	2068
1425	→	628
1425	→	1732
2151	→	799
1404	→	2027
1404	→	2062
1538	→	771
1035	→	1440
580	→	606
959	→	724
66	→	9
66	→	115
379	→	166
1155	→	227
1997	→	318
795	→	166
795	→	1825
887	→	874
1334	→	1966
1334	→	2156
535	→	510
535	→	833
348	→	319
348	→	650
348	→	1560
1125	→	400
2255	→	933
925	→	1827
2011	→	320
1600	→	166
1369	→	1422
684	→	326
12	→	396
12	→	679
2028	→	117
2028	→	2131
1901	→	1029
169	→	158
169	→	426
989	→	1073
989	→	1130
989	→	1410
989	→	1617
2038	→	10
1296	→	1285
1497	→	706
1013	→	1282
753	→	410
1559	→	799
1632	→	894
1632	→	1654
1632	→	1662
295	→	6
295	→	874
295	→	1020
295	→	746
295	→	10
295	→	887
295	→	939
295	→	924
295	→	883
2177	→	894
2177	→	2221
2177	→	2239
234	→	224
1049	→	1038
1049	→	1430
1049	→	1436
2187	→	895
902	→	95
1207	→	958
1038	→	1262
1038	→	1367
885	→	874
1780	→	1770
42	→	1964
42	→	2154
2163	→	702
2299	→	1020
2257	→	224
579	→	825
453	→	410
189	→	158
189	→	817
950	→	1568
752	→	1646
1756	→	2192
1396	→	1424
856	→	834
2269	→	1770
158	→	428
158	→	737
158	→	823
158	→	1601
1657	→	302
893	→	874
990	→	5
990	→	966
990	→	633
990	→	510
990	→	855
990	→	554
990	→	521
990	→	705
990	→	833
990	→	535
990	→	167
952	→	1
952	→	854
952	→	823
952	→	428
952	→	402
952	→	860
952	→	158
952	→	821
952	→	207
952	→	1030
1429	→	650
17	→	1245
17	→	1295
160	→	3
160	→	455
160	→	1829
160	→	166
160	→	1602
683	→	1037
683	→	1077
683	→	1118
683	→	1395
510	→	633
510	→	859
510	→	966
510	→	1496
1569	→	833
718	→	400
1433	→	658
250	→	1915
250	→	1939
250	→	2094
1439	→	680
1129	→	1119
1129	→	1356
1129	→	1517
68	→	9
68	→	133
68	→	318
159	→	287
159	→	1154
159	→	2060
1407	→	1396
2201	→	916
768	→	326
768	→	1609
2234	→	702
703	→	3
703	→	932
703	→	894
703	→	445
703	→	455
703	→	933
703	→	474
703	→	686
703	→	494
703	→	1829
703	→	166
703	→	1602
703	→	2177
703	→	2255
2324	→	1975
832	→	576
858	→	834
1153	→	227
492	→	445
974	→	702
1087	→	738
693	→	302
2095	→	1396
1828	→	1003
521	→	510
521	→	851
1677	→	941
866	→	575
2226	→	924
829	→	2233
629	→	991
629	→	1593
744	→	1264
1271	→	117
1271	→	1336
1290	→	871
1561	→	799
1649	→	924
1120	→	1152
1959	→	158
711	→	301
1903	→	9
1520	→	738
474	→	445
943	→	291
351	→	719
351	→	771
852	→	834
1375	→	2035
1375	→	2262
1375	→	2270
1942	→	158
1518	→	738
2159	→	833
43	→	9
43	→	117
43	→	115
43	→	404
43	→	4
43	→	695
43	→	66
1269	→	117
1269	→	1327
1967	→	224
1777	→	2184
822	→	797
1449	→	225
1449	→	823
1449	→	428
1449	→	158
1449	→	884
1449	→	454
1449	→	168
1449	→	40
1449	→	233
1449	→	509
1449	→	1
1449	→	817
1449	→	189
1671	→	942
1211	→	1202
1265	→	117
605	→	3
605	→	932
605	→	894
605	→	445
605	→	455
605	→	933
605	→	474
605	→	1829
605	→	166
605	→	1602
605	→	2177
1826	→	1000
1973	→	224
1844	→	874
767	→	1623
1924	→	87
1924	→	2304
875	→	1012
875	→	1676
1897	→	1020
1423	→	607
632	→	354
725	→	702
929	→	663
576	→	1212
576	→	1578
576	→	2325
427	→	403
166	→	1094
166	→	1829
1702	→	854
1702	→	823
1702	→	428
1702	→	402
1702	→	860
1702	→	1
1702	→	158
1702	→	821
1702	→	207
1702	→	1030
1263	→	350
2326	→	1975
2236	→	933
327	→	2
327	→	704
327	→	685
327	→	967
327	→	224
327	→	270
327	→	253
1039	→	1529
1039	→	1695
228	→	1558
228	→	2010
1542	→	790
883	→	874
883	→	1181
883	→	939
883	→	888
883	→	471
883	→	157
883	→	8
883	→	223
883	→	551
883	→	6
883	→	924
1427	→	650
2157	→	833
1115	→	287
1115	→	159
1₁(1122)	→	1123
1₁(351)	→	352
1₁(1365)	→	1366
1₁(293)	→	294
1₁(1404)	→	1405
1₁(186)	→	187
1₁(95)	→	96
1₁(1502)	→	1503
1₁(1941)	→	1942
1₁(1295)	→	1296
1₁(738)	→	739
1₁(1013)	→	1014
1₁(1332)	→	1333
1₁(1375)	→	1376
1₁(1358)	→	1359
1₁(2066)	→	2067
1₁(940)	→	941
1₁(208)	→	209
1₁(611)	→	612
1₁(2045)	→	2046
1₁(1517)	→	1518
1₁(446)	→	447
1₁(1566)	→	1567
1₁(851)	→	852
1₁(962)	→	963
1₁(710)	→	711
1₁(1336)	→	1337
1₁(920)	→	921
1₁(2068)	→	2069
1₁(1202)	→	1203
1₁(1753)	→	1754
1₁(1126)	→	1127
1₁(1438)	→	1439
1₁(1130)	→	1131
1₁(679)	→	680
1₁(763)	→	764
1₁(859)	→	860
1₁(1519)	→	1520
1₁(1003)	→	1004
1₁(772)	→	773
1₁(1676)	→	1677
1₁(1172)	→	1173
1₁(964)	→	965
1₁(168)	→	169
1₁(1103)	→	1104
1₁(985)	→	986
1₁(157)	→	158
1₁(397)	→	398
1₁(708)	→	709
1₁(857)	→	858
1₁(1832)	→	1833
1₁(378)	→	379
1₁(206)	→	207
1₁(604)	→	605
1₁(349)	→	350
1₁(1933)	→	1934
1₁(754)	→	755
1₁(188)	→	189
1₁(571)	→	572
1₁(1262)	→	1263
1₁(970)	→	971
1₁(853)	→	854
1₁(2043)	→	2044
1₁(230)	→	231
1₁(744)	→	745
1₁(833)	→	834
1₁(716)	→	717
1₁(686)	→	687
1₁(1001)	→	1002
1₁(2131)	→	2132
1₁(1118)	→	1119
1₁(1327)	→	1328
1₁(224)	→	225
1₁(2060)	→	2061
1₁(827)	→	828
1₁(399)	→	400
1₁(826)	→	827
1₁(723)	→	724
1₁(937)	→	938
1₁(1297)	→	1298
1₁(377)	→	378
1₁(925)	→	926
1₁(975)	→	976
1₁(511)	→	512
1₁(1958)	→	1959
1₁(737)	→	738
1₁(1357)	→	1358
1₁(1021)	→	1022
1₁(855)	→	856
1₁(877)	→	878
1₁(701)	→	702
1₁(1128)	→	1129
1₁(865)	→	866
1₁(1032)	→	1033
1₁(1564)	→	1565
1₁(1442)	→	1443
1₁(653)	→	654
1₁(924)	→	925
1₁(516)	→	517
1₁(651)	→	652
1₁(800)	→	801
1₁(570)	→	571
1₁(714)	→	715
1₁(1939)	→	1940
1₁(1029)	→	1030
1₁(1284)	→	1285
1₁(161)	→	162
3₂(1980)	→	1981
3₂(1256)	→	1257
3₂(1078)	→	1079
3₂(2306)	→	2307
3₂(1976)	→	1977
3₂(2211)	→	2212
3₂(1983)	→	1984
3₂(2017)	→	2018
2₂(1108)	→	1109
2₂(2016)	→	2017
2₂(2207)	→	2208
2₂(1254)	→	1255
2₂(2312)	→	2313
2₂(2012)	→	2013
2₂(1077)	→	1078
2₂(1251)	→	1252
2₂(2307)	→	2308
2₂(1259)	→	1260
2₂(1084)	→	1085
2₂(1979)	→	1980
2₂(2015)	→	2016
2₂(1105)	→	1106
2₂(1925)	→	1926
2₂(1111)	→	1112
2₂(2020)	→	2021
2₂(1981)	→	1982
2₂(1106)	→	1107
2₂(2209)	→	2210
2₂(1080)	→	1081
2₂(1255)	→	1256
2₂(2215)	→	2216
0₂(2323)	→	2324
0₂(1260)	→	1261
0₂(2311)	→	2312
0₂(2325)	→	2326
0₂(2212)	→	2213
0₂(1974)	→	1975
0₂(2021)	→	2022
3₁(380)	→	381
3₁(884)	→	885
3₁(1276)	→	1277
3₁(751)	→	752
3₁(1368)	→	1369
3₁(923)	→	924
3₁(757)	→	758
3₁(322)	→	323
3₁(2290)	→	2291
3₁(870)	→	871
3₁(918)	→	919
3₁(1124)	→	1125
3₁(957)	→	958
3₁(2150)	→	2151
3₁(746)	→	747
3₁(1496)	→	1497
3₁(163)	→	164
3₁(1166)	→	1167
3₁(1165)	→	1166
3₁(162)	→	163
3₁(396)	→	397
3₁(2298)	→	2299
3₁(2304)	→	2305
3₁(1843)	→	1844
3₁(663)	→	664
3₁(1282)	→	1283
3₁(9)	→	10
3₁(791)	→	792
3₁(747)	→	748
3₁(289)	→	290
3₁(988)	→	989
3₁(158)	→	159
3₁(766)	→	767
3₁(1177)	→	1178
3₁(767)	→	768
3₁(831)	→	832
3₁(956)	→	957
3₁(287)	→	288
3₁(1446)	→	1447
3₁(629)	→	630
3₁(942)	→	943
3₁(584)	→	585
3₁(353)	→	354
3₁(752)	→	753
3₁(1448)	→	1449
3₁(375)	→	376
3₁(829)	→	830
3₁(352)	→	353
3₁(798)	→	799
3₁(1894)	→	1895
3₁(2037)	→	2038
3₁(1529)	→	1530
3₁(948)	→	949
3₁(580)	→	581
3₁(1119)	→	1120
3₁(404)	→	405
3₁(690)	→	691
3₁(888)	→	889
3₁(1168)	→	1169
3₁(1698)	→	1699
3₁(771)	→	772
3₁(899)	→	900
3₁(1777)	→	1778
3₁(1369)	→	1370
3₁(2223)	→	2224
3₁(1896)	→	1897
3₁(997)	→	998
3₁(1123)	→	1124
3₁(949)	→	950
3₁(1000)	→	1001
3₁(743)	→	744
3₁(886)	→	887
3₁(451)	→	452
3₁(705)	→	706
3₁(892)	→	893
3₁(1030)	→	1031
3₁(372)	→	373
3₁(2225)	→	2226
3₁(873)	→	874
3₁(1648)	→	1649
3₁(1756)	→	1757
3₁(225)	→	226
3₁(958)	→	959
3₁(1558)	→	1559
3₁(2296)	→	2297
3₁(1179)	→	1180
3₁(2227)	→	2228
3₁(1278)	→	1279
3₁(1829)	→	1830
3₁(944)	→	945
3₁(1287)	→	1288
3₁(302)	→	303
3₁(1834)	→	1835
3₁(878)	→	879
3₁(1373)	→	1374
3₁(1654)	→	1655
3₁(299)	→	300
3₁(1038)	→	1039
3₁(2221)	→	2222
3₁(1015)	→	1016
3₁(971)	→	972
3₁(762)	→	763
3₁(954)	→	955
3₁(579)	→	580
3₁(1956)	→	1957
3₁(1560)	→	1561
3₁(1699)	→	1700
3₁(882)	→	883
3₁(231)	→	232
3₁(1181)	→	1182
3₁(774)	→	775
3₁(1203)	→	1204
3₁(830)	→	831
3₁(376)	→	377
3₁(610)	→	611
3₁(692)	→	693
3₁(1543)	→	1544
3₁(933)	→	934
5₀(3)	→	5
5₀(6)	→	5
5₀(5)	→	5
5₀(4)	→	5
5₀(2)	→	5
5₀(1)	→	5
3₀(2)	→	6
3₀(6)	→	6
3₀(4)	→	6
3₀(1)	→	6
3₀(3)	→	6
3₀(5)	→	6
1₂(2308)	→	2309
1₂(1975)	→	1976
1₂(1114)	→	1115
1₂(2213)	→	2214
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
2₁(926)	→	927
2₁(87)	→	88
2₁(1239)	→	1240
2₁(1247)	→	1248
2₁(42)	→	43
2₁(876)	→	877
2₁(1996)	→	1997
2₁(794)	→	795
2₁(1288)	→	1289
2₁(1434)	→	1435
2₁(1050)	→	1051
2₁(694)	→	695
2₁(1775)	→	1776
2₁(946)	→	947
2₁(515)	→	516
2₁(1356)	→	1357
2₁(8)	→	9
2₁(695)	→	696
2₁(160)	→	161
2₁(1831)	→	1832
2₁(406)	→	407
2₁(1020)	→	1021
2₁(1286)	→	1287
2₁(1695)	→	1696
2₁(135)	→	136
2₁(796)	→	797
2₁(1334)	→	1335
2₁(1931)	→	1932
2₁(994)	→	995
2₁(740)	→	741
2₁(764)	→	765
2₁(2004)	→	2005
2₁(628)	→	629
2₁(972)	→	973
2₁(864)	→	865
2₁(320)	→	321
2₁(687)	→	688
2₁(117)	→	118
2₁(597)	→	598
2₁(1037)	→	1038
2₁(569)	→	570
2₁(741)	→	742
2₁(449)	→	450
2₁(11)	→	12
2₁(1206)	→	1207
2₁(510)	→	511
2₁(1241)	→	1242
2₁(226)	→	227
2₁(1268)	→	1269
2₁(1615)	→	1616
2₁(896)	→	897
2₁(1331)	→	1332
2₁(575)	→	576
2₁(355)	→	356
2₁(2029)	→	2030
2₁(775)	→	776
2₁(373)	→	374
2₁(986)	→	987
2₁(821)	→	822
2₁(1167)	→	1168
2₁(700)	→	701
2₁(1917)	→	1918
2₁(1094)	→	1095
2₁(1116)	→	1117
2₁(661)	→	662
2₁(576)	→	577
2₁(1073)	→	1074
2₁(709)	→	710
2₁(823)	→	824
2₁(1095)	→	1096
2₁(815)	→	816
2₁(2148)	→	2149
2₁(936)	→	937
2₁(839)	→	840
2₁(288)	→	289
2₁(978)	→	979
2₁(1827)	→	1828
2₁(1396)	→	1397
2₁(448)	→	449
2₁(92)	→	93
2₁(1432)	→	1433
2₁(658)	→	659
2₁(739)	→	740
2₁(403)	→	404
2₁(67)	→	68
2₁(1270)	→	1271
2₁(1048)	→	1049
2₁(1121)	→	1122
2₁(1915)	→	1916
2₁(2027)	→	2028
2₁(89)	→	90
2₁(1436)	→	1437
2₁(15)	→	16
2₁(1770)	→	1771
2₁(608)	→	609
2₁(897)	→	898
2₁(1002)	→	1003
2₁(817)	→	818
2₁(350)	→	351
2₁(894)	→	895
2₁(1245)	→	1246
2₁(1040)	→	1041
2₁(1397)	→	1398
2₁(40)	→	41
2₁(1044)	→	1045
2₁(298)	→	299
2₁(518)	→	519
2₁(1264)	→	1265
2₁(321)	→	322
2₁(1994)	→	1995
2₁(1025)	→	1026
2₁(1012)	→	1013
2₁(133)	→	134
2₁(354)	→	355
2₁(835)	→	836
2₁(2133)	→	2134
2₁(2002)	→	2003
2₁(724)	→	725
2₁(65)	→	66
2₁(1537)	→	1538
2₁(1923)	→	1924
2₁(1154)	→	1155
2₁(1238)	→	1239
2₁(916)	→	917
2₁(292)	→	293
2₁(1440)	→	1441
2₁(707)	→	708
2₁(1171)	→	1172
2₁(1235)	→	1236
2₁(1249)	→	1250
2₁(1593)	→	1594
2₁(945)	→	946
2₁(901)	→	902
2₁(995)	→	996
2₁(1362)	→	1363
2₁(85)	→	86
2₁(1363)	→	1364
2₁(607)	→	608
2₁(863)	→	864
2₁(1754)	→	1755
2₁(713)	→	714
2₁(1696)	→	1697
2₁(300)	→	301
2₁(405)	→	406
2₁(410)	→	411
2₁(2186)	→	2187
2₁(1100)	→	1101
2₁(1902)	→	1903
2₁(115)	→	116
2₁(950)	→	951
2₁(325)	→	326
2₁(1531)	→	1532
2₁(409)	→	410
2₁(609)	→	610
2₁(398)	→	399
2₁(1152)	→	1153
2₁(1700)	→	1701
2₁(715)	→	716
2₁(2035)	→	2036
2₁(834)	→	835
2₁(1774)	→	1775
2₁(1443)	→	1444
2₁(720)	→	721
2₁(749)	→	750
2₁(1289)	→	1290
2₁(838)	→	839
2₁(1097)	→	1098
2₁(976)	→	977
0₁(1033)	→	1034
0₁(1773)	→	1774
0₁(919)	→	920
0₁(765)	→	766
0₁(598)	→	599
0₁(1972)	→	1973
0₁(1398)	→	1399
0₁(428)	→	429
0₁(1309)	→	1310
0₁(748)	→	749
0₁(717)	→	718
0₁(836)	→	837
0₁(683)	→	684
0₁(1212)	→	1213
0₁(1024)	→	1025
0₁(233)	→	234
0₁(880)	→	881
0₁(1726)	→	1727
0₁(966)	→	967
0₁(2256)	→	2257
0₁(799)	→	800
0₁(1372)	→	1373
0₁(1745)	→	1746
0₁(792)	→	793
0₁(691)	→	692
0₁(250)	→	251
0₁(951)	→	952
0₁(1208)	→	1209
0₁(983)	→	984
0₁(879)	→	880
0₁(1966)	→	1967
0₁(269)	→	270
0₁(1201)	→	1202
0₁(252)	→	253
0₁(698)	→	699
0₁(790)	→	791
0₁(1964)	→	1965
0₁(989)	→	990
0₁(769)	→	770
0₁(1447)	→	1448
0₁(583)	→	584
0₁(1757)	→	1758
0₁(867)	→	868
0₁(1035)	→	1036
0₁(993)	→	994
0₁(1701)	→	1702
0₁(1607)	→	1608
0₁(2062)	→	2063
0₁(761)	→	762
0₁(271)	→	272
0₁(426)	→	427
0₁(1367)	→	1368
0₁(402)	→	403
0₁(801)	→	802
0₁(955)	→	956
0₁(326)	→	327
0₁(1210)	→	1211
0₁(953)	→	954
0₁(445)	→	446
0₁(2262)	→	2263
0₁(1285)	→	1286
0₁(660)	→	661
0₁(578)	→	579
0₁(1477)	→	1478
0₁(223)	→	224
0₁(1751)	→	1752
0₀(3)	→	2
0₀(5)	→	2
0₀(2)	→	2
0₀(4)	→	2
0₀(1)	→	2
0₀(6)	→	2
4₀(2)	→	3
4₀(4)	→	3
4₀(3)	→	3
4₀(6)	→	3
4₀(1)	→	3
4₀(5)	→	3
5₁(627)	→	628
5₁(689)	→	690
5₁(2094)	→	2095
5₁(606)	→	607
5₁(534)	→	535
5₁(861)	→	862
5₁(574)	→	575
5₁(324)	→	325
5₁(758)	→	759
5₁(1570)	→	1571
5₁(94)	→	95
5₁(509)	→	510
5₁(947)	→	948
5₁(166)	→	167
5₁(1574)	→	1575
5₁(1018)	→	1019
5₁(928)	→	929
5₁(2268)	→	2269
5₁(2152)	→	2153
5₁(408)	→	409
5₁(1422)	→	1423
5₁(1359)	→	1360
5₁(650)	→	651
5₁(13)	→	14
5₁(1836)	→	1837
5₁(969)	→	970
5₁(960)	→	961
5₁(1031)	→	1032
5₁(704)	→	705
5₁(165)	→	166
5₁(900)	→	901
5₁(828)	→	829
5₁(228)	→	229
5₁(630)	→	631
5₁(1779)	→	1780
5₁(721)	→	722
5₁(1772)	→	1773
5₁(681)	→	682
5₁(536)	→	537
5₁(788)	→	789
5₁(2270)	→	2271
5₁(655)	→	656
5₁(229)	→	230
5₁(1576)	→	1577
5₁(1395)	→	1396
5₁(1042)	→	1043
5₁(1360)	→	1361
5₁(967)	→	968
5₁(654)	→	655
5₁(1102)	→	1103
5₁(992)	→	993
5₁(1410)	→	1411
5₁(722)	→	723
5₁(14)	→	15
5₁(921)	→	922
5₁(1769)	→	1770
5₁(1017)	→	1018
5₁(961)	→	962
5₁(1043)	→	1044
5₁(2158)	→	2159
5₁(1374)	→	1375
5₁(2154)	→	2155
5₁(862)	→	863
5₁(1445)	→	1446
5₁(756)	→	757
5₁(2083)	→	2084
5₁(1023)	→	1024
5₁(2156)	→	2157
5₁(2096)	→	2097
5₁(759)	→	760
5₁(1424)	→	1425
5₁(633)	→	634
5₁(520)	→	521
5₁(1900)	→	1901
5₁(980)	→	981
5₁(1406)	→	1407
5₁(1837)	→	1838
5₁(573)	→	574
5₁(1578)	→	1579
5₁(793)	→	794
5₁(553)	→	554
5₁(2178)	→	2179
5₁(895)	→	896
5₁(664)	→	665
5₁(981)	→	982
5₁(706)	→	707
5₁(789)	→	790
5₁(1568)	→	1569
5₁(551)	→	552
5₁(1408)	→	1409
5₁(1541)	→	1542
5₁(572)	→	573
5₁(968)	→	969
5₁(452)	→	453
5₁(1732)	→	1733
5₁(1697)	→	1698
5₁(1361)	→	1362
4₁(296)	→	297
4₁(685)	→	686
4₁(1771)	→	1772
4₁(1237)	→	1238
4₁(581)	→	582
4₁(2254)	→	2255
4₁(662)	→	663
4₁(1633)	→	1634
4₁(699)	→	700
4₁(1656)	→	1657
4₁(318)	→	319
4₁(999)	→	1000
4₁(512)	→	513
4₁(1330)	→	1331
4₁(915)	→	916
4₁(290)	→	291
4₁(517)	→	518
4₁(1371)	→	1372
4₁(1014)	→	1015
4₁(1101)	→	1102
4₁(898)	→	899
4₁(17)	→	18
4₁(291)	→	292
4₁(374)	→	375
4₁(1045)	→	1046
4₁(16)	→	17
4₁(696)	→	697
4₁(652)	→	653
4₁(2235)	→	2236
4₁(600)	→	601
4₁(347)	→	348
4₁(1776)	→	1777
4₁(1668)	→	1669
4₁(1173)	→	1174
4₁(1478)	→	1479
4₁(450)	→	451
4₁(802)	→	803
4₁(979)	→	980
4₁(2184)	→	2185
4₁(328)	→	329
4₁(1041)	→	1042
4₁(1307)	→	1308
4₁(1428)	→	1429
4₁(88)	→	89
4₁(159)	→	160
4₁(868)	→	869
4₁(1205)	→	1206
4₁(1402)	→	1403
4₁(444)	→	445
4₁(601)	→	602
4₁(12)	→	13
4₁(1022)	→	1023
4₁(514)	→	515
4₁(875)	→	876
4₁(319)	→	320
4₁(1430)	→	1431
4₁(603)	→	604
4₁(1631)	→	1632
4₁(294)	→	295
4₁(750)	→	751
4₁(1096)	→	1097
4₁(1830)	→	1831
4₁(2010)	→	2011
4₁(917)	→	918
4₁(682)	→	683
4₁(2176)	→	2177
4₁(471)	→	472
4₁(1399)	→	1400
4₁(227)	→	228
4₁(1752)	→	1753
4₁(680)	→	681
4₁(2200)	→	2201
4₁(1034)	→	1035
4₁(454)	→	455
4₁(2239)	→	2240
4₁(871)	→	872
4₁(941)	→	942
4₁(1169)	→	1170
4₁(2233)	→	2234
4₁(1403)	→	1404
4₁(773)	→	774
4₁(1617)	→	1618
4₁(599)	→	600
4₁(932)	→	933
4₁(1099)	→	1100
4₁(90)	→	91
4₁(712)	→	713
4₁(1755)	→	1756
4₁(688)	→	689
4₁(755)	→	756
4₁(1825)	→	1826
4₁(987)	→	988
4₁(1625)	→	1626
4₁(602)	→	603
4₁(977)	→	978
4₁(10)	→	11
4₁(2117)	→	2118
4₁(1835)	→	1836
4₁(656)	→	657
4₁(1476)	→	1477
4₁(1039)	→	1040
4₁(1329)	→	1330
4₁(493)	→	494
4₁(1120)	→	1121
4₁(869)	→	870
4₁(1333)	→	1334
4₁(400)	→	401
4₁(91)	→	92
4₁(164)	→	165
4₁(991)	→	992
4₁(697)	→	698
4₁(513)	→	514
4₁(2162)	→	2163
4₁(582)	→	583
4₁(1204)	→	1205
4₁(447)	→	448
4₁(742)	→	743
4₁(1609)	→	1610
4₁(1170)	→	1171
4₁(1599)	→	1600
4₁(1401)	→	1402
4₁(934)	→	935
4₁(93)	→	94
4₁(1601)	→	1602
4₁(407)	→	408
4₁(1400)	→	1401
4₁(631)	→	632
4₁(491)	→	492
4₁(702)	→	703
4₁(935)	→	936
4₁(297)	→	298
4₁(996)	→	997
4₁(1833)	→	1834
4₁(1623)	→	1624
4₁(797)	→	798
4₁(473)	→	474
4₁(1098)	→	1099
4₁(963)	→	964
4₁(2198)	→	2199
4₁(1660)	→	1661
4₁(984)	→	985
4₁(1370)	→	1371
4₁(2237)	→	2238
4₁(1016)	→	1017
4₁(659)	→	660
4₁(301)	→	302
4₁(1662)	→	1663
4₁(719)	→	720
4₁(1426)	→	1427
4₁(874)	→	875
4₁(837)	→	838
4₁(825)	→	826
4₁(323)	→	324
4₁(939)	→	940
4₁(973)	→	974
4₁(1670)	→	1671
4₁(927)	→	928
4₁(1046)	→	1047
4₁(2192)	→	2193
4₁(1749)	→	1750
4₁(1646)	→	1647
4₁(1444)	→	1445
4₁(1328)	→	1329
4₁(1236)	→	1237
4₂(1085)	→	1086
4₂(1257)	→	1258
4₂(1110)	→	1111
4₂(1977)	→	1978
4₂(1081)	→	1082
4₂(2018)	→	2019
4₂(1978)	→	1979
4₂(2206)	→	2207
4₂(1107)	→	1108
4₂(1109)	→	1110
4₂(2208)	→	2209
4₂(1982)	→	1983
4₂(2313)	→	2314
4₂(1086)	→	1087
4₂(2013)	→	2014
4₂(1252)	→	1253
4₂(2309)	→	2310
4₂(2210)	→	2211
4₂(2014)	→	2015
4₂(1112)	→	1113
4₂(1079)	→	1080
4₂(1253)	→	1254
1₀(1)	→	1
1₀(6)	→	1
1₀(5)	→	1
1₀(2)	→	1
1₀(3)	→	1
1₀(4)	→	1
5₂(2214)	→	2215
5₂(1082)	→	1083
5₂(2019)	→	2020
5₂(1113)	→	1114
5₂(2310)	→	2311
5₂(1083)	→	1084
5₂(1258)	→	1259

The automaton is closed under rewriting as it is compatible.