Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4824)

The rewrite relation of the following TRS is considered.

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

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:

1182	→	1171
1839	→	214
730	→	720
854	→	2019
1659	→	1647
1793	→	589
1793	→	1899
1197	→	1171
279	→	231
279	→	598
2386	→	8
588	→	5
588	→	710
588	→	421
588	→	834
588	→	667
588	→	378
588	→	833
588	→	590
239	→	1658
239	→	1734
239	→	1954
1868	→	850
1301	→	545
329	→	300
329	→	731
329	→	1946
2119	→	1201
869	→	1297
958	→	840
534	→	735
534	→	1224
2166	→	1325
1231	→	164
1231	→	920
1231	→	758
1231	→	326
1231	→	165
1231	→	85
1231	→	241
1231	→	376
1231	→	1
1231	→	936
2360	→	231
2150	→	484
1674	→	844
1106	→	833
1106	→	950
1106	→	533
1106	→	5
1106	→	510
1106	→	569
1106	→	377
1106	→	590
1406	→	620
1406	→	3
1406	→	231
1406	→	281
1406	→	1533
1406	→	1545
1056	→	579
1056	→	633
1056	→	125
1056	→	85
1056	→	241
1056	→	376
1056	→	758
1056	→	326
1056	→	165
1056	→	1
2152	→	484
860	→	851
732	→	720
2268	→	1665
1117	→	231
874	→	550
1007	→	876
1007	→	114
1007	→	85
1007	→	241
1007	→	376
1007	→	1016
1007	→	758
1007	→	326
1007	→	165
1007	→	1
1007	→	1270
1007	→	166
10	→	87
10	→	543
10	→	801
2196	→	1325
1163	→	300
742	→	693
1261	→	484
734	→	720
1694	→	978
1694	→	875
1694	→	589
1694	→	1
1694	→	579
1694	→	633
1694	→	114
1694	→	989
2142	→	484
15	→	2218
2029	→	1261
1199	→	1171
640	→	1950
1578	→	1962
2105	→	85
578	→	4
578	→	988
578	→	865
578	→	748
578	→	115
578	→	979
578	→	859
578	→	759
448	→	17
2069	→	1086
374	→	1198
374	→	1590
374	→	2133
374	→	2173
2204	→	599
641	→	374
2182	→	1325
1280	→	535
1073	→	186
2099	→	1152
1140	→	2259
1140	→	2271
1140	→	2327
882	→	647
1593	→	1578
352	→	300
352	→	729
352	→	1944
728	→	6
728	→	935
728	→	482
728	→	919
728	→	440
728	→	9
728	→	842
728	→	591
728	→	570
728	→	185
728	→	685
728	→	62
728	→	998
1195	→	1171
2040	→	1460
511	→	485
511	→	676
511	→	1544
145	→	114
145	→	1279
145	→	1
145	→	844
145	→	1827
145	→	1835
122	→	1162
122	→	2098
2217	→	1094
2217	→	2351
466	→	441
260	→	231
260	→	1467
1589	→	1578
1953	→	9
550	→	1074
550	→	1656
550	→	1958
18	→	1
18	→	579
18	→	633
18	→	166
18	→	895
18	→	876
18	→	125
18	→	928
18	→	164
18	→	936
1230	→	2110
1230	→	2118
1230	→	2165
1230	→	2251
1141	→	950
1141	→	533
1141	→	5
1141	→	510
1141	→	569
1141	→	377
815	→	16
41	→	9
41	→	919
41	→	440
41	→	842
41	→	782
41	→	349
41	→	163
41	→	63
41	→	230
41	→	422
41	→	6
41	→	570
41	→	185
41	→	685
41	→	62
41	→	998
2260	→	748
39	→	9
39	→	194
39	→	465
39	→	695
39	→	927
39	→	1307
3	→	38
3	→	124
3	→	280
3	→	308
3	→	438
3	→	784
1362	→	599
2063	→	1086
2278	→	85
1727	→	447
1254	→	484
1011	→	998
817	→	1246
1789	→	1766
405	→	377
1119	→	231
1294	→	535
146	→	997
2252	→	719
2252	→	2343
9	→	216
9	→	482
9	→	708
9	→	935
9	→	1311
5	→	61
5	→	146
5	→	278
5	→	299
5	→	420
5	→	747
147	→	114
2107	→	85
443	→	1397
95	→	5
95	→	590
95	→	533
95	→	950
95	→	377
95	→	439
95	→	1460
2103	→	85
1055	→	2100
1055	→	2106
1027	→	2062
1027	→	2084
1027	→	2143
1027	→	2279
1027	→	2295
483	→	441
1252	→	895
1252	→	875
1252	→	589
1252	→	114
1252	→	758
1252	→	326
1252	→	165
1252	→	85
1252	→	241
1252	→	376
1252	→	1
1252	→	166
1252	→	876
692	→	1170
692	→	1200
692	→	1324
2172	→	1325
756	→	1018
756	→	1037
1970	→	2068
1970	→	2086
1970	→	2149
1970	→	2203
1970	→	2285
1970	→	2301
696	→	686
1095	→	833
1095	→	590
1095	→	1426
1095	→	569
1095	→	510
1095	→	533
1095	→	950
1095	→	377
674	→	1196
674	→	1577
674	→	2195
2358	→	1086
1866	→	850
749	→	1302
892	→	884
193	→	94
673	→	1447
1900	→	9
1159	→	1045
62	→	9
62	→	185
62	→	440
62	→	685
62	→	919
1833	→	833
1833	→	950
1833	→	533
1833	→	5
1833	→	510
1833	→	569
1833	→	377
1833	→	590
1898	→	121
2280	→	589
2344	→	825
1	→	85
1	→	165
1	→	241
1	→	326
1	→	376
1	→	758
1105	→	2261
1105	→	2273
1105	→	2333
123	→	1
123	→	579
123	→	633
123	→	125
123	→	978
123	→	989
40	→	2104
1077	→	188
1791	→	589
841	→	1
841	→	895
841	→	875
841	→	589
841	→	114
841	→	166
841	→	876
841	→	145
826	→	990
1308	→	748
1902	→	9
542	→	3
542	→	441
542	→	620
542	→	231
542	→	483
1591	→	1578
1026	→	2209
1009	→	998
1957	→	9
936	→	920
936	→	1300
840	→	1662
840	→	1742
840	→	1952
840	→	2265
2244	→	676
1299	→	586
1663	→	1647
2113	→	231
716	→	1258
1545	→	1533
549	→	2030
165	→	1016
165	→	1999
755	→	1151
755	→	1164
901	→	2185
1004	→	2385
1267	→	484
1994	→	9
570	→	842
570	→	1357
965	→	17
2392	→	850
590	→	833
2117	→	1201
2334	→	9
987	→	978
1661	→	1647
1278	→	441
1312	→	748
2288	→	589
606	→	239
606	→	1072
748	→	865
748	→	893
748	→	988
1700	→	820
1366	→	599
634	→	650
634	→	867
423	→	377
423	→	484
1676	→	812
1676	→	1897
2310	→	850
1161	→	300
125	→	114
125	→	1291
86	→	9
86	→	214
86	→	467
86	→	706
86	→	933
86	→	1309
86	→	825
86	→	782
86	→	349
86	→	163
86	→	63
86	→	230
86	→	422
86	→	6
86	→	301
86	→	41
86	→	1009
86	→	1994
1398	→	638
675	→	4
675	→	988
675	→	865
675	→	748
675	→	850
675	→	783
675	→	1312
675	→	1308
1643	→	737
1729	→	1722
2250	→	719
2250	→	2341
2304	→	850
233	→	368
309	→	300
309	→	1948
1654	→	2094
1654	→	2108
1005	→	2379
518	→	1881
783	→	748
783	→	850
1971	→	928
1971	→	164
1971	→	1
1971	→	936
385	→	1194
385	→	1592
385	→	2116
385	→	2163
2087	→	231
890	→	518
1896	→	888
2390	→	589
619	→	599
540	→	1359
2174	→	1325
824	→	1
824	→	978
824	→	875
824	→	589
824	→	579
824	→	633
824	→	114
824	→	989
894	→	884
894	→	1687
2136	→	484
1310	→	748
1358	→	592
1084	→	187
597	→	239
839	→	1253
2071	→	1086
639	→	2181
6	→	63
6	→	163
6	→	230
6	→	349
6	→	422
6	→	782
1075	→	186
1075	→	1728
519	→	1181
519	→	1588
519	→	2179
116	→	1960
1539	→	935
1539	→	482
1539	→	919
1539	→	440
1539	→	9
1539	→	842
1539	→	6
1539	→	591
1539	→	570
1539	→	185
1539	→	685
1539	→	62
1539	→	998
468	→	441
1882	→	850
1456	→	935
1456	→	482
1456	→	919
1456	→	440
1456	→	9
1456	→	842
1456	→	782
1456	→	349
1456	→	163
1456	→	63
1456	→	230
1456	→	422
1456	→	6
1456	→	570
1456	→	185
1456	→	685
1456	→	62
1456	→	998
88	→	959
377	→	510
377	→	533
377	→	569
377	→	950
377	→	1426
2061	→	677
386	→	1
386	→	164
386	→	920
386	→	936
1292	→	535
2111	→	231
124	→	1010
1047	→	590
1047	→	510
1047	→	569
1047	→	1426
1047	→	950
1047	→	533
1047	→	377
1364	→	601
1377	→	733
1377	→	300
1377	→	624
1377	→	799
1377	→	351
1377	→	144
1377	→	40
1377	→	261
1377	→	402
1377	→	2
1377	→	580
1377	→	719
1377	→	327
2158	→	484
2134	→	1201
2010	→	1040
657	→	648
2274	→	85
350	→	300
350	→	1083
831	→	1085
831	→	1131
831	→	1765
1180	→	733
1180	→	300
1180	→	624
1180	→	799
1180	→	351
1180	→	144
1180	→	40
1180	→	261
1180	→	402
1180	→	2
1180	→	580
1180	→	719
1180	→	327
1180	→	2102
1180	→	85
1180	→	2103
2316	→	9
1500	→	1305
2262	→	748
717	→	1660
717	→	1740
717	→	1956
873	→	2201
301	→	825
999	→	2009
808	→	756
2	→	40
2	→	144
2	→	261
2	→	351
2	→	402
2	→	799
2144	→	484
11	→	1675
4	→	8
4	→	113
4	→	259
4	→	328
4	→	404
4	→	797
232	→	816
232	→	1399
1945	→	952
876	→	895
2258	→	748
1655	→	144
520	→	3
520	→	620
520	→	231
520	→	281
520	→	441
520	→	483
520	→	536
1538	→	2263
1538	→	2277
1538	→	2335
904	→	1469
580	→	624
580	→	1642
300	→	733
2085	→	231
281	→	231
281	→	1459
1015	→	998
1587	→	935
1587	→	482
1587	→	919
1587	→	440
1587	→	9
1587	→	842
1587	→	6
1587	→	591
1587	→	570
1587	→	185
1587	→	685
1587	→	62
1587	→	998
114	→	579
114	→	589
114	→	633
114	→	875
114	→	1293
16	→	1367
1470	→	1450
862	→	851
2254	→	719
2254	→	2349
421	→	377
1334	→	979
1343	→	710
1343	→	421
1343	→	834
1343	→	747
1343	→	299
1343	→	146
1343	→	61
1343	→	278
1343	→	420
1343	→	5
1343	→	667
1343	→	378
1773	→	2135
800	→	748
800	→	863
800	→	891
800	→	986
800	→	115
800	→	797
800	→	328
800	→	113
800	→	8
800	→	259
800	→	404
800	→	4
800	→	979
800	→	859
800	→	759
2093	→	231
1835	→	1827
581	→	903
581	→	1076
985	→	122
684	→	6
684	→	935
684	→	482
684	→	919
684	→	440
684	→	9
684	→	842
684	→	570
684	→	185
684	→	685
684	→	62
684	→	998
1743	→	300
2350	→	825
989	→	978
1458	→	1448
2101	→	1152
85	→	2102
759	→	748
759	→	859
759	→	1048
596	→	2187
1455	→	2078
1455	→	2157
1455	→	2293
1455	→	2309
1432	→	2243
1013	→	998
2352	→	2053
736	→	1699
1020	→	1039
2077	→	1086
2264	→	748
1006	→	2357
1006	→	2359
1006	→	2377
1006	→	2389
1006	→	2391
694	→	6
694	→	935
694	→	482
694	→	919
694	→	440
694	→	9
694	→	842
694	→	570
694	→	185
694	→	685
694	→	62
694	→	591
694	→	825
694	→	301
694	→	41
694	→	1015
694	→	1009
694	→	1994
621	→	599
757	→	1
757	→	145
757	→	625
757	→	895
757	→	166
757	→	876
757	→	1370
217	→	186
217	→	512
217	→	1834
2202	→	1325
934	→	920
113	→	1014
902	→	717
1038	→	9
1179	→	2112
1179	→	2120
1179	→	2171
1179	→	2249
64	→	9
2079	→	231
1735	→	300
1795	→	589
1795	→	1901
1259	→	484
709	→	686
709	→	1363
2186	→	1325
1657	→	1647
231	→	620
240	→	5
240	→	833
240	→	950
240	→	533
240	→	510
240	→	569
240	→	377
240	→	590
2270	→	85
707	→	686
707	→	1422
909	→	693
2194	→	1325
1774	→	2257
1774	→	2267
1774	→	2269
1774	→	2325
1025	→	2224
17	→	1118
17	→	1264
17	→	1794
17	→	1865
17	→	2076
683	→	1116
683	→	1266
683	→	1792
683	→	1873
2342	→	825
1537	→	2141
718	→	6
718	→	935
718	→	482
718	→	919
718	→	440
718	→	9
718	→	842
718	→	591
718	→	570
718	→	185
718	→	685
718	→	62
718	→	998
712	→	1895
164	→	114
926	→	908
1433	→	2114
1433	→	2193
1433	→	2253
1017	→	998
242	→	231
242	→	618
242	→	1461
2328	→	9
1874	→	850
832	→	756
2302	→	850
858	→	550
215	→	186
215	→	1826
492	→	94
492	→	1365
2109	→	85
2286	→	589
693	→	1160
693	→	1457
693	→	1530
2095	→	1152
928	→	920
1368	→	599
2225	→	8
866	→	851
1360	→	599
1434	→	988
1434	→	865
1434	→	748
1434	→	797
1434	→	328
1434	→	113
1434	→	8
1434	→	259
1434	→	404
1434	→	4
1434	→	850
1434	→	783
1434	→	1312
1434	→	1308
2000	→	9
2188	→	1325
378	→	667
378	→	710
378	→	1496
1959	→	9
649	→	3
649	→	620
649	→	231
649	→	281
649	→	618
649	→	242
649	→	441
649	→	990
649	→	826
649	→	483
649	→	1533
649	→	1545
649	→	1294
2219	→	2209
1165	→	300
1028	→	579
1028	→	633
1028	→	166
1028	→	895
1028	→	876
1741	→	300
1955	→	9
375	→	2
375	→	733
375	→	300
375	→	624
375	→	580
375	→	719
375	→	327
375	→	2102
375	→	85
375	→	2103
2272	→	85
541	→	1096
541	→	1268
541	→	1788
541	→	1875
1210	→	624
1210	→	580
807	→	1646
807	→	1664
807	→	1720
195	→	186
2294	→	589
2294	→	2315
1947	→	952
1306	→	374
2115	→	231
1775	→	895
1775	→	875
1775	→	589
1775	→	114
1775	→	758
1775	→	326
1775	→	165
1775	→	85
1775	→	241
1775	→	376
1775	→	1
1775	→	166
1775	→	876
1251	→	2070
1251	→	2092
1251	→	2151
1251	→	2287
1251	→	2303
2380	→	2210
144	→	1008
144	→	1993
1269	→	484
2296	→	850
1876	→	850
785	→	748
1951	→	9
1265	→	484
551	→	3
551	→	441
551	→	620
551	→	231
551	→	483
551	→	281
551	→	260
551	→	536
551	→	1400
605	→	2051
2180	→	1325
403	→	377
1423	→	652
632	→	2
632	→	733
632	→	300
632	→	624
632	→	580
632	→	719
632	→	327
632	→	2102
632	→	85
632	→	2103
1961	→	981
442	→	642
166	→	114
166	→	1270
166	→	758
166	→	326
166	→	165
166	→	85
166	→	241
166	→	376
166	→	1
163	→	1012
798	→	748
798	→	861
798	→	883
798	→	977
2378	→	484
439	→	377
1263	→	484
864	→	851
1468	→	1449
2326	→	9
1949	→	952
2164	→	1325
599	→	809
996	→	17
996	→	1361
2336	→	9
262	→	231
94	→	1114
94	→	1262
94	→	1790
94	→	1838
94	→	1867
2121	→	1201
849	→	587
1460	→	1449
327	→	300
327	→	719
327	→	1335
327	→	1369
327	→	1940
1941	→	952
2266	→	1665
1462	→	1449
857	→	1260
1115	→	231
307	→	93
0₁(1268)	→	1269
0₁(1692)	→	1693
0₁(721)	→	722
0₁(1264)	→	1265
0₁(2151)	→	2152
0₁(1766)	→	1767
0₁(576)	→	577
0₁(1642)	→	1643
0₁(891)	→	892
0₁(674)	→	675
0₁(692)	→	693
0₁(1375)	→	1376
0₁(883)	→	884
0₁(438)	→	439
0₁(749)	→	750
0₁(1580)	→	1581
0₁(10)	→	11
0₁(639)	→	640
0₁(1771)	→	1772
0₁(190)	→	191
0₁(687)	→	688
0₁(671)	→	672
0₁(1230)	→	1231
0₁(851)	→	852
0₁(1227)	→	1228
0₁(1173)	→	1174
0₁(1767)	→	1768
0₁(901)	→	902
0₁(889)	→	890
0₁(2143)	→	2144
0₁(2135)	→	2136
0₁(385)	→	386
0₁(847)	→	848
0₁(630)	→	631
0₁(443)	→	444
0₁(1340)	→	1341
0₁(1964)	→	1965
0₁(1461)	→	1462
0₁(1430)	→	1431
0₁(822)	→	823
0₁(2157)	→	2158
0₁(422)	→	423
0₁(650)	→	651
0₁(2149)	→	2150
0₁(990)	→	991
0₁(585)	→	586
0₁(404)	→	405
0₁(1724)	→	1725
0₁(980)	→	981
0₁(708)	→	709
0₁(376)	→	377
0₁(596)	→	597
0₁(837)	→	838
0₁(1459)	→	1460
0₁(1448)	→	1449
0₁(120)	→	121
0₁(544)	→	545
0₁(1965)	→	1966
0₁(1258)	→	1259
0₁(1300)	→	1301
0₁(1496)	→	1497
0₁(1253)	→	1254
0₁(93)	→	94
0₁(1266)	→	1267
0₁(1262)	→	1263
0₁(1373)	→	1374
0₁(810)	→	811
0₁(1648)	→	1649
0₁(589)	→	590
0₁(636)	→	637
0₁(672)	→	673
0₁(1337)	→	1338
0₁(713)	→	714
0₁(816)	→	817
0₁(853)	→	854
0₁(922)	→	923
0₁(1053)	→	1054
0₁(991)	→	992
0₁(519)	→	520
0₁(1467)	→	1468
0₁(833)	→	834
0₁(903)	→	904
0₁(1433)	→	1434
0₁(686)	→	687
0₁(402)	→	403
0₁(1246)	→	1247
0₁(1260)	→	1261
0₁(1830)	→	1831
0₁(868)	→	869
0₁(695)	→	696
0₁(420)	→	421
0₁(2377)	→	2378
0₁(89)	→	90
0₁(827)	→	828
0₁(736)	→	737
0₁(1428)	→	1429
0₁(893)	→	894
0₁(961)	→	962
0₁(884)	→	885
0₁(1534)	→	1535
0₁(377)	→	378
0₁(873)	→	874
0₁(374)	→	375
0₁(628)	→	629
0₁(1357)	→	1358
0₁(514)	→	515
0₁(676)	→	677
0₁(382)	→	383
0₁(599)	→	600
0₁(442)	→	443
0₁(2141)	→	2142
0₁(368)	→	369
0₁(706)	→	707
0₁(669)	→	670
0₁(899)	→	900
0₁(1179)	→	1180
0₁(685)	→	686
0₁(653)	→	654
0₁(1960)	→	1961
0₁(582)	→	583
0₁(655)	→	656
0₁(591)	→	592
0₁(1431)	→	1432
0₁(956)	→	957
0₁(486)	→	487
0₁(1530)	→	1531
0₂(1045)	→	1046
0₂(1203)	→	1204
0₂(2185)	→	2186
0₂(1332)	→	1333
0₂(2025)	→	2026
0₂(999)	→	1000
0₂(2193)	→	2194
0₂(2181)	→	2182
0₂(2179)	→	2180
0₂(1020)	→	1021
0₂(1666)	→	1667
0₂(2173)	→	2174
0₂(2171)	→	2172
0₂(1209)	→	1210
0₂(2163)	→	2164
0₂(2210)	→	2211
0₂(2036)	→	2037
0₂(2195)	→	2196
0₂(1324)	→	1325
0₂(2187)	→	2188
0₂(2201)	→	2202
0₂(1041)	→	1042
0₂(2057)	→	2058
0₂(2165)	→	2166
4₂(2216)	→	2217
4₂(1157)	→	1158
4₂(1154)	→	1155
4₂(997)	→	998
4₂(1672)	→	1673
4₂(1014)	→	1015
4₂(2030)	→	2031
4₂(2019)	→	2020
4₂(1018)	→	1019
4₂(1208)	→	1209
4₂(1325)	→	1326
4₂(1008)	→	1009
4₂(1010)	→	1011
4₂(1152)	→	1153
4₂(2209)	→	2210
4₂(1012)	→	1013
4₂(1158)	→	1159
4₂(2379)	→	2380
4₂(1207)	→	1208
4₂(1153)	→	1154
4₂(998)	→	999
4₂(1090)	→	1091
4₂(2051)	→	2052
4₂(1019)	→	1020
4₂(1016)	→	1017
5₂(1669)	→	1670
5₂(1671)	→	1672
5₂(1329)	→	1330
5₂(1673)	→	1674
5₂(1156)	→	1157
5₁(754)	→	755
5₁(1794)	→	1795
5₁(165)	→	166
5₁(919)	→	920
5₁(677)	→	678
5₁(1653)	→	1654
5₁(867)	→	868
5₁(113)	→	114
5₁(163)	→	164
5₁(2279)	→	2280
5₁(533)	→	534
5₁(988)	→	989
5₁(820)	→	821
5₁(1792)	→	1793
5₁(927)	→	928
5₁(1765)	→	1766
5₁(2389)	→	2390
5₁(812)	→	813
5₁(2287)	→	2288
5₁(752)	→	753
5₁(756)	→	757
5₁(1303)	→	1304
5₁(805)	→	806
5₁(378)	→	379
5₁(1651)	→	1652
5₁(1826)	→	1827
5₁(2285)	→	2286
5₁(1449)	→	1450
5₁(124)	→	125
5₁(1371)	→	1372
5₁(144)	→	145
5₁(1369)	→	1370
5₁(1687)	→	1688
5₁(1790)	→	1791
5₁(2293)	→	2294
5₁(935)	→	936
5₁(146)	→	147
5₁(304)	→	305
5₁(1581)	→	1582
5₁(543)	→	544
5₁(977)	→	978
5₁(1834)	→	1835
5₁(843)	→	844
5₁(573)	→	574
5₁(1690)	→	1691
5₁(986)	→	987
5₁(817)	→	818
5₁(875)	→	876
5₁(626)	→	627
5₁(516)	→	517
5₁(1788)	→	1789
5₁(722)	→	723
5₁(1469)	→	1470
5₁(624)	→	625
5₁(933)	→	934
0₀(3)	→	5
0₀(6)	→	5
0₀(5)	→	5
0₀(4)	→	5
0₀(2)	→	5
0₀(1)	→	5
4₀(2)	→	6
4₀(6)	→	6
4₀(4)	→	6
4₀(1)	→	6
4₀(3)	→	6
4₀(5)	→	6
3₂(1205)	→	1206
3₂(1021)	→	1022
3₂(1330)	→	1331
3₂(1092)	→	1093
3₂(2058)	→	2059
3₂(1326)	→	1327
3₂(1331)	→	1332
3₂(2026)	→	2027
3₂(1043)	→	1044
3₂(1086)	→	1087
3₂(2037)	→	2038
3₂(1002)	→	1003
3₂(1023)	→	1024
3₂(2215)	→	2216
3₂(1201)	→	1202
3₂(1024)	→	1025
3₂(1665)	→	1666
3₂(1202)	→	1203
3₂(1000)	→	1001
3₂(1204)	→	1205
3₂(1087)	→	1088
3₂(1003)	→	1004
3₂(2267)	→	2268
3₂(2265)	→	2266
3₂(1333)	→	1334
3₂(1327)	→	1328
3₂(1042)	→	1043
3₂(1664)	→	1665
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
1₁(2102)	→	2103
1₁(690)	→	691
1₁(2277)	→	2278
1₁(1578)	→	1579
1₁(299)	→	300
1₁(17)	→	18
1₁(846)	→	847
1₁(1497)	→	1498
1₁(753)	→	754
1₁(1499)	→	1500
1₁(1577)	→	1578
1₁(547)	→	548
1₁(2104)	→	2105
1₁(643)	→	644
1₁(490)	→	491
1₁(1251)	→	1252
1₁(1164)	→	1165
1₁(192)	→	193
1₁(1742)	→	1743
1₁(88)	→	89
1₁(349)	→	350
1₁(1099)	→	1100
1₁(716)	→	717
1₁(850)	→	851
1₁(689)	→	690
1₁(94)	→	95
1₁(859)	→	860
1₁(741)	→	742
1₁(1162)	→	1163
1₁(857)	→	858
1₁(733)	→	734
1₁(896)	→	897
1₁(351)	→	352
1₁(586)	→	587
1₁(865)	→	866
1₁(2253)	→	2254
1₁(536)	→	537
1₁(2271)	→	2272
1₁(1829)	→	1830
1₁(738)	→	739
1₁(603)	→	604
1₁(1072)	→	1073
1₁(1652)	→	1653
1₁(234)	→	235
1₁(839)	→	840
1₁(625)	→	626
1₁(92)	→	93
1₁(731)	→	732
1₁(1455)	→	1456
1₁(688)	→	689
1₁(953)	→	954
1₁(2108)	→	2109
1₁(803)	→	804
1₁(1740)	→	1741
1₁(116)	→	117
1₁(1650)	→	1651
1₁(1768)	→	1769
1₁(194)	→	195
1₁(601)	→	602
1₁(2269)	→	2270
1₁(735)	→	736
1₁(729)	→	730
1₁(1590)	→	1591
1₁(16)	→	17
1₁(541)	→	542
1₁(518)	→	519
1₁(189)	→	190
1₁(1160)	→	1161
1₁(1276)	→	1277
1₁(308)	→	309
1₁(869)	→	870
1₁(954)	→	955
1₁(1537)	→	1538
1₁(592)	→	593
1₁(216)	→	217
1₁(878)	→	879
1₁(1134)	→	1135
1₁(1970)	→	1971
1₁(737)	→	738
1₁(579)	→	580
1₁(1341)	→	1342
1₁(185)	→	186
1₁(2249)	→	2250
1₁(1400)	→	1401
1₁(863)	→	864
1₁(326)	→	327
1₁(1592)	→	1593
1₁(593)	→	594
1₁(1588)	→	1589
1₁(842)	→	843
1₁(517)	→	518
1₁(1498)	→	1499
1₁(962)	→	963
1₁(214)	→	215
1₁(1773)	→	1774
1₁(1734)	→	1735
1₁(1049)	→	1050
1₁(328)	→	329
1₁(2251)	→	2252
1₁(1100)	→	1101
1₁(233)	→	234
1₁(861)	→	862
1₁(950)	→	951
1₁(725)	→	726
1₁(2106)	→	2107
1₁(485)	→	486
1₁(751)	→	752
1₁(1272)	→	1273
1₁(1370)	→	1371
1₁(818)	→	819
1₁(1074)	→	1075
1₁(1688)	→	1689
1₁(719)	→	720
1₁(834)	→	835
1₁(1277)	→	1278
1₁(831)	→	832
1₁(2273)	→	2274
1₁(1720)	→	1721
1₁(1135)	→	1136
1₁(955)	→	956
1₁(540)	→	541
1₁(683)	→	684
1₁(1584)	→	1585
1₁(801)	→	802
2₁(488)	→	489
2₁(303)	→	304
2₁(807)	→	808
2₁(960)	→	961
2₁(995)	→	996
2₁(572)	→	573
2₁(1583)	→	1584
2₁(602)	→	603
2₁(1083)	→	1084
2₁(646)	→	647
2₁(838)	→	839
2₁(539)	→	540
2₁(1096)	→	1097
2₁(1114)	→	1115
2₁(1968)	→	1969
2₁(2110)	→	2111
2₁(236)	→	237
2₁(750)	→	751
2₁(261)	→	262
2₁(1293)	→	1294
2₁(87)	→	88
2₁(484)	→	485
2₁(1649)	→	1650
2₁(1401)	→	1402
2₁(467)	→	468
2₁(717)	→	718
2₁(1585)	→	1586
2₁(230)	→	231
2₁(982)	→	983
2₁(880)	→	881
2₁(1397)	→	1398
2₁(1302)	→	1303
2₁(2114)	→	2115
2₁(1104)	→	1105
2₁(12)	→	13
2₁(1969)	→	1970
2₁(2359)	→	2360
2₁(278)	→	279
2₁(994)	→	995
2₁(1105)	→	1106
2₁(550)	→	551
2₁(534)	→	535
2₁(906)	→	907
2₁(510)	→	511
2₁(188)	→	189
2₁(1271)	→	1272
2₁(594)	→	595
2₁(1140)	→	1141
2₁(491)	→	492
2₁(644)	→	645
2₁(2092)	→	2093
2₁(238)	→	239
2₁(1457)	→	1458
2₁(465)	→	466
2₁(1895)	→	1896
2₁(1722)	→	1723
2₁(595)	→	596
2₁(2112)	→	2113
2₁(446)	→	447
2₁(2243)	→	2244
2₁(879)	→	880
2₁(840)	→	841
2₁(1118)	→	1119
2₁(580)	→	581
2₁(489)	→	490
2₁(1291)	→	1292
2₁(1335)	→	1336
2₁(634)	→	635
2₁(1139)	→	1140
2₁(186)	→	187
2₁(280)	→	281
2₁(1403)	→	1404
2₁(1963)	→	1964
2₁(642)	→	643
2₁(1279)	→	1280
2₁(724)	→	725
2₁(241)	→	242
2₁(640)	→	641
2₁(1538)	→	1539
2₁(1447)	→	1448
2₁(239)	→	240
2₁(887)	→	888
2₁(852)	→	853
2₁(656)	→	657
2₁(711)	→	712
2₁(710)	→	711
2₁(1181)	→	1182
2₁(1249)	→	1250
2₁(637)	→	638
2₁(952)	→	953
2₁(2084)	→	2085
2₁(2224)	→	2225
2₁(855)	→	856
2₁(1452)	→	1453
2₁(726)	→	727
2₁(1772)	→	1773
2₁(2086)	→	2087
2₁(886)	→	887
2₁(806)	→	807
2₁(904)	→	905
2₁(1198)	→	1199
2₁(1399)	→	1400
2₁(535)	→	536
2₁(1363)	→	1364
2₁(371)	→	372
2₁(1116)	→	1117
2₁(1275)	→	1276
2₁(1076)	→	1077
2₁(1137)	→	1138
2₁(600)	→	601
2₁(825)	→	826
2₁(1531)	→	1532
2₁(259)	→	260
2₁(2078)	→	2079
2₁(1176)	→	1177
2₁(1544)	→	1545
2₁(856)	→	857
2₁(1270)	→	1271
2₁(1196)	→	1197
2₁(1170)	→	1171
2₁(652)	→	653
2₁(963)	→	964
2₁(900)	→	901
2₁(1131)	→	1132
2₁(1102)	→	1103
2₁(2385)	→	2386
2₁(482)	→	483
2₁(187)	→	188
2₁(15)	→	16
2₁(1532)	→	1533
2₁(680)	→	681
2₁(1194)	→	1195
2₁(440)	→	441
2₁(885)	→	886
2₁(1774)	→	1775
1₀(3)	→	2
1₀(5)	→	2
1₀(2)	→	2
1₀(4)	→	2
1₀(1)	→	2
1₀(6)	→	2
2₀(2)	→	3
2₀(4)	→	3
2₀(3)	→	3
2₀(6)	→	3
2₀(1)	→	3
2₀(5)	→	3
4₁(627)	→	628
4₁(1699)	→	1700
4₁(590)	→	591
4₁(821)	→	822
4₁(302)	→	303
4₁(300)	→	301
4₁(40)	→	41
4₁(538)	→	539
4₁(814)	→	815
4₁(1958)	→	1959
4₁(1048)	→	1049
4₁(9)	→	10
4₁(1229)	→	1230
4₁(1359)	→	1360
4₁(1899)	→	1900
4₁(720)	→	721
4₁(854)	→	855
4₁(618)	→	619
4₁(1675)	→	1676
4₁(829)	→	830
4₁(117)	→	118
4₁(1454)	→	1455
4₁(1274)	→	1275
4₁(373)	→	374
4₁(63)	→	64
4₁(2327)	→	2328
4₁(979)	→	980
4₁(305)	→	306
4₁(384)	→	385
4₁(372)	→	373
4₁(964)	→	965
4₁(1827)	→	1828
4₁(306)	→	307
4₁(828)	→	829
4₁(809)	→	810
4₁(235)	→	236
4₁(1055)	→	1056
4₁(1226)	→	1227
4₁(1901)	→	1902
4₁(1726)	→	1727
4₁(85)	→	86
4₁(1051)	→	1052
4₁(1037)	→	1038
4₁(1050)	→	1051
4₁(38)	→	39
4₁(920)	→	921
4₁(811)	→	812
4₁(8)	→	9
4₁(1298)	→	1299
4₁(549)	→	550
4₁(923)	→	924
4₁(1451)	→	1452
4₁(2333)	→	2334
4₁(898)	→	899
4₁(537)	→	538
4₁(1952)	→	1953
4₁(682)	→	683
4₁(1721)	→	1722
4₁(1533)	→	1534
4₁(1177)	→	1178
4₁(654)	→	655
4₁(1372)	→	1373
4₁(813)	→	814
4₁(1838)	→	1839
4₁(1432)	→	1433
4₁(921)	→	922
4₁(620)	→	621
4₁(1297)	→	1298
4₁(844)	→	845
4₁(1999)	→	2000
4₁(1579)	→	1580
4₁(1954)	→	1955
4₁(908)	→	909
4₁(907)	→	908
4₁(605)	→	606
4₁(983)	→	984
4₁(819)	→	820
4₁(673)	→	674
4₁(115)	→	116
4₁(2335)	→	2336
4₁(545)	→	546
4₁(1993)	→	1994
4₁(2341)	→	2342
4₁(2343)	→	2344
4₁(2349)	→	2350
4₁(122)	→	123
4₁(1956)	→	1957
4₁(569)	→	570
4₁(802)	→	803
4₁(2203)	→	2204
4₁(2325)	→	2326
4₁(61)	→	62
4₁(633)	→	634
4₁(2315)	→	2316
4₁(1950)	→	1951
4₁(888)	→	889
4₁(598)	→	599
4₁(1101)	→	1102
4₁(1654)	→	1655
4₁(1367)	→	1368
4₁(877)	→	878
4₁(1725)	→	1726
4₁(1689)	→	1690
4₁(381)	→	382
4₁(1728)	→	1729
4₁(1178)	→	1179
4₁(679)	→	680
4₁(1962)	→	1963
4₁(755)	→	756
4₁(712)	→	713
4₁(1136)	→	1137
4₁(905)	→	906
4₁(1691)	→	1692
4₁(984)	→	985
4₁(693)	→	694
4₁(739)	→	740
4₁(897)	→	898
4₁(301)	→	302
4₁(876)	→	877
4₁(546)	→	547
4₁(1361)	→	1362
4₁(118)	→	119
4₁(1365)	→	1366
4₁(1273)	→	1274
3₁(645)	→	646
3₁(992)	→	993
3₁(1769)	→	1770
3₁(848)	→	849
3₁(383)	→	384
3₁(441)	→	442
3₁(1311)	→	1312
3₁(570)	→	571
3₁(1948)	→	1949
3₁(232)	→	233
3₁(925)	→	926
3₁(2259)	→	2260
3₁(581)	→	582
3₁(667)	→	668
3₁(11)	→	12
3₁(1656)	→	1657
3₁(2309)	→	2310
3₁(723)	→	724
3₁(1338)	→	1339
3₁(1429)	→	1430
3₁(1248)	→	1249
3₁(512)	→	513
3₁(1586)	→	1587
3₁(1405)	→	1406
3₁(1940)	→	1941
3₁(2301)	→	2302
3₁(1867)	→	1868
3₁(583)	→	584
3₁(1770)	→	1771
3₁(2261)	→	2262
3₁(835)	→	836
3₁(1404)	→	1405
3₁(1831)	→	1832
3₁(1946)	→	1947
3₁(1171)	→	1172
3₁(574)	→	575
3₁(237)	→	238
3₁(1304)	→	1305
3₁(2303)	→	2304
3₁(1175)	→	1176
3₁(1133)	→	1134
3₁(647)	→	648
3₁(1307)	→	1308
3₁(1247)	→	1248
3₁(830)	→	831
3₁(191)	→	192
3₁(1865)	→	1866
3₁(670)	→	671
3₁(1402)	→	1403
3₁(444)	→	445
3₁(638)	→	639
3₁(845)	→	846
3₁(1103)	→	1104
3₁(1374)	→	1375
3₁(748)	→	749
3₁(2257)	→	2258
3₁(1336)	→	1337
3₁(836)	→	837
3₁(1832)	→	1833
3₁(1647)	→	1648
3₁(1536)	→	1537
3₁(13)	→	14
3₁(1828)	→	1829
3₁(1453)	→	1454
3₁(1174)	→	1175
3₁(629)	→	630
3₁(872)	→	873
3₁(575)	→	576
3₁(691)	→	692
3₁(895)	→	896
3₁(871)	→	872
3₁(1225)	→	1226
3₁(924)	→	925
3₁(1172)	→	1173
3₁(1342)	→	1343
3₁(668)	→	669
3₁(604)	→	605
3₁(799)	→	800
3₁(14)	→	15
3₁(1450)	→	1451
3₁(1097)	→	1098
3₁(870)	→	871
3₁(1339)	→	1340
3₁(90)	→	91
3₁(678)	→	679
3₁(1309)	→	1310
3₁(121)	→	122
3₁(635)	→	636
3₁(804)	→	805
3₁(114)	→	115
3₁(1427)	→	1428
3₁(1054)	→	1055
3₁(747)	→	748
3₁(91)	→	92
3₁(1138)	→	1139
3₁(959)	→	960
3₁(1224)	→	1225
3₁(513)	→	514
3₁(380)	→	381
3₁(587)	→	588
3₁(1723)	→	1724
3₁(447)	→	448
3₁(648)	→	649
3₁(1873)	→	1874
3₁(714)	→	715
3₁(1966)	→	1967
3₁(631)	→	632
3₁(515)	→	516
3₁(1693)	→	1694
3₁(1582)	→	1583
3₁(715)	→	716
3₁(957)	→	958
3₁(1944)	→	1945
3₁(1052)	→	1053
3₁(1967)	→	1968
3₁(993)	→	994
3₁(681)	→	682
3₁(784)	→	785
3₁(548)	→	549
3₁(978)	→	979
3₁(651)	→	652
3₁(571)	→	572
3₁(758)	→	759
3₁(797)	→	798
3₁(1098)	→	1099
3₁(2391)	→	2392
3₁(1660)	→	1661
3₁(1422)	→	1423
3₁(826)	→	827
3₁(951)	→	952
3₁(577)	→	578
3₁(445)	→	446
3₁(823)	→	824
3₁(1662)	→	1663
3₁(379)	→	380
3₁(1376)	→	1377
3₁(369)	→	370
3₁(881)	→	882
3₁(740)	→	741
3₁(1881)	→	1882
3₁(727)	→	728
3₁(1426)	→	1427
3₁(1897)	→	1898
3₁(1535)	→	1536
3₁(584)	→	585
3₁(2263)	→	2264
3₁(782)	→	783
3₁(487)	→	488
3₁(1132)	→	1133
3₁(370)	→	371
3₁(981)	→	982
3₁(231)	→	232
3₁(1250)	→	1251
3₁(1658)	→	1659
3₁(119)	→	120
3₁(1646)	→	1647
3₁(1305)	→	1306
3₁(1875)	→	1876
3₁(2295)	→	2296
3₁(1228)	→	1229
2₂(1085)	→	1086
2₂(1022)	→	1023
2₂(2218)	→	2219
2₂(2076)	→	2077
2₂(2023)	→	2024
2₂(2022)	→	2023
2₂(2133)	→	2134
2₂(2213)	→	2214
2₂(1004)	→	1005
2₂(2053)	→	2054
2₂(1039)	→	1040
2₂(2068)	→	2069
2₂(2021)	→	2022
2₂(1328)	→	1329
2₂(2054)	→	2055
2₂(2120)	→	2121
2₂(2357)	→	2358
2₂(2070)	→	2071
2₂(2211)	→	2212
2₂(2116)	→	2117
2₂(1091)	→	1092
2₂(1001)	→	1002
2₂(1025)	→	1026
2₂(2118)	→	2119
2₂(1667)	→	1668
2₂(1094)	→	1095
2₂(2062)	→	2063
2₂(2034)	→	2035
2₂(2055)	→	2056
2₂(2033)	→	2034
2₂(1093)	→	1094
2₂(2009)	→	2010
2₂(1200)	→	1201
2₂(1206)	→	1207
2₂(1155)	→	1156
2₂(2032)	→	2033
5₀(1)	→	1
5₀(6)	→	1
5₀(5)	→	1
5₀(2)	→	1
5₀(3)	→	1
5₀(4)	→	1
1₂(1151)	→	1152
1₂(2214)	→	2215
1₂(2024)	→	2025
1₂(2035)	→	2036
1₂(1005)	→	1006
1₂(2027)	→	2028
1₂(2052)	→	2053
1₂(1670)	→	1671
1₂(2020)	→	2021
1₂(1006)	→	1007
1₂(2060)	→	2061
1₂(1089)	→	1090
1₂(2094)	→	2095
1₂(1026)	→	1027
1₂(1668)	→	1669
1₂(1044)	→	1045
1₂(2100)	→	2101
1₂(1046)	→	1047
1₂(2059)	→	2060
1₂(2351)	→	2352
1₂(2039)	→	2040
1₂(2031)	→	2032
1₂(2212)	→	2213
1₂(1040)	→	1041
1₂(1027)	→	1028
1₂(2056)	→	2057
1₂(2038)	→	2039
1₂(2028)	→	2029
1₂(1088)	→	1089
1₂(2098)	→	2099

The automaton is closed under rewriting as it is compatible.