Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3633)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

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

transitions:

854	→	3
854	→	801
854	→	115
854	→	147
1198	→	428
1793	→	1782
2312	→	2145
2312	→	888
2312	→	645
2312	→	643
2312	→	1
2312	→	330
2312	→	774
2312	→	395
2312	→	2160
339	→	3
339	→	801
339	→	115
339	→	125
339	→	147
239	→	185
239	→	456
239	→	629
239	→	657
239	→	787
239	→	882
1268	→	1986
1268	→	2094
429	→	689
429	→	1361
329	→	2144
1627	→	802
494	→	1580
899	→	1875
457	→	450
2166	→	2145
1231	→	1574
818	→	578
818	→	1586
1573	→	747
2178	→	714
89	→	9
89	→	1126
89	→	2
89	→	889
89	→	41
745	→	5
745	→	886
745	→	672
745	→	474
745	→	185
745	→	544
745	→	627
745	→	196
745	→	787
745	→	629
745	→	915
745	→	91
745	→	456
745	→	657
745	→	882
745	→	239
745	→	648
745	→	673
745	→	618
745	→	2139
1674	→	2245
263	→	1216
1737	→	737
1056	→	16
338	→	1233
338	→	1384
1418	→	955
1418	→	916
1418	→	801
1418	→	3
1418	→	543
1418	→	115
1418	→	396
1418	→	186
2322	→	91
2246	→	88
658	→	648
98	→	1678
1787	→	338
2141	→	618
897	→	6
897	→	595
897	→	331
897	→	581
897	→	2208
897	→	2204
286	→	257
286	→	499
286	→	755
286	→	4
286	→	795
2504	→	257
1989	→	185
2349	→	330
2349	→	2421
2512	→	1024
1354	→	574
2518	→	713
2518	→	2523
809	→	193
809	→	1170
10	→	1043
2196	→	428
2277	→	761
2297	→	922
2229	→	256
97	→	1272
2208	→	98
1379	→	618
2198	→	98
2198	→	2405
2137	→	618
2029	→	418
2029	→	1128
2029	→	889
2029	→	9
2029	→	41
2240	→	1919
2240	→	1214
2240	→	906
2240	→	570
2240	→	606
2240	→	283
2240	→	144
2240	→	8
2240	→	236
2240	→	360
2240	→	6
2240	→	595
2240	→	607
2240	→	331
2240	→	2319
2240	→	2208
2240	→	2204
1367	→	801
1367	→	115
1367	→	580
1367	→	285
1367	→	146
1367	→	88
1367	→	195
1367	→	378
1367	→	3
1367	→	125
571	→	819
571	→	886
571	→	672
571	→	474
571	→	5
571	→	185
571	→	237
1391	→	913
640	→	625
1717	→	829
2105	→	428
578	→	2209
2204	→	98
303	→	257
303	→	517
303	→	722
303	→	757
303	→	1177
303	→	4
303	→	2122
303	→	2021
96	→	1250
641	→	2203
2182	→	746
1979	→	186
1280	→	1980
1280	→	2080
2131	→	256
1073	→	1050
1073	→	1421
1209	→	428
2239	→	2302
2396	→	2145
1993	→	185
2206	→	98
655	→	1114
655	→	1146
655	→	1504
655	→	1893
2330	→	146
2330	→	2348
2330	→	2403
2330	→	2417
2330	→	2431
2330	→	2441
628	→	619
628	→	1330
995	→	2116
995	→	2179
811	→	922
956	→	1887
706	→	6
706	→	906
706	→	570
706	→	607
706	→	792
706	→	574
706	→	1354
706	→	1678
706	→	1679
706	→	2289
706	→	98
706	→	2206
1273	→	1551
595	→	570
145	→	115
145	→	580
145	→	285
145	→	146
145	→	88
145	→	195
145	→	378
145	→	3
145	→	957
1575	→	768
2242	→	2231
705	→	1072
705	→	1199
1589	→	325
2097	→	428
18	→	1
18	→	888
18	→	645
18	→	643
18	→	330
18	→	774
18	→	395
18	→	641
18	→	772
18	→	379
18	→	793
18	→	450
18	→	572
18	→	674
18	→	475
18	→	2145
18	→	2160
18	→	2162
2428	→	98
2402	→	2145
2511	→	2532
41	→	9
41	→	1128
3	→	88
3	→	146
3	→	195
3	→	285
3	→	378
3	→	580
1079	→	1050
1079	→	1409
2170	→	675
1003	→	570
1003	→	792
1003	→	6
218	→	185
218	→	472
218	→	618
218	→	659
218	→	789
218	→	884
1565	→	747
1888	→	918
2156	→	2145
2154	→	931
2154	→	1908
500	→	492
617	→	3
617	→	801
617	→	115
617	→	125
617	→	147
617	→	931
617	→	794
617	→	1908
1995	→	257
1324	→	1716
980	→	1730
838	→	625
907	→	979
907	→	1357
1789	→	1782
1226	→	320
1226	→	116
2320	→	989
626	→	616
187	→	1388
646	→	634
646	→	1353
646	→	1978
2539	→	746
9	→	90
9	→	418
914	→	705
914	→	1037
914	→	1796
331	→	1214
331	→	606
331	→	283
331	→	144
331	→	8
331	→	236
331	→	360
331	→	6
331	→	607
331	→	1679
331	→	2289
331	→	2206
5	→	67
5	→	114
5	→	184
5	→	256
5	→	329
5	→	569
2143	→	618
147	→	115
147	→	1166
147	→	1946
1200	→	428
1629	→	454
2002	→	2401
2107	→	330
2107	→	2193
1999	→	257
642	→	634
642	→	216
642	→	618
642	→	2141
642	→	2146
1932	→	956
1567	→	747
1071	→	1050
1071	→	1425
1124	→	1988
1124	→	2096
2524	→	922
1918	→	938
2103	→	428
2289	→	810
1229	→	1459
1229	→	1742
185	→	474
185	→	631
185	→	672
185	→	791
185	→	886
997	→	819
997	→	571
1328	→	1950
1328	→	2276
361	→	330
1991	→	185
1639	→	428
2374	→	256
2505	→	2530
381	→	330
381	→	633
381	→	763
2053	→	419
2053	→	2114
2053	→	2185
2172	→	185
756	→	747
696	→	1638
696	→	1667
2311	→	2503
2311	→	2505
2311	→	2515
2311	→	2517
2311	→	2521
193	→	1116
193	→	1237
193	→	1378
193	→	2165
673	→	648
99	→	5
99	→	819
99	→	886
99	→	672
99	→	474
99	→	185
99	→	237
99	→	571
99	→	646
99	→	216
99	→	642
99	→	544
99	→	627
99	→	196
99	→	2172
473	→	450
1238	→	1228
1238	→	1564
1238	→	1917
1890	→	185
2018	→	146
2018	→	2106
2018	→	2167
2018	→	2191
2018	→	2224
2018	→	2228
2343	→	419
380	→	2163
1	→	40
1	→	124
1	→	215
1	→	266
1	→	358
1	→	594
123	→	17
123	→	1370
1791	→	1782
1817	→	877
1817	→	1925
2406	→	714
542	→	5
542	→	648
542	→	886
542	→	672
542	→	474
542	→	631
542	→	791
542	→	185
542	→	673
786	→	193
2291	→	810
1957	→	988
936	→	720
654	→	1049
654	→	1193
1884	→	761
2244	→	2231
2113	→	491
2113	→	2189
1022	→	2373
1331	→	1323
1081	→	1050
2190	→	747
2418	→	779
570	→	810
570	→	906
570	→	2205
770	→	1889
1387	→	637
1749	→	2197
1749	→	2226
777	→	764
777	→	2078
2037	→	2020
1426	→	674
1173	→	1648
1645	→	815
1215	→	452
747	→	945
747	→	1323
2392	→	2145
2117	→	1252
426	→	2036
723	→	713
1213	→	450
1029	→	808
609	→	570
1194	→	428
748	→	855
1329	→	888
1329	→	645
1329	→	641
1329	→	1
1329	→	330
1329	→	772
1329	→	379
1329	→	2145
1329	→	2162
1683	→	98
1683	→	2177
1676	→	1996
1676	→	2002
1676	→	2173
1676	→	2241
1676	→	2290
573	→	962
2176	→	185
125	→	115
330	→	645
330	→	776
330	→	888
881	→	861
1514	→	1507
1750	→	801
1750	→	115
1750	→	580
1750	→	285
1750	→	146
1750	→	88
1750	→	195
1750	→	378
1750	→	3
1750	→	147
1232	→	830
1729	→	713
1729	→	1891
91	→	915
518	→	492
2238	→	2425
2432	→	491
2533	→	746
1385	→	618
994	→	2130
2390	→	2145
1499	→	185
186	→	396
186	→	955
1127	→	1118
2348	→	2511
619	→	737
1723	→	828
552	→	1
552	→	888
552	→	645
552	→	641
552	→	330
552	→	772
552	→	379
552	→	2145
552	→	2162
912	→	1015
1176	→	831
2005	→	330
1926	→	940
2174	→	185
2003	→	330
824	→	1844
257	→	428
257	→	519
257	→	724
257	→	761
918	→	1929
788	→	779
1358	→	576
1358	→	1515
597	→	570
6	→	8
6	→	144
6	→	236
6	→	283
6	→	360
6	→	606
773	→	764
404	→	6
404	→	906
404	→	792
404	→	810
404	→	570
792	→	779
792	→	1359
116	→	320
921	→	913
921	→	1614
921	→	1736
2081	→	428
88	→	2034
986	→	888
986	→	645
986	→	643
986	→	1
986	→	330
986	→	774
986	→	395
986	→	2145
986	→	2160
1417	→	1990
1417	→	2102
2106	→	2395
1356	→	573
1853	→	1962
1853	→	2278
799	→	1080
799	→	1210
799	→	2067
455	→	434
1234	→	1228
1234	→	1572
1234	→	2050
1234	→	2128
394	→	2108
394	→	2138
394	→	2159
2111	→	491
2111	→	2183
2200	→	98
237	→	185
498	→	97
2158	→	2145
764	→	937
2400	→	2145
1987	→	185
2021	→	2122
2035	→	2020
264	→	1212
1192	→	1172
1192	→	1506
1180	→	1172
1180	→	1513
923	→	1588
951	→	987
853	→	1682
853	→	1794
1516	→	1507
301	→	257
301	→	491
301	→	712
301	→	746
117	→	1452
808	→	2019
2	→	65
2	→	165
2	→	238
2	→	302
2	→	394
2	→	608
2506	→	330
2043	→	2021
1679	→	1668
4	→	42
4	→	163
4	→	217
4	→	300
4	→	380
4	→	596
265	→	193
1178	→	1172
1621	→	794
258	→	1618
258	→	1816
284	→	257
284	→	1179
843	→	336
419	→	534
419	→	1818
520	→	492
520	→	1026
188	→	707
1001	→	2124
1892	→	922
1854	→	595
1854	→	6
1854	→	331
1854	→	2208
1854	→	2204
754	→	98
754	→	1626
1587	→	779
66	→	9
66	→	1788
359	→	330
359	→	1
359	→	361
359	→	641
359	→	772
359	→	379
359	→	2145
359	→	2001
359	→	2158
359	→	2162
359	→	2398
2223	→	713
2223	→	2296
2516	→	185
379	→	330
379	→	641
379	→	772
379	→	1620
1505	→	185
1997	→	257
862	→	4
862	→	286
862	→	802
862	→	534
862	→	757
862	→	517
862	→	722
862	→	303
862	→	419
862	→	890
862	→	2182
862	→	2187
862	→	491
862	→	2109
2184	→	747
887	→	874
421	→	1644
2531	→	1024
800	→	17
1125	→	888
1125	→	645
1125	→	643
1125	→	1
1125	→	330
1125	→	774
1125	→	395
1125	→	2145
1125	→	2160
2075	→	2027
2442	→	256
1369	→	1361
1369	→	1650
738	→	839
738	→	998
581	→	570
1145	→	801
1145	→	115
1145	→	580
1145	→	285
1145	→	146
1145	→	88
1145	→	195
1145	→	378
1145	→	3
1145	→	125
985	→	1998
985	→	2004
985	→	2175
985	→	2222
985	→	2243
1963	→	988
1856	→	1846
1458	→	286
1458	→	4
1458	→	802
1458	→	795
1458	→	2182
450	→	793
2004	→	2399
944	→	98
697	→	4
697	→	286
697	→	802
697	→	795
697	→	2182
1044	→	118
1878	→	761
2077	→	2068
2162	→	2145
2192	→	779
635	→	2169
2202	→	98
758	→	747
1236	→	1228
1236	→	1566
1420	→	1410
1038	→	92
885	→	874
1581	→	768
630	→	619
216	→	185
216	→	449
216	→	647
216	→	778
216	→	873
216	→	5
216	→	237
681	→	1078
681	→	1208
2299	→	320
2045	→	2021
1675	→	1992
1675	→	2076
1675	→	2104
579	→	1
579	→	888
579	→	645
579	→	330
579	→	361
579	→	643
579	→	774
579	→	395
579	→	2145
579	→	2001
579	→	2158
579	→	2398
2079	→	429
1196	→	428
1795	→	1128
825	→	799
2186	→	747
115	→	543
115	→	801
1739	→	840
952	→	98
908	→	1722
2408	→	746
2194	→	794
2139	→	618
1383	→	618
905	→	896
1025	→	886
1025	→	672
1025	→	474
1025	→	185
1025	→	237
1025	→	819
1025	→	5
1025	→	571
1025	→	2172
1025	→	1978
1025	→	634
1025	→	778
1025	→	449
1025	→	2141
1025	→	196
1025	→	544
1025	→	216
1025	→	1669
1025	→	646
1025	→	642
1025	→	99
771	→	327
1512	→	874
1512	→	418
1512	→	9
1512	→	608
1512	→	302
1512	→	165
1512	→	65
1512	→	238
1512	→	394
1512	→	2
1512	→	68
1512	→	887
17	→	1112
17	→	1135
17	→	1498
17	→	1728
17	→	2230
1894	→	810
2160	→	2145
714	→	826
714	→	833
896	→	1877
896	→	1956
360	→	2157
164	→	115
164	→	1158
164	→	1931
1136	→	1861
2168	→	185
1144	→	2112
1144	→	2142
1129	→	1118
1129	→	1782
1129	→	1907
1260	→	648
1260	→	673
68	→	9
68	→	1792
1464	→	770
2404	→	185
2279	→	761
2129	→	429
267	→	257
267	→	1191
762	→	747
762	→	898
832	→	616
215	→	2207
492	→	698
492	→	846
492	→	1738
2109	→	491
2109	→	2187
1862	→	1846
2095	→	428
928	→	2220
1457	→	2195
1457	→	2199
2225	→	491
1677	→	793
1677	→	450
1677	→	330
1677	→	1
1677	→	572
1677	→	674
1677	→	475
1677	→	2145
2221	→	2210
1422	→	1410
1360	→	575
2000	→	2397
1058	→	1050
1058	→	1419
1281	→	886
1281	→	672
1281	→	474
1281	→	569
1281	→	256
1281	→	114
1281	→	67
1281	→	184
1281	→	329
1281	→	5
1281	→	631
1281	→	791
1281	→	185
744	→	1594
1619	→	794
1271	→	537
1649	→	815
2188	→	747
378	→	2161
378	→	2181
2219	→	794
711	→	402
1165	→	1002
775	→	764
92	→	610
1002	→	2052
1002	→	2136
1002	→	2391
2522	→	2231
358	→	2110
358	→	2140
358	→	2155
790	→	779
451	→	1386
1955	→	988
1955	→	2044
2422	→	285
1651	→	816
541	→	1057
541	→	1195
2303	→	2321
2303	→	2342
2426	→	8
2426	→	2468
1171	→	1261
1947	→	956
2051	→	420
2530	→	2538
1113	→	257
2125	→	1251
2115	→	492
2123	→	1253
328	→	1
328	→	888
328	→	645
328	→	643
328	→	330
328	→	774
328	→	395
328	→	359
328	→	2160
328	→	2156
1908	→	931
144	→	1994
144	→	2000
144	→	2171
144	→	2288
43	→	9
43	→	1790
660	→	648
1269	→	648
1269	→	886
1269	→	672
1269	→	474
1269	→	569
1269	→	256
1269	→	114
1269	→	67
1269	→	184
1269	→	329
1269	→	5
1269	→	631
1269	→	791
1269	→	185
1269	→	673
1930	→	904
1876	→	910
961	→	743
1552	→	747
785	→	1227
194	→	1
194	→	888
194	→	645
194	→	330
194	→	361
194	→	641
194	→	772
194	→	379
194	→	643
194	→	774
194	→	395
194	→	2145
194	→	2001
194	→	2158
194	→	2162
194	→	2398
1951	→	988
1951	→	2042
1211	→	428
551	→	1883
551	→	1954
2398	→	2145
2180	→	746
403	→	1235
403	→	1382
403	→	2389
1615	→	793
632	→	619
632	→	1368
966	→	743
1371	→	256
725	→	713
929	→	705
1167	→	397
427	→	2
427	→	418
427	→	9
427	→	889
427	→	41
427	→	320
427	→	116
427	→	89
427	→	2020
427	→	2035
682	→	3
682	→	955
682	→	916
682	→	801
682	→	543
682	→	115
682	→	396
682	→	186
321	→	930
1023	→	2358
1023	→	2407
166	→	115
1920	→	144
1920	→	2298
721	→	2
721	→	874
721	→	418
721	→	9
721	→	68
721	→	887
721	→	320
721	→	116
721	→	89
721	→	2020
721	→	2035
1803	→	720
2359	→	1252
475	→	450
475	→	674
475	→	1355
1981	→	185
2164	→	2145
644	→	634
996	→	2017
996	→	2201
395	→	330
395	→	643
395	→	774
395	→	1
395	→	2145
395	→	2160
1147	→	1136
1147	→	1855
656	→	3
656	→	801
656	→	115
656	→	145
430	→	1270
430	→	1628
1595	→	779
327	→	1070
327	→	1197
607	→	570
607	→	1919
1819	→	876
2001	→	330
1024	→	2329
1024	→	2427
1731	→	835
883	→	874
196	→	185
196	→	627
2227	→	747
1115	→	257
435	→	425
2469	→	761
0₁(95)	→	96
0₁(625)	→	626
0₁(1212)	→	1213
0₁(1409)	→	1410
0₁(622)	→	623
0₁(2106)	→	2107
0₁(576)	→	577
0₁(547)	→	548
0₁(119)	→	120
0₁(358)	→	359
0₁(963)	→	964
0₁(919)	→	920
0₁(962)	→	963
0₁(360)	→	361
0₁(329)	→	330
0₁(1159)	→	1160
0₁(634)	→	635
0₁(785)	→	786
0₁(322)	→	323
0₁(1263)	→	1264
0₁(2000)	→	2001
0₁(1818)	→	1819
0₁(1146)	→	1147
0₁(908)	→	909
0₁(1849)	→	1850
0₁(2505)	→	2506
0₁(1614)	→	1615
0₁(1783)	→	1784
0₁(338)	→	339
0₁(397)	→	398
0₁(394)	→	395
0₁(449)	→	450
0₁(856)	→	857
0₁(1917)	→	1918
0₁(875)	→	876
0₁(1844)	→	1845
0₁(1270)	→	1271
0₁(378)	→	379
0₁(403)	→	404
0₁(2348)	→	2349
0₁(860)	→	861
0₁(652)	→	653
0₁(2004)	→	2005
0₁(571)	→	572
0₁(1326)	→	1327
0₁(1135)	→	1136
0₁(902)	→	903
0₁(1421)	→	1422
0₁(1144)	→	1145
0₁(495)	→	496
0₁(1028)	→	1029
0₁(1002)	→	1003
0₁(1390)	→	1391
0₁(892)	→	893
0₁(474)	→	475
0₁(456)	→	457
0₁(536)	→	537
0₁(1275)	→	1276
0₁(830)	→	831
0₁(1000)	→	1001
0₁(472)	→	473
0₁(937)	→	938
0₁(549)	→	550
0₁(925)	→	926
0₁(2002)	→	2003
0₁(453)	→	454
0₁(1324)	→	1325
0₁(97)	→	98
0₁(1119)	→	1120
0₁(380)	→	381
0₁(676)	→	677
0₁(257)	→	258
0₁(619)	→	620
0₁(1425)	→	1426
0₁(797)	→	798
0₁(1412)	→	1413
0₁(1419)	→	1420
0₁(739)	→	740
0₁(2245)	→	2246
0₁(898)	→	899
0₁(1798)	→	1799
0₁(193)	→	194
0₂(2155)	→	2156
0₂(2144)	→	2145
0₂(1023)	→	1024
0₂(2243)	→	2244
0₂(2401)	→	2402
0₂(2235)	→	2236
0₂(995)	→	996
0₂(2395)	→	2396
0₂(1021)	→	1022
0₂(2152)	→	2153
0₂(2157)	→	2158
0₂(2521)	→	2522
0₂(2530)	→	2531
0₂(2146)	→	2147
0₂(2511)	→	2512
0₂(2216)	→	2217
0₂(2399)	→	2400
0₂(993)	→	994
0₂(2161)	→	2162
0₂(2159)	→	2160
0₂(2389)	→	2390
0₂(1221)	→	1222
0₂(2397)	→	2398
0₂(2163)	→	2164
0₂(2391)	→	2392
0₂(2230)	→	2231
0₂(2241)	→	2242
0₂(1217)	→	1218
0₂(1254)	→	1255
0₂(2165)	→	2166
3₂(2213)	→	2214
3₂(2238)	→	2239
3₂(991)	→	992
3₂(1223)	→	1224
3₂(1019)	→	1020
3₂(1259)	→	1260
3₂(2147)	→	2148
3₂(1258)	→	1259
3₂(2210)	→	2211
3₂(2214)	→	2215
3₂(2074)	→	2075
3₂(2148)	→	2149
3₂(1218)	→	1219
1₂(2073)	→	2074
1₂(2233)	→	2234
1₂(2068)	→	2069
1₂(1257)	→	1258
1₂(2122)	→	2123
1₂(1252)	→	1253
1₁(192)	→	193
1₁(941)	→	942
1₁(1368)	→	1369
1₁(923)	→	924
1₁(1978)	→	1979
1₁(1644)	→	1645
1₁(1454)	→	1455
1₁(165)	→	166
1₁(428)	→	429
1₁(433)	→	434
1₁(13)	→	14
1₁(1126)	→	1127
1₁(163)	→	164
1₁(1166)	→	1167
1₁(1929)	→	1930
1₁(1117)	→	1118
1₁(399)	→	400
1₁(396)	→	397
1₁(494)	→	495
1₁(985)	→	986
1₁(814)	→	815
1₁(1907)	→	1908
1₁(747)	→	748
1₁(114)	→	115
1₁(840)	→	841
1₁(1745)	→	1746
1₁(695)	→	696
1₁(1792)	→	1793
1₁(960)	→	961
1₁(900)	→	901
1₁(956)	→	957
1₁(1158)	→	1159
1₁(1847)	→	1848
1₁(1050)	→	1051
1₁(849)	→	850
1₁(1456)	→	1457
1₁(915)	→	916
1₁(793)	→	794
1₁(946)	→	947
1₁(1738)	→	1739
1₁(693)	→	694
1₁(534)	→	535
1₁(1676)	→	1677
1₁(124)	→	125
1₁(2421)	→	2422
1₁(333)	→	334
1₁(144)	→	145
1₁(748)	→	749
1₁(879)	→	880
1₁(1746)	→	1747
1₁(185)	→	186
1₁(1620)	→	1621
1₁(1790)	→	1791
1₁(802)	→	803
1₁(949)	→	950
1₁(1054)	→	1055
1₁(850)	→	851
1₁(187)	→	188
1₁(1618)	→	1619
1₁(890)	→	891
1₁(539)	→	540
1₁(611)	→	612
1₁(1273)	→	1274
1₁(981)	→	982
1₁(1052)	→	1053
1₁(146)	→	147
1₁(768)	→	769
1₁(1648)	→	1649
1₁(1266)	→	1267
1₁(2307)	→	2308
1₁(2311)	→	2312
1₁(940)	→	941
1₁(655)	→	656
1₁(1261)	→	1262
1₁(1278)	→	1279
1₁(740)	→	741
1₁(839)	→	840
1₁(1919)	→	1920
1₁(1231)	→	1232
1₁(837)	→	838
1₁(648)	→	649
1₁(189)	→	190
1₁(2128)	→	2129
1₁(824)	→	825
1₁(320)	→	321
1₁(930)	→	931
1₁(1161)	→	1162
1₁(2078)	→	2079
1₁(1139)	→	1140
1₁(1788)	→	1789
1₁(1128)	→	1129
1₁(2193)	→	2194
1₁(1802)	→	1803
1₁(17)	→	18
1₁(1361)	→	1362
1₁(753)	→	754
1₁(610)	→	611
1₁(1674)	→	1675
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
5₂(996)	→	997
5₂(2149)	→	2150
5₂(2237)	→	2238
5₂(2319)	→	2320
5₂(2021)	→	2022
5₂(2215)	→	2216
5₂(1024)	→	1025
5₂(2069)	→	2070
5₂(988)	→	989
5₂(2145)	→	2146
5₂(1216)	→	1217
5₂(1016)	→	1017
5₂(2234)	→	2235
5₂(1253)	→	1254
5₂(2151)	→	2152
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
2₁(1123)	→	1124
2₁(699)	→	700
2₁(2102)	→	2103
2₁(1233)	→	1234
2₁(1996)	→	1997
2₁(794)	→	795
2₁(283)	→	284
2₁(807)	→	808
2₁(1748)	→	1749
2₁(1460)	→	1461
2₁(191)	→	192
2₁(1366)	→	1367
2₁(2532)	→	2533
2₁(1230)	→	1231
2₁(2104)	→	2105
2₁(932)	→	933
2₁(1172)	→	1173
2₁(1507)	→	1508
2₁(1197)	→	1198
2₁(934)	→	935
2₁(624)	→	625
2₁(2052)	→	2053
2₁(544)	→	545
2₁(979)	→	980
2₁(774)	→	775
2₁(1883)	→	1884
2₁(2276)	→	2277
2₁(2305)	→	2306
2₁(1626)	→	1627
2₁(499)	→	500
2₁(906)	→	907
2₁(1877)	→	1878
2₁(430)	→	431
2₁(2309)	→	2310
2₁(650)	→	651
2₁(764)	→	765
2₁(2179)	→	2180
2₁(1574)	→	1575
2₁(1511)	→	1512
2₁(629)	→	630
2₁(1801)	→	1802
2₁(811)	→	812
2₁(2306)	→	2307
2₁(613)	→	614
2₁(716)	→	717
2₁(833)	→	834
2₁(574)	→	575
2₁(2503)	→	2504
2₁(1193)	→	1194
2₁(493)	→	494
2₁(94)	→	95
2₁(1037)	→	1038
2₁(1388)	→	1389
2₁(928)	→	929
2₁(11)	→	12
2₁(763)	→	764
2₁(578)	→	579
2₁(744)	→	745
2₁(616)	→	617
2₁(957)	→	958
2₁(980)	→	981
2₁(1228)	→	1229
2₁(821)	→	822
2₁(1208)	→	1209
2₁(782)	→	783
2₁(2431)	→	2432
2₁(431)	→	432
2₁(1359)	→	1360
2₁(738)	→	739
2₁(2468)	→	2469
2₁(2407)	→	2408
2₁(1638)	→	1639
2₁(2096)	→	2097
2₁(2405)	→	2406
2₁(1112)	→	1113
2₁(10)	→	11
2₁(718)	→	719
2₁(2310)	→	2311
2₁(92)	→	93
2₁(983)	→	984
2₁(285)	→	286
2₁(1463)	→	1464
2₁(651)	→	652
2₁(451)	→	452
2₁(984)	→	985
2₁(2108)	→	2109
2₁(1121)	→	1122
2₁(858)	→	859
2₁(2094)	→	2095
2₁(964)	→	965
2₁(452)	→	453
2₁(15)	→	16
2₁(420)	→	421
2₁(1210)	→	1211
2₁(492)	→	493
2₁(1744)	→	1745
2₁(848)	→	849
2₁(631)	→	632
2₁(1229)	→	1230
2₁(904)	→	905
2₁(2177)	→	2178
2₁(2112)	→	2113
2₁(1199)	→	1200
2₁(16)	→	17
2₁(2110)	→	2111
2₁(618)	→	619
2₁(918)	→	919
2₁(1237)	→	1238
2₁(1264)	→	1265
2₁(256)	→	257
2₁(1994)	→	1995
2₁(1027)	→	1028
2₁(701)	→	702
2₁(1214)	→	1215
2₁(1122)	→	1123
2₁(1114)	→	1115
2₁(1276)	→	1277
2₁(805)	→	806
2₁(835)	→	836
2₁(1227)	→	1228
2₁(454)	→	455
2₁(813)	→	814
2₁(2080)	→	2081
2₁(765)	→	766
2₁(878)	→	879
2₁(910)	→	911
2₁(702)	→	703
2₁(302)	→	303
2₁(1669)	→	1670
2₁(1671)	→	1672
2₁(819)	→	820
2₁(1235)	→	1236
2₁(1462)	→	1463
2₁(752)	→	753
2₁(737)	→	738
2₁(1195)	→	1196
2₁(2538)	→	2539
2₁(750)	→	751
2₁(776)	→	777
2₁(121)	→	122
2₁(1736)	→	1737
2₁(901)	→	902
2₁(1782)	→	1783
2₁(874)	→	875
2₁(1363)	→	1364
2₁(836)	→	837
2₁(422)	→	423
2₁(497)	→	498
2₁(627)	→	628
2₁(889)	→	890
2₁(425)	→	426
2₁(1389)	→	1390
2₁(1174)	→	1175
2₁(326)	→	327
2₁(713)	→	714
2₁(1846)	→	1847
2₁(300)	→	301
2₁(842)	→	843
2₁(517)	→	518
2₁(1797)	→	1798
2₁(924)	→	925
2₁(880)	→	881
2₁(2342)	→	2343
2₁(496)	→	497
2₁(519)	→	520
2₁(418)	→	419
2₁(537)	→	538
2₁(1509)	→	1510
2₁(1170)	→	1171
2₁(91)	→	92
2₁(767)	→	768
2₁(999)	→	1000
2₁(259)	→	260
2₁(861)	→	862
2₁(950)	→	951
2₁(2181)	→	2182
2₁(12)	→	13
2₁(491)	→	492
2₁(325)	→	326
2₁(783)	→	784
2₁(2224)	→	2225
2₁(424)	→	425
2₁(855)	→	856
2₁(852)	→	853
2₁(1580)	→	1581
2₁(751)	→	752
2₁(1272)	→	1273
2₁(2114)	→	2115
2₁(772)	→	773
2₁(2195)	→	2196
2₁(1785)	→	1786
2₁(2304)	→	2305
2₁(266)	→	267
2₁(1998)	→	1999
2₁(831)	→	832
2₁(720)	→	721
2₁(324)	→	325
2₁(2278)	→	2279
2₁(742)	→	743
2₁(801)	→	802
2₁(766)	→	767
2₁(816)	→	817
5₁(184)	→	185
5₁(337)	→	338
5₁(90)	→	91
5₁(857)	→	858
5₁(572)	→	573
5₁(743)	→	744
5₁(692)	→	693
5₁(2403)	→	2404
5₁(1049)	→	1050
5₁(2171)	→	2172
5₁(263)	→	264
5₁(1177)	→	1178
5₁(1053)	→	1054
5₁(236)	→	237
5₁(877)	→	878
5₁(643)	→	644
5₁(1072)	→	1073
5₁(945)	→	946
5₁(1378)	→	1379
5₁(2050)	→	2051
5₁(903)	→	904
5₁(1057)	→	1058
5₁(982)	→	983
5₁(321)	→	322
5₁(1357)	→	1358
5₁(1504)	→	1505
5₁(1668)	→	1669
5₁(2308)	→	2309
5₁(817)	→	818
5₁(780)	→	781
5₁(959)	→	960
5₁(575)	→	576
5₁(2173)	→	2174
5₁(1453)	→	1454
5₁(1455)	→	1456
5₁(672)	→	673
5₁(118)	→	119
5₁(98)	→	99
5₁(2321)	→	2322
5₁(796)	→	797
5₁(188)	→	189
5₁(853)	→	854
5₁(2138)	→	2139
5₁(2140)	→	2141
5₁(1498)	→	1499
5₁(258)	→	259
5₁(238)	→	239
5₁(1980)	→	1981
5₁(1457)	→	1458
5₁(1986)	→	1987
5₁(543)	→	544
5₁(429)	→	430
5₁(1990)	→	1991
5₁(2167)	→	2168
5₁(920)	→	921
5₁(1171)	→	1172
5₁(803)	→	804
5₁(2136)	→	2137
5₁(1749)	→	1750
5₁(217)	→	218
5₁(1138)	→	1139
5₁(1078)	→	1079
5₁(215)	→	216
5₁(1118)	→	1119
5₁(894)	→	895
5₁(899)	→	900
5₁(1461)	→	1462
5₁(1070)	→	1071
5₁(186)	→	187
5₁(570)	→	571
5₁(645)	→	646
5₁(698)	→	699
5₁(2175)	→	2176
5₁(2142)	→	2143
5₁(694)	→	695
5₁(891)	→	892
5₁(847)	→	848
5₁(1889)	→	1890
5₁(14)	→	15
5₁(708)	→	709
5₁(1143)	→	1144
5₁(1992)	→	1993
5₁(1784)	→	1785
5₁(2017)	→	2018
5₁(696)	→	697
5₁(1051)	→	1052
5₁(1370)	→	1371
5₁(1988)	→	1989
5₁(2329)	→	2330
5₁(1459)	→	1460
5₁(637)	→	638
5₁(1080)	→	1081
5₁(657)	→	658
5₁(1743)	→	1744
5₁(1851)	→	1852
5₁(1382)	→	1383
5₁(1411)	→	1412
5₁(659)	→	660
5₁(2515)	→	2516
5₁(1800)	→	1801
5₁(1355)	→	1356
5₁(1848)	→	1849
5₁(1325)	→	1326
5₁(1274)	→	1275
5₁(535)	→	536
5₁(700)	→	701
5₁(1191)	→	1192
5₁(402)	→	403
5₁(1164)	→	1165
5₁(264)	→	265
5₁(812)	→	813
5₁(1160)	→	1161
5₁(419)	→	420
5₁(647)	→	648
5₁(714)	→	715
5₁(913)	→	914
5₁(922)	→	923
5₁(398)	→	399
5₁(332)	→	333
5₁(675)	→	676
5₁(653)	→	654
5₁(1179)	→	1180
5₁(641)	→	642
5₁(633)	→	634
5₁(195)	→	196
5₁(931)	→	932
5₁(639)	→	640
5₁(548)	→	549
5₁(829)	→	830
5₁(1384)	→	1385
5₁(1262)	→	1263
5₁(649)	→	650
4₀(3)	→	2
4₀(5)	→	2
4₀(2)	→	2
4₀(4)	→	2
4₀(1)	→	2
4₀(6)	→	2
1₀(2)	→	3
1₀(4)	→	3
1₀(3)	→	3
1₀(6)	→	3
1₀(1)	→	3
1₀(5)	→	3
3₁(434)	→	435
3₁(916)	→	917
3₁(1682)	→	1683
3₁(707)	→	708
3₁(606)	→	607
3₁(827)	→	828
3₁(2290)	→	2291
3₁(1279)	→	1280
3₁(947)	→	948
3₁(1353)	→	1354
3₁(917)	→	918
3₁(1816)	→	1817
3₁(1162)	→	1163
3₁(1515)	→	1516
3₁(741)	→	742
3₁(1650)	→	1651
3₁(541)	→	542
3₁(823)	→	824
3₁(9)	→	10
3₁(791)	→	792
3₁(1362)	→	1363
3₁(1675)	→	1676
3₁(117)	→	118
3₁(815)	→	816
3₁(841)	→	842
3₁(787)	→	788
3₁(1628)	→	1629
3₁(1716)	→	1717
3₁(1893)	→	1894
3₁(704)	→	705
3₁(709)	→	710
3₁(1513)	→	1514
3₁(799)	→	800
3₁(636)	→	637
3₁(400)	→	401
3₁(828)	→	829
3₁(335)	→	336
3₁(820)	→	821
3₁(1055)	→	1056
3₁(1506)	→	1507
3₁(1120)	→	1121
3₁(1673)	→	1674
3₁(681)	→	682
3₁(851)	→	852
3₁(1747)	→	1748
3₁(680)	→	681
3₁(2417)	→	2418
3₁(1026)	→	1027
3₁(580)	→	581
3₁(1667)	→	1668
3₁(1267)	→	1268
3₁(935)	→	936
3₁(336)	→	337
3₁(1386)	→	1387
3₁(795)	→	796
3₁(1323)	→	1324
3₁(612)	→	613
3₁(2222)	→	2223
3₁(2427)	→	2428
3₁(2199)	→	2200
3₁(909)	→	910
3₁(1140)	→	1141
3₁(540)	→	541
3₁(2425)	→	2426
3₁(943)	→	944
3₁(1887)	→	1888
3₁(1417)	→	1418
3₁(1268)	→	1269
3₁(654)	→	655
3₁(938)	→	939
3₁(722)	→	723
3₁(1875)	→	1876
3₁(1141)	→	1142
3₁(1931)	→	1932
3₁(778)	→	779
3₁(1364)	→	1365
3₁(705)	→	706
3₁(2517)	→	2518
3₁(620)	→	621
3₁(955)	→	956
3₁(958)	→	959
3₁(806)	→	807
3₁(323)	→	324
3₁(2303)	→	2304
3₁(804)	→	805
3₁(190)	→	191
3₁(1043)	→	1044
3₁(927)	→	928
3₁(2201)	→	2202
3₁(594)	→	595
3₁(401)	→	402
3₁(2288)	→	2289
3₁(1670)	→	1671
3₁(1852)	→	1853
3₁(93)	→	94
3₁(621)	→	622
3₁(327)	→	328
3₁(1799)	→	1800
3₁(1925)	→	1926
3₁(678)	→	679
3₁(2207)	→	2208
3₁(577)	→	578
3₁(1586)	→	1587
3₁(2191)	→	2192
3₁(1124)	→	1125
3₁(262)	→	263
3₁(450)	→	451
3₁(569)	→	570
3₁(1416)	→	1417
3₁(2197)	→	2198
3₁(2203)	→	2204
3₁(1678)	→	1679
3₁(2205)	→	2206
3₁(1280)	→	1281
3₁(690)	→	691
3₁(911)	→	912
3₁(573)	→	574
3₁(1142)	→	1143
3₁(715)	→	716
3₁(1327)	→	1328
3₁(614)	→	615
3₁(550)	→	551
3₁(724)	→	725
3₁(334)	→	335
3₁(1415)	→	1416
3₁(895)	→	896
3₁(596)	→	597
3₁(1728)	→	1729
3₁(789)	→	790
3₁(635)	→	636
3₁(679)	→	680
3₁(1594)	→	1595
3₁(712)	→	713
3₁(1136)	→	1137
3₁(330)	→	331
3₁(120)	→	121
3₁(998)	→	999
3₁(784)	→	785
3₁(1414)	→	1415
3₁(116)	→	117
3₁(1946)	→	1947
3₁(1722)	→	1723
3₁(939)	→	940
3₁(608)	→	609
3₁(1163)	→	1164
3₁(876)	→	877
3₁(546)	→	547
3₁(948)	→	949
4₁(2183)	→	2184
4₁(1566)	→	1567
4₁(1845)	→	1846
4₁(888)	→	889
4₁(2226)	→	2227
4₁(1365)	→	1366
4₁(1796)	→	1797
4₁(1855)	→	1856
4₁(65)	→	66
4₁(261)	→	262
4₁(677)	→	678
4₁(1116)	→	1117
4₁(538)	→	539
4₁(1330)	→	1331
4₁(426)	→	427
4₁(965)	→	966
4₁(615)	→	616
4₁(40)	→	41
4₁(689)	→	690
4₁(1413)	→	1414
4₁(822)	→	823
4₁(1786)	→	1787
4₁(710)	→	711
4₁(1173)	→	1174
4₁(2523)	→	2524
4₁(2130)	→	2131
4₁(551)	→	552
4₁(703)	→	704
4₁(1175)	→	1176
4₁(912)	→	913
4₁(859)	→	860
4₁(749)	→	750
4₁(331)	→	332
4₁(882)	→	883
4₁(798)	→	799
4₁(115)	→	116
4₁(88)	→	89
4₁(779)	→	780
4₁(781)	→	782
4₁(2187)	→	2188
4₁(834)	→	835
4₁(1794)	→	1795
4₁(1452)	→	1453
4₁(1588)	→	1589
4₁(638)	→	639
4₁(1265)	→	1266
4₁(122)	→	123
4₁(1730)	→	1731
4₁(2189)	→	2190
4₁(933)	→	934
4₁(623)	→	624
4₁(770)	→	771
4₁(96)	→	97
4₁(67)	→	68
4₁(2296)	→	2297
4₁(691)	→	692
4₁(1672)	→	1673
4₁(1508)	→	1509
4₁(1551)	→	1552
4₁(2185)	→	2186
4₁(1572)	→	1573
4₁(42)	→	43
4₁(1742)	→	1743
4₁(755)	→	756
4₁(2373)	→	2374
4₁(1891)	→	1892
4₁(886)	→	887
4₁(746)	→	747
4₁(1277)	→	1278
4₁(757)	→	758
4₁(2298)	→	2299
4₁(810)	→	811
4₁(893)	→	894
4₁(846)	→	847
4₁(432)	→	433
4₁(769)	→	770
4₁(674)	→	675
4₁(2169)	→	2170
4₁(1853)	→	1854
4₁(926)	→	927
4₁(2228)	→	2229
4₁(1861)	→	1862
4₁(2441)	→	2442
4₁(1850)	→	1851
4₁(761)	→	762
4₁(826)	→	827
4₁(1001)	→	1002
4₁(951)	→	952
4₁(1410)	→	1411
4₁(423)	→	424
4₁(873)	→	874
4₁(719)	→	720
4₁(1510)	→	1511
4₁(2302)	→	2303
4₁(1137)	→	1138
4₁(421)	→	422
4₁(896)	→	897
4₁(1564)	→	1565
4₁(942)	→	943
4₁(884)	→	885
4₁(808)	→	809
4₁(717)	→	718
4₁(8)	→	9
4₁(907)	→	908
4₁(260)	→	261
4₁(1328)	→	1329
4₁(545)	→	546
2₂(2209)	→	2210
2₂(989)	→	990
2₂(2071)	→	2072
2₂(2218)	→	2219
2₂(2076)	→	2077
2₂(1018)	→	1019
2₂(2217)	→	2218
2₂(2022)	→	2023
2₂(1219)	→	1220
2₂(2153)	→	2154
2₂(2042)	→	2043
2₂(1020)	→	1021
2₂(2020)	→	2021
2₂(1222)	→	1223
2₂(2070)	→	2071
2₂(2211)	→	2212
2₂(1255)	→	1256
2₂(2358)	→	2359
2₂(2044)	→	2045
2₂(2116)	→	2117
2₂(2024)	→	2025
2₂(2232)	→	2233
2₂(2067)	→	2068
2₂(1017)	→	1018
2₂(1220)	→	1221
2₂(2026)	→	2027
2₂(2220)	→	2221
2₂(2027)	→	2028
2₂(990)	→	991
2₂(992)	→	993
2₂(1251)	→	1252
2₂(1224)	→	1225
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
4₂(1022)	→	1023
4₂(2239)	→	2240
4₂(2231)	→	2232
4₂(2019)	→	2020
4₂(987)	→	988
4₂(1250)	→	1251
4₂(994)	→	995
4₂(2023)	→	2024
4₂(2036)	→	2037
4₂(1225)	→	1226
4₂(2124)	→	2125
4₂(1950)	→	1951
4₂(1956)	→	1957
4₂(1015)	→	1016
4₂(1962)	→	1963
4₂(2072)	→	2073
4₂(1954)	→	1955
4₂(2212)	→	2213
4₂(1256)	→	1257
4₂(2236)	→	2237
4₂(2025)	→	2026
4₂(2034)	→	2035
4₂(2150)	→	2151
4₂(2028)	→	2029

The automaton is closed under rewriting as it is compatible.