Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4314)

The rewrite relation of the following TRS is considered.

0(1(1(2(x1))))	→	3(3(0(3(3(2(2(0(0(0(x1))))))))))	(1)
5(4(4(0(x1))))	→	2(3(1(0(0(3(3(3(4(0(x1))))))))))	(2)
0(0(5(0(5(x1)))))	→	2(5(2(2(3(3(3(5(1(0(x1))))))))))	(3)
0(4(1(5(5(x1)))))	→	2(1(3(5(2(2(3(3(2(5(x1))))))))))	(4)
5(0(5(5(0(x1)))))	→	3(4(0(3(0(4(0(3(3(5(x1))))))))))	(5)
5(0(5(5(5(x1)))))	→	5(1(3(0(3(3(1(3(1(2(x1))))))))))	(6)
5(5(2(1(0(x1)))))	→	3(3(1(3(3(0(4(5(1(2(x1))))))))))	(7)
0(1(0(5(5(2(x1))))))	→	0(2(3(2(4(0(1(3(2(0(x1))))))))))	(8)
0(2(1(5(5(2(x1))))))	→	0(3(4(2(1(2(0(1(2(3(x1))))))))))	(9)
0(4(0(5(3(1(x1))))))	→	3(2(3(2(2(3(4(0(1(1(x1))))))))))	(10)
0(4(0(5(3(4(x1))))))	→	0(0(0(0(3(0(4(4(5(1(x1))))))))))	(11)
0(4(4(4(5(4(x1))))))	→	3(2(0(2(1(3(0(4(5(4(x1))))))))))	(12)
0(5(4(5(5(5(x1))))))	→	3(3(4(3(1(4(4(3(3(5(x1))))))))))	(13)
1(1(1(5(3(4(x1))))))	→	1(5(1(3(3(3(2(0(4(4(x1))))))))))	(14)
1(1(4(1(5(5(x1))))))	→	4(2(3(0(4(4(1(0(0(4(x1))))))))))	(15)
2(1(1(1(4(5(x1))))))	→	2(0(4(2(0(3(3(2(1(5(x1))))))))))	(16)
3(1(1(1(5(4(x1))))))	→	3(3(5(4(1(5(1(3(5(4(x1))))))))))	(17)
4(4(0(5(5(2(x1))))))	→	0(1(2(2(0(2(0(1(4(2(x1))))))))))	(18)
4(4(1(1(5(0(x1))))))	→	4(0(3(2(2(1(1(0(4(0(x1))))))))))	(19)
4(4(4(0(5(0(x1))))))	→	3(4(0(0(1(3(4(2(3(2(x1))))))))))	(20)
5(0(5(5(3(1(x1))))))	→	5(0(5(1(3(0(0(3(0(1(x1))))))))))	(21)
5(5(1(1(0(3(x1))))))	→	3(3(0(2(5(1(3(3(2(3(x1))))))))))	(22)
0(2(2(5(4(5(2(x1)))))))	→	3(2(2(3(5(2(0(3(2(2(x1))))))))))	(23)
0(4(5(2(1(5(0(x1)))))))	→	0(2(3(2(0(1(5(4(1(2(x1))))))))))	(24)
0(5(0(5(5(0(0(x1)))))))	→	0(2(4(0(3(0(3(5(4(0(x1))))))))))	(25)
0(5(4(3(5(2(4(x1)))))))	→	0(3(1(3(0(0(4(3(2(4(x1))))))))))	(26)
0(5(5(5(1(5(5(x1)))))))	→	0(1(0(1(3(5(1(3(2(5(x1))))))))))	(27)
1(0(0(5(0(1(3(x1)))))))	→	1(2(0(3(3(4(0(2(1(3(x1))))))))))	(28)
1(5(5(5(2(2(0(x1)))))))	→	3(0(4(2(0(2(1(0(3(2(x1))))))))))	(29)
2(1(0(4(5(5(2(x1)))))))	→	4(3(3(2(1(2(4(1(2(3(x1))))))))))	(30)
2(1(1(5(5(5(0(x1)))))))	→	3(3(4(5(3(2(1(4(3(0(x1))))))))))	(31)
2(1(5(3(4(4(0(x1)))))))	→	4(3(2(3(0(1(3(4(3(0(x1))))))))))	(32)
2(1(5(5(3(4(4(x1)))))))	→	3(3(1(3(3(1(5(5(4(4(x1))))))))))	(33)
4(1(1(3(1(0(2(x1)))))))	→	4(2(3(5(2(2(0(0(0(0(x1))))))))))	(34)
4(1(5(0(5(1(4(x1)))))))	→	0(1(0(1(1(0(0(0(0(1(x1))))))))))	(35)
4(4(4(1(1(5(3(x1)))))))	→	4(4(2(5(3(3(4(3(3(2(x1))))))))))	(36)
4(4(4(5(5(5(0(x1)))))))	→	0(4(0(4(1(3(0(4(3(2(x1))))))))))	(37)
4(5(5(1(1(3(4(x1)))))))	→	0(2(3(2(0(4(4(5(2(4(x1))))))))))	(38)
5(2(0(5(4(0(5(x1)))))))	→	3(3(0(4(3(1(5(2(3(2(x1))))))))))	(39)
5(2(4(5(3(4(4(x1)))))))	→	2(0(5(2(3(3(5(1(3(4(x1))))))))))	(40)
5(3(1(5(4(4(0(x1)))))))	→	1(0(3(2(1(3(1(0(4(0(x1))))))))))	(41)
5(4(4(0(4(5(0(x1)))))))	→	2(3(5(2(2(5(0(4(3(0(x1))))))))))	(42)
5(5(2(2(1(1(5(x1)))))))	→	3(3(4(2(3(1(1(3(2(4(x1))))))))))	(43)
5(5(2(5(1(4(0(x1)))))))	→	4(3(1(3(2(0(0(4(3(2(x1))))))))))	(44)
5(5(5(0(0(1(3(x1)))))))	→	5(4(1(2(3(0(0(1(1(3(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	→	1934
1374	→	780
854	→	665
1197	→	535
1197	→	1515
588	→	566
588	→	611
871	→	665
1268	→	1259
221	→	1795
221	→	1801
221	→	1860
534	→	475
534	→	546
1231	→	510
917	→	1151
1859	→	414
1191	→	535
1191	→	1521
1496	→	832
750	→	742
1845	→	535
271	→	5
271	→	627
271	→	323
271	→	193
271	→	304
271	→	242
271	→	287
271	→	261
1551	→	667
1551	→	1566
967	→	1928
1156	→	326
715	→	855
715	→	822
715	→	190
715	→	820
715	→	118
715	→	1
715	→	9
715	→	170
715	→	88
715	→	1045
715	→	142
715	→	1796
715	→	1776
1109	→	10
98	→	5
98	→	306
98	→	627
98	→	637
98	→	831
98	→	567
98	→	244
98	→	261
98	→	881
1624	→	763
874	→	932
1935	→	667
97	→	969
97	→	1023
97	→	1182
1557	→	873
1248	→	511
1199	→	535
1733	→	9
1237	→	414
886	→	1501
933	→	1371
608	→	1623
326	→	656
326	→	712
326	→	749
371	→	326
371	→	646
371	→	708
371	→	741
371	→	1562
1593	→	1586
655	→	6
655	→	904
655	→	625
655	→	566
655	→	830
655	→	602
655	→	592
655	→	621
655	→	594
655	→	1155
655	→	1055
655	→	414
655	→	1220
655	→	1861
543	→	414
543	→	1367
352	→	326
352	→	698
352	→	1560
956	→	1877
956	→	1924
511	→	475
511	→	2
511	→	476
119	→	90
1923	→	667
668	→	791
668	→	864
668	→	872
610	→	2
610	→	511
610	→	548
610	→	191
610	→	497
638	→	1369
1851	→	535
676	→	6
676	→	904
676	→	625
676	→	566
676	→	830
676	→	602
676	→	592
1589	→	1885
1953	→	1052
18	→	1
18	→	715
18	→	88
18	→	477
18	→	626
18	→	659
18	→	43
18	→	603
18	→	818
18	→	116
18	→	64
18	→	1045
18	→	142
18	→	1796
18	→	1776
18	→	1772
547	→	536
624	→	612
1230	→	1958
1098	→	1087
41	→	9
41	→	142
3	→	63
3	→	260
3	→	387
3	→	455
3	→	533
3	→	574
1362	→	737
1411	→	1389
499	→	475
499	→	550
600	→	16
553	→	536
1565	→	881
817	→	3
817	→	749
817	→	656
817	→	326
817	→	698
817	→	352
817	→	629
817	→	780
817	→	1374
817	→	1808
817	→	1802
626	→	612
626	→	1217
626	→	1232
740	→	395
1325	→	660
861	→	653
919	→	5
919	→	627
919	→	262
919	→	193
919	→	224
1340	→	1556
9	→	140
9	→	190
9	→	406
9	→	822
1714	→	948
1931	→	667
620	→	2
620	→	511
5	→	8
5	→	241
5	→	370
5	→	416
5	→	512
5	→	565
931	→	395
1778	→	1045
1778	→	1954
592	→	566
1524	→	855
1567	→	881
1071	→	1056
1071	→	1946
456	→	417
483	→	17
1183	→	417
1183	→	589
1183	→	457
1183	→	223
1183	→	65
1183	→	353
1183	→	498
1183	→	4
1183	→	787
1183	→	473
765	→	926
1139	→	1568
1639	→	764
1220	→	414
1095	→	1701
1095	→	1719
1095	→	1820
1929	→	667
1806	→	326
674	→	1204
622	→	612
622	→	1225
90	→	658
90	→	756
892	→	739
193	→	323
193	→	627
1965	→	476
673	→	1738
473	→	417
473	→	787
224	→	193
224	→	262
713	→	668
713	→	1960
1800	→	262
1164	→	1912
938	→	5
938	→	627
938	→	304
938	→	193
938	→	242
1132	→	1852
1132	→	1936
968	→	715
968	→	88
968	→	587
968	→	439
968	→	192
968	→	40
968	→	325
968	→	496
968	→	1
968	→	1695
968	→	477
968	→	1045
968	→	142
968	→	1796
968	→	1776
1	→	40
1	→	192
1	→	325
1	→	439
1	→	496
1	→	587
1443	→	1621
786	→	609
1776	→	1045
1591	→	261
1591	→	565
1591	→	416
1591	→	241
1591	→	8
1591	→	370
1591	→	512
1591	→	5
1591	→	881
1040	→	1707
1040	→	1721
1040	→	1822
1957	→	1946
654	→	1070
654	→	1136
654	→	1153
1884	→	413
1884	→	1964
305	→	263
305	→	1263
1545	→	667
549	→	536
1837	→	535
1837	→	1920
645	→	4
645	→	789
645	→	417
645	→	787
645	→	473
755	→	411
222	→	193
222	→	289
222	→	5
1154	→	326
770	→	424
1185	→	417
777	→	414
477	→	1695
1323	→	424
334	→	1097
334	→	1138
334	→	1238
1823	→	417
1722	→	9
1130	→	1989
590	→	566
590	→	623
1345	→	1991
1283	→	904
1283	→	625
1283	→	566
1283	→	830
1283	→	591
1283	→	441
1283	→	243
1283	→	42
1283	→	372
1283	→	474
1283	→	6
1283	→	602
1283	→	592
970	→	959
1522	→	855
748	→	482
1366	→	751
634	→	1410
261	→	193
261	→	287
261	→	1223
573	→	482
1772	→	1045
1137	→	1124
1398	→	513
1398	→	593
1398	→	472
1398	→	221
1398	→	87
1398	→	351
1398	→	510
1398	→	2
1398	→	628
816	→	1554
675	→	1236
675	→	1552
269	→	1198
1348	→	904
1348	→	625
1348	→	566
1348	→	830
1348	→	591
1348	→	441
1348	→	243
1348	→	42
1348	→	372
1348	→	474
1348	→	6
1348	→	602
1348	→	592
91	→	1186
1370	→	759
1622	→	921
1553	→	667
1553	→	1558
201	→	150
268	→	1758
619	→	1188
1170	→	417
912	→	97
141	→	90
141	→	1275
150	→	958
150	→	1008
150	→	1169
983	→	88
983	→	587
983	→	439
983	→	192
983	→	40
983	→	325
983	→	496
983	→	1
983	→	142
983	→	1796
1937	→	667
1937	→	1944
1339	→	1365
1921	→	855
1913	→	9
173	→	143
788	→	779
779	→	939
911	→	1388
171	→	143
810	→	824
810	→	920
6	→	42
6	→	243
6	→	372
6	→	441
6	→	474
6	→	591
1193	→	535
1193	→	1523
1235	→	414
792	→	1363
1240	→	1319
116	→	1842
88	→	9
88	→	118
88	→	170
88	→	820
1853	→	414
823	→	809
823	→	1359
1397	→	1922
799	→	2
799	→	513
799	→	628
982	→	1930
1282	→	1777
1282	→	1799
1282	→	1805
1041	→	306
1041	→	627
1041	→	637
1041	→	8
1041	→	370
1041	→	512
1041	→	565
1041	→	416
1041	→	241
1041	→	5
1041	→	567
1041	→	244
1450	→	749
1450	→	656
1450	→	326
1450	→	574
1450	→	455
1450	→	260
1450	→	63
1450	→	387
1450	→	533
1450	→	3
1450	→	698
1450	→	352
1450	→	780
1450	→	1374
1450	→	1808
1450	→	1802
288	→	263
288	→	1267
1205	→	535
1131	→	1844
1364	→	745
764	→	880
699	→	668
270	→	1234
270	→	1550
1146	→	609
657	→	647
264	→	595
665	→	1196
665	→	1483
1346	→	1850
1516	→	855
117	→	90
117	→	830
117	→	591
117	→	441
117	→	243
117	→	42
117	→	372
117	→	474
117	→	6
117	→	602
117	→	592
2	→	87
2	→	221
2	→	351
2	→	472
2	→	510
2	→	593
937	→	1190
11	→	848
1347	→	1858
1347	→	1938
4	→	65
4	→	223
4	→	353
4	→	457
4	→	498
4	→	589
1018	→	477
1504	→	9
1945	→	881
244	→	193
244	→	306
244	→	1221
1650	→	627
1650	→	304
1650	→	5
1650	→	193
1650	→	242
1222	→	414
419	→	800
1821	→	417
425	→	414
440	→	417
959	→	1157
66	→	9
66	→	89
66	→	172
66	→	808
1748	→	1135
1043	→	1035
602	→	830
1843	→	535
1843	→	1918
1224	→	414
373	→	326
373	→	710
887	→	654
972	→	959
1915	→	855
63	→	1771
63	→	1962
925	→	96
1925	→	667
1555	→	667
1835	→	535
1835	→	1914
497	→	475
497	→	548
636	→	3
636	→	749
636	→	656
636	→	326
636	→	698
636	→	352
636	→	780
636	→	1374
636	→	1808
636	→	1802
720	→	1086
720	→	1099
1963	→	667
335	→	5
335	→	627
335	→	323
335	→	193
335	→	304
335	→	242
697	→	668
1247	→	1834
1939	→	667
1939	→	1942
1543	→	667
1559	→	881
1020	→	1009
1878	→	325
1878	→	1883
1187	→	480
1943	→	881
635	→	971
635	→	1019
635	→	1184
290	→	263
1563	→	881
417	→	789
1861	→	414
806	→	1192
1239	→	1638
64	→	9
64	→	116
64	→	818
957	→	715
957	→	1695
957	→	477
957	→	1045
957	→	142
957	→	1796
957	→	1776
1122	→	197
1133	→	627
1133	→	5
1133	→	323
1133	→	193
1510	→	849
709	→	668
458	→	417
458	→	778
566	→	601
566	→	625
566	→	763
566	→	904
566	→	1284
414	→	1055
414	→	1134
414	→	1155
1372	→	769
905	→	1042
1484	→	809
1484	→	1583
821	→	809
1720	→	9
1886	→	667
17	→	1536
946	→	334
1569	→	668
836	→	815
714	→	1775
714	→	1797
714	→	1807
1537	→	667
1502	→	9
242	→	193
242	→	304
242	→	1219
1260	→	1592
1464	→	810
666	→	6
666	→	904
666	→	625
666	→	566
666	→	830
666	→	602
666	→	592
666	→	621
666	→	594
666	→	1155
666	→	1055
666	→	414
666	→	1861
664	→	1044
664	→	1640
1919	→	855
567	→	637
567	→	1495
762	→	413
413	→	1503
324	→	263
1990	→	1739
1696	→	942
1266	→	1259
1796	→	142
1368	→	756
865	→	1121
865	→	1361
1054	→	637
1054	→	567
1054	→	831
1360	→	717
722	→	334
722	→	1441
829	→	805
388	→	326
388	→	696
388	→	1564
1708	→	948
1264	→	1259
1561	→	881
1649	→	1836
1959	→	763
711	→	668
1165	→	714
1798	→	262
1285	→	1276
790	→	779
790	→	1259
1955	→	1947
807	→	3
807	→	749
807	→	656
807	→	326
807	→	698
807	→	352
807	→	629
807	→	780
807	→	1374
807	→	1808
807	→	1802
1520	→	855
575	→	566
195	→	771
1233	→	1226
43	→	9
594	→	566
594	→	621
1065	→	831
1065	→	637
1065	→	1495
1065	→	567
1829	→	417
418	→	734
1218	→	570
1759	→	1739
660	→	913
961	→	1509
354	→	326
354	→	667
669	→	888
785	→	947
785	→	973
396	→	270
1449	→	1940
1152	→	326
603	→	1324
1992	→	1739
551	→	536
1961	→	927
442	→	417
442	→	1034
442	→	1463
798	→	1542
1702	→	1009
721	→	1123
721	→	1338
721	→	1956
475	→	552
475	→	714
475	→	1373
151	→	1
151	→	41
151	→	10
151	→	626
151	→	622
151	→	43
151	→	1842
151	→	781
151	→	64
151	→	88
151	→	855
151	→	715
151	→	659
151	→	1056
151	→	415
1590	→	1713
1590	→	1732
1590	→	1828
644	→	1544
1802	→	326
191	→	143
415	→	1
415	→	855
415	→	822
415	→	190
415	→	820
415	→	118
415	→	9
415	→	170
415	→	88
415	→	715
415	→	818
415	→	116
415	→	64
415	→	626
415	→	659
415	→	43
415	→	781
415	→	1056
415	→	1772
1096	→	41
1096	→	587
1096	→	439
1096	→	192
1096	→	40
1096	→	325
1096	→	496
1096	→	1
1096	→	10
327	→	389
327	→	751
1941	→	667
1262	→	924
1189	→	535
1189	→	1519
1135	→	1124
819	→	809
1024	→	1009
879	→	654
1808	→	326
513	→	475
513	→	535
307	→	263
307	→	1265
2₁(406)	→	407
2₁(1092)	→	1093
2₁(351)	→	352
2₁(482)	→	483
2₁(1645)	→	1646
2₁(828)	→	829
2₁(738)	→	739
2₁(1885)	→	1886
2₁(196)	→	197
2₁(1151)	→	1152
2₁(411)	→	412
2₁(1121)	→	1122
2₁(741)	→	742
2₁(1392)	→	1393
2₁(1922)	→	1923
2₁(749)	→	750
2₁(1388)	→	1389
2₁(1363)	→	1364
2₁(479)	→	480
2₁(1093)	→	1094
2₁(480)	→	481
2₁(1962)	→	1963
2₁(370)	→	371
2₁(962)	→	963
2₁(1155)	→	1156
2₁(1938)	→	1939
2₁(1164)	→	1165
2₁(1807)	→	1808
2₁(923)	→	924
2₁(785)	→	786
2₁(1410)	→	1411
2₁(763)	→	764
2₁(1444)	→	1445
2₁(793)	→	794
2₁(1321)	→	1322
2₁(1936)	→	1937
2₁(1340)	→	1341
2₁(779)	→	780
2₁(422)	→	423
2₁(325)	→	326
2₁(933)	→	934
2₁(1590)	→	1591
2₁(929)	→	930
2₁(1544)	→	1545
2₁(886)	→	887
2₁(801)	→	802
2₁(1550)	→	1551
2₁(417)	→	418
2₁(1805)	→	1806
2₁(1095)	→	1096
2₁(649)	→	650
2₁(943)	→	944
2₁(915)	→	916
2₁(635)	→	636
2₁(850)	→	851
2₁(652)	→	653
2₁(150)	→	151
2₁(1157)	→	1158
2₁(795)	→	796
2₁(571)	→	572
2₁(1373)	→	1374
2₁(1040)	→	1041
2₁(1153)	→	1154
2₁(1930)	→	1931
2₁(661)	→	662
2₁(869)	→	870
2₁(632)	→	633
2₁(1801)	→	1802
2₁(849)	→	850
2₁(853)	→	854
2₁(922)	→	923
2₁(747)	→	748
2₁(12)	→	13
2₁(1536)	→	1537
2₁(618)	→	619
2₁(387)	→	388
2₁(1924)	→	1925
2₁(1162)	→	1163
2₁(744)	→	745
2₁(976)	→	977
2₁(1940)	→	1941
2₁(1246)	→	1247
2₁(668)	→	669
2₁(1280)	→	1281
2₁(1338)	→	1339
2₁(420)	→	421
2₁(1225)	→	1226
2₁(1587)	→	1588
2₁(1277)	→	1278
2₁(1640)	→	1641
2₁(11)	→	12
2₁(977)	→	978
2₁(1934)	→	1935
2₁(961)	→	962
2₁(884)	→	885
2₁(909)	→	910
2₁(662)	→	663
2₁(1138)	→	1139
2₁(628)	→	629
2₁(97)	→	98
2₁(1232)	→	1233
2₁(1322)	→	1323
2₁(603)	→	604
2₁(1542)	→	1543
2₁(1638)	→	1639
2₁(353)	→	354
2₁(811)	→	812
2₁(1394)	→	1395
2₁(197)	→	198
2₁(1279)	→	1280
2₁(651)	→	652
2₁(413)	→	414
2₁(372)	→	373
2₁(803)	→	804
2₁(1554)	→	1555
2₁(147)	→	148
2₁(1552)	→	1553
2₁(148)	→	149
2₁(1186)	→	1187
2₁(1928)	→	1929
2₁(193)	→	194
0₂(948)	→	949
0₂(1023)	→	1024
0₂(1015)	→	1016
0₂(1010)	→	1011
0₂(954)	→	955
0₂(1948)	→	1949
0₂(1055)	→	1056
0₂(1099)	→	1100
0₂(1019)	→	1020
0₂(1701)	→	1702
0₂(1989)	→	1990
0₂(1991)	→	1992
0₂(1049)	→	1050
0₂(1050)	→	1051
0₂(947)	→	948
0₂(1008)	→	1009
0₂(1775)	→	1776
0₂(1777)	→	1778
0₂(1713)	→	1714
0₂(1061)	→	1062
0₂(1738)	→	1739
0₂(1758)	→	1759
0₂(1744)	→	1745
0₂(1743)	→	1744
0₂(1771)	→	1772
0₂(1044)	→	1045
0₂(1060)	→	1061
0₂(949)	→	950
0₂(1956)	→	1957
0₂(1009)	→	1010
0₂(1070)	→	1071
0₂(1707)	→	1708
2₂(1012)	→	1013
2₂(1064)	→	1065
2₂(1011)	→	1012
2₂(951)	→	952
2₂(1950)	→	1951
2₂(1747)	→	1748
2₂(1106)	→	1107
2₂(1951)	→	1952
2₂(950)	→	951
2₂(1053)	→	1054
2₂(1105)	→	1106
2₂(1108)	→	1109
5₂(1949)	→	1950
5₂(1952)	→	1953
5₂(1107)	→	1108
5₂(1101)	→	1102
0₁(794)	→	795
0₁(616)	→	617
0₁(419)	→	420
0₁(1276)	→	1277
0₁(941)	→	942
0₁(754)	→	755
0₁(1359)	→	1360
0₁(40)	→	41
0₁(65)	→	66
0₁(1503)	→	1504
0₁(1644)	→	1645
0₁(1695)	→	1696
0₁(1643)	→	1644
0₁(959)	→	960
0₁(716)	→	717
0₁(1036)	→	1037
0₁(331)	→	332
0₁(87)	→	88
0₁(1344)	→	1345
0₁(93)	→	94
0₁(540)	→	541
0₁(1130)	→	1131
0₁(1126)	→	1127
0₁(650)	→	651
0₁(541)	→	542
0₁(1240)	→	1241
0₁(856)	→	857
0₁(974)	→	975
0₁(1282)	→	1283
0₁(9)	→	10
0₁(791)	→	792
0₁(766)	→	767
0₁(391)	→	392
0₁(775)	→	776
0₁(860)	→	861
0₁(767)	→	768
0₁(960)	→	961
0₁(1732)	→	1733
0₁(714)	→	715
0₁(1509)	→	1510
0₁(623)	→	624
0₁(625)	→	626
0₁(1920)	→	1921
0₁(1914)	→	1915
0₁(1912)	→	1913
0₁(826)	→	827
0₁(721)	→	722
0₁(612)	→	613
0₁(1160)	→	1161
0₁(1393)	→	1394
0₁(268)	→	269
0₁(1244)	→	1245
0₁(965)	→	966
0₁(1086)	→	1087
0₁(673)	→	674
0₁(1515)	→	1516
0₁(672)	→	673
0₁(654)	→	655
0₁(8)	→	9
0₁(1144)	→	1145
0₁(63)	→	64
0₁(973)	→	974
0₁(621)	→	622
0₁(1037)	→	1038
0₁(1369)	→	1370
0₁(94)	→	95
0₁(264)	→	265
0₁(1345)	→	1346
0₁(542)	→	543
0₁(1621)	→	1622
0₁(883)	→	884
0₁(1795)	→	1796
0₁(409)	→	410
0₁(266)	→	267
0₁(1390)	→	1391
0₁(1396)	→	1397
0₁(743)	→	744
0₁(1721)	→	1722
0₁(848)	→	849
0₁(877)	→	878
0₁(568)	→	569
0₁(611)	→	612
0₁(658)	→	659
0₁(758)	→	759
0₁(10)	→	11
0₁(932)	→	933
0₁(476)	→	477
0₁(780)	→	781
0₁(602)	→	603
0₁(873)	→	874
0₁(975)	→	976
0₁(920)	→	921
0₁(717)	→	718
0₁(1097)	→	1098
0₁(958)	→	959
0₁(1501)	→	1502
0₁(940)	→	941
0₁(1589)	→	1590
0₁(857)	→	858
0₁(1278)	→	1279
0₁(760)	→	761
0₁(969)	→	970
0₁(631)	→	632
0₁(1523)	→	1524
0₁(917)	→	918
0₁(648)	→	649
0₁(15)	→	16
0₁(1519)	→	1520
0₁(980)	→	981
0₁(1918)	→	1919
0₁(784)	→	785
0₁(1719)	→	1720
0₁(971)	→	972
0₁(911)	→	912
0₁(634)	→	635
0₁(1521)	→	1522
0₁(855)	→	856
0₁(538)	→	539
0₁(572)	→	573
0₁(1239)	→	1240
0₁(42)	→	43
0₁(1128)	→	1129
0₁(414)	→	415
0₁(797)	→	798
0₁(739)	→	740
0₁(664)	→	665
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
4₂(1739)	→	1740
4₂(1056)	→	1057
4₂(1045)	→	1046
4₂(1947)	→	1948
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
5₁(1123)	→	1124
5₁(143)	→	144
5₁(868)	→	869
5₁(756)	→	757
5₁(1230)	→	1231
5₁(1136)	→	1137
5₁(223)	→	224
5₁(192)	→	193
5₁(906)	→	907
5₁(535)	→	536
5₁(1495)	→	1496
5₁(830)	→	831
5₁(1558)	→	1559
5₁(260)	→	261
5₁(550)	→	551
5₁(241)	→	242
5₁(198)	→	199
5₁(1094)	→	1095
5₁(1259)	→	1260
5₁(921)	→	922
5₁(745)	→	746
5₁(546)	→	547
5₁(1944)	→	1945
5₁(608)	→	609
5₁(334)	→	335
5₁(566)	→	567
5₁(149)	→	150
5₁(1560)	→	1561
5₁(888)	→	889
5₁(1799)	→	1800
5₁(1562)	→	1563
5₁(813)	→	814
5₁(910)	→	911
5₁(1134)	→	1135
5₁(752)	→	753
5₁(737)	→	738
5₁(548)	→	549
5₁(851)	→	852
5₁(1588)	→	1589
5₁(642)	→	643
5₁(1797)	→	1798
5₁(1564)	→	1565
5₁(924)	→	925
5₁(880)	→	881
5₁(552)	→	553
5₁(1088)	→	1089
5₁(389)	→	390
5₁(772)	→	773
5₁(1566)	→	1567
5₁(1446)	→	1447
5₁(1942)	→	1943
5₁(831)	→	832
5₁(221)	→	222
5₁(720)	→	721
5₁(639)	→	640
5₁(243)	→	244
5₁(1584)	→	1585
4₁(601)	→	602
4₁(751)	→	752
4₁(881)	→	882
4₁(674)	→	675
4₁(765)	→	766
4₁(781)	→	782
4₁(646)	→	647
4₁(1395)	→	1396
4₁(1219)	→	1220
4₁(589)	→	590
4₁(945)	→	946
4₁(1346)	→	1347
4₁(1649)	→	1650
4₁(410)	→	411
4₁(614)	→	615
4₁(565)	→	566
4₁(265)	→	266
4₁(1221)	→	1222
4₁(669)	→	670
4₁(872)	→	873
4₁(1463)	→	1464
4₁(615)	→	616
4₁(593)	→	594
4₁(477)	→	478
4₁(809)	→	810
4₁(118)	→	119
4₁(930)	→	931
4₁(1858)	→	1859
4₁(796)	→	797
4₁(1958)	→	1959
4₁(870)	→	871
4₁(800)	→	801
4₁(1242)	→	1243
4₁(595)	→	596
4₁(1860)	→	1861
4₁(1243)	→	1244
4₁(140)	→	141
4₁(596)	→	597
4₁(1442)	→	1443
4₁(269)	→	270
4₁(1642)	→	1643
4₁(1247)	→	1248
4₁(591)	→	592
4₁(882)	→	883
4₁(574)	→	575
4₁(1341)	→	1342
4₁(536)	→	537
4₁(891)	→	892
4₁(876)	→	877
4₁(1447)	→	1448
4₁(390)	→	391
4₁(1127)	→	1128
4₁(656)	→	657
4₁(1623)	→	1624
4₁(89)	→	90
4₁(1234)	→	1235
4₁(865)	→	866
4₁(806)	→	807
4₁(761)	→	762
4₁(587)	→	588
4₁(1161)	→	1162
4₁(937)	→	938
4₁(423)	→	424
4₁(599)	→	600
4₁(1367)	→	1368
4₁(878)	→	879
4₁(116)	→	117
4₁(1223)	→	1224
4₁(1852)	→	1853
4₁(619)	→	620
4₁(1261)	→	1262
4₁(1236)	→	1237
4₁(1131)	→	1132
4₁(1556)	→	1557
4₁(567)	→	568
4₁(665)	→	666
4₁(641)	→	642
4₁(633)	→	634
4₁(814)	→	815
4₁(1238)	→	1239
4₁(537)	→	538
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
3₁(92)	→	93
3₁(710)	→	711
3₁(916)	→	917
3₁(816)	→	817
3₁(606)	→	607
3₁(1371)	→	1372
3₁(827)	→	828
3₁(199)	→	200
3₁(17)	→	18
3₁(332)	→	333
3₁(885)	→	886
3₁(90)	→	91
3₁(928)	→	929
3₁(670)	→	671
3₁(481)	→	482
3₁(1227)	→	1228
3₁(1125)	→	1126
3₁(1129)	→	1130
3₁(1184)	→	1185
3₁(1441)	→	1442
3₁(708)	→	709
3₁(146)	→	147
3₁(263)	→	264
3₁(864)	→	865
3₁(834)	→	835
3₁(696)	→	697
3₁(13)	→	14
3₁(1449)	→	1450
3₁(472)	→	473
3₁(815)	→	816
3₁(979)	→	980
3₁(1182)	→	1183
3₁(144)	→	145
3₁(964)	→	965
3₁(1035)	→	1036
3₁(966)	→	967
3₁(667)	→	668
3₁(890)	→	891
3₁(1877)	→	1878
3₁(306)	→	307
3₁(718)	→	719
3₁(1448)	→	1449
3₁(1592)	→	1593
3₁(783)	→	784
3₁(539)	→	540
3₁(630)	→	631
3₁(820)	→	821
3₁(874)	→	875
3₁(1226)	→	1227
3₁(407)	→	408
3₁(798)	→	799
3₁(392)	→	393
3₁(936)	→	937
3₁(1169)	→	1170
3₁(267)	→	268
3₁(145)	→	146
3₁(675)	→	676
3₁(1648)	→	1649
3₁(1342)	→	1343
3₁(1228)	→	1229
3₁(982)	→	983
3₁(808)	→	809
3₁(1646)	→	1647
3₁(735)	→	736
3₁(1339)	→	1340
3₁(913)	→	914
3₁(416)	→	417
3₁(1042)	→	1043
3₁(698)	→	699
3₁(329)	→	330
3₁(734)	→	735
3₁(812)	→	813
3₁(1140)	→	1141
3₁(643)	→	644
3₁(805)	→	806
3₁(967)	→	968
3₁(942)	→	943
3₁(822)	→	823
3₁(1483)	→	1484
3₁(304)	→	305
3₁(14)	→	15
3₁(1822)	→	1823
3₁(866)	→	867
3₁(934)	→	935
3₁(904)	→	905
3₁(663)	→	664
3₁(1039)	→	1040
3₁(629)	→	630
3₁(323)	→	324
3₁(804)	→	805
3₁(478)	→	479
3₁(782)	→	783
3₁(439)	→	440
3₁(746)	→	747
3₁(908)	→	909
3₁(1132)	→	1133
3₁(907)	→	908
3₁(1145)	→	1146
3₁(424)	→	425
3₁(605)	→	606
3₁(833)	→	834
3₁(852)	→	853
3₁(768)	→	769
3₁(824)	→	825
3₁(1445)	→	1446
3₁(1090)	→	1091
3₁(1389)	→	1390
3₁(327)	→	328
3₁(16)	→	17
3₁(867)	→	868
3₁(1245)	→	1246
3₁(270)	→	271
3₁(1641)	→	1642
3₁(395)	→	396
3₁(457)	→	458
3₁(644)	→	645
3₁(963)	→	964
3₁(1586)	→	1587
3₁(1124)	→	1125
3₁(759)	→	760
3₁(1347)	→	1348
3₁(1034)	→	1035
3₁(262)	→	263
3₁(1143)	→	1144
3₁(569)	→	570
3₁(764)	→	765
3₁(91)	→	92
3₁(757)	→	758
3₁(598)	→	599
3₁(1142)	→	1143
3₁(715)	→	716
3₁(455)	→	456
3₁(195)	→	196
3₁(773)	→	774
3₁(637)	→	638
3₁(289)	→	290
3₁(1397)	→	1398
3₁(194)	→	195
3₁(742)	→	743
3₁(617)	→	618
3₁(287)	→	288
3₁(1158)	→	1159
3₁(981)	→	982
3₁(393)	→	394
3₁(1217)	→	1218
3₁(1091)	→	1092
3₁(96)	→	97
3₁(1568)	→	1569
3₁(712)	→	713
3₁(330)	→	331
3₁(441)	→	442
3₁(1828)	→	1829
3₁(818)	→	819
3₁(978)	→	979
3₁(1585)	→	1586
3₁(1089)	→	1090
3₁(1820)	→	1821
3₁(1163)	→	1164
3₁(604)	→	605
3₁(412)	→	413
1₁(1324)	→	1325
1₁(774)	→	775
1₁(570)	→	571
1₁(1188)	→	1189
1₁(1365)	→	1366
1₁(1883)	→	1884
1₁(418)	→	419
1₁(1038)	→	1039
1₁(512)	→	513
1₁(190)	→	191
1₁(1263)	→	1264
1₁(1361)	→	1362
1₁(326)	→	327
1₁(653)	→	654
1₁(1319)	→	1320
1₁(778)	→	779
1₁(905)	→	906
1₁(835)	→	836
1₁(736)	→	737
1₁(408)	→	409
1₁(597)	→	598
1₁(1241)	→	1242
1₁(498)	→	499
1₁(333)	→	334
1₁(859)	→	860
1₁(1960)	→	1961
1₁(802)	→	803
1₁(1192)	→	1193
1₁(328)	→	329
1₁(647)	→	648
1₁(1844)	→	1845
1₁(170)	→	171
1₁(510)	→	511
1₁(1583)	→	1584
1₁(1834)	→	1835
1₁(1320)	→	1321
1₁(1267)	→	1268
1₁(875)	→	876
1₁(638)	→	639
1₁(914)	→	915
1₁(1190)	→	1191
1₁(753)	→	754
1₁(1265)	→	1266
1₁(1964)	→	1965
1₁(1087)	→	1088
1₁(640)	→	641
1₁(613)	→	614
1₁(858)	→	859
1₁(1647)	→	1648
1₁(607)	→	608
1₁(1229)	→	1230
1₁(1284)	→	1285
1₁(1275)	→	1276
1₁(944)	→	945
1₁(1281)	→	1282
1₁(771)	→	772
1₁(1443)	→	1444
1₁(1836)	→	1837
1₁(1260)	→	1261
1₁(627)	→	628
1₁(1842)	→	1843
1₁(1204)	→	1205
1₁(810)	→	811
1₁(1139)	→	1140
1₁(609)	→	610
1₁(533)	→	534
1₁(1198)	→	1199
1₁(889)	→	890
1₁(769)	→	770
1₁(394)	→	395
1₁(475)	→	476
1₁(935)	→	936
1₁(142)	→	143
1₁(926)	→	927
1₁(1159)	→	1160
1₁(172)	→	173
1₁(660)	→	661
1₁(918)	→	919
1₁(671)	→	672
1₁(1850)	→	1851
1₁(789)	→	790
1₁(792)	→	793
1₁(832)	→	833
1₁(496)	→	497
1₁(659)	→	660
1₁(200)	→	201
1₁(1196)	→	1197
1₁(719)	→	720
1₁(421)	→	422
1₁(776)	→	777
1₁(787)	→	788
1₁(95)	→	96
1₁(825)	→	826
1₁(939)	→	940
1₁(927)	→	928
1₁(1343)	→	1344
1₁(1391)	→	1392
1₁(474)	→	475
1₁(1141)	→	1142
1₂(1051)	→	1052
1₂(1745)	→	1746
1₂(1100)	→	1101
1₂(1062)	→	1063
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
3₂(1048)	→	1049
3₂(1013)	→	1014
3₂(1058)	→	1059
3₂(1017)	→	1018
3₂(955)	→	956
3₂(1103)	→	1104
3₂(1742)	→	1743
3₂(956)	→	957
3₂(1057)	→	1058
3₂(1741)	→	1742
3₂(952)	→	953
3₂(1102)	→	1103
3₂(953)	→	954
3₂(1063)	→	1064
3₂(1052)	→	1053
3₂(1740)	→	1741
3₂(1059)	→	1060
3₂(1016)	→	1017
3₂(1046)	→	1047
3₂(1047)	→	1048
3₂(1946)	→	1947
3₂(1014)	→	1015
3₂(1954)	→	1955
3₂(1746)	→	1747
3₂(1104)	→	1105

The automaton is closed under rewriting as it is compatible.