Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4827)

The rewrite relation of the following TRS is considered.

2(4(2(x1)))	→	0(2(0(0(5(1(0(2(0(4(x1))))))))))	(1)
1(4(2(1(x1))))	→	2(4(1(5(4(3(2(3(1(2(x1))))))))))	(2)
1(4(4(2(x1))))	→	3(4(0(3(0(2(5(5(1(2(x1))))))))))	(3)
1(5(3(1(x1))))	→	1(1(5(4(3(0(2(1(1(1(x1))))))))))	(4)
1(5(4(0(x1))))	→	3(3(1(1(1(4(0(1(0(0(x1))))))))))	(5)
2(2(4(1(x1))))	→	0(2(2(0(3(0(2(5(0(0(x1))))))))))	(6)
2(4(2(1(x1))))	→	0(1(0(3(5(3(2(3(2(1(x1))))))))))	(7)
1(4(1(2(0(x1)))))	→	5(2(0(4(0(5(0(5(1(2(x1))))))))))	(8)
1(4(2(4(0(x1)))))	→	5(1(4(3(5(0(0(0(3(0(x1))))))))))	(9)
1(4(4(1(4(x1)))))	→	3(3(2(1(0(5(0(5(2(4(x1))))))))))	(10)
1(5(4(2(1(x1)))))	→	3(4(1(3(3(3(3(3(0(1(x1))))))))))	(11)
2(1(4(4(1(x1)))))	→	2(5(0(2(2(1(2(0(0(0(x1))))))))))	(12)
3(2(4(4(2(x1)))))	→	3(3(3(0(2(3(1(4(0(4(x1))))))))))	(13)
5(3(2(1(5(x1)))))	→	0(4(0(4(3(4(3(2(2(5(x1))))))))))	(14)
1(4(0(4(0(5(x1))))))	→	5(1(1(2(4(0(2(1(3(5(x1))))))))))	(15)
1(5(5(3(2(2(x1))))))	→	0(1(2(4(0(5(0(1(2(3(x1))))))))))	(16)
2(5(3(0(4(4(x1))))))	→	2(2(5(0(4(4(5(0(4(4(x1))))))))))	(17)
3(1(2(4(2(4(x1))))))	→	4(3(2(0(1(2(3(0(5(4(x1))))))))))	(18)
3(4(2(2(0(5(x1))))))	→	0(1(3(1(2(0(2(0(4(3(x1))))))))))	(19)
4(1(1(4(0(4(x1))))))	→	4(0(2(3(5(0(4(1(5(2(x1))))))))))	(20)
5(5(0(1(4(2(x1))))))	→	5(2(0(1(2(4(1(3(3(3(x1))))))))))	(21)
0(1(4(0(0(4(2(x1)))))))	→	0(1(0(1(5(2(1(0(1(2(x1))))))))))	(22)
1(0(4(4(2(5(5(x1)))))))	→	1(0(4(1(0(5(3(5(2(5(x1))))))))))	(23)
1(3(0(5(4(1(4(x1)))))))	→	1(0(3(0(1(3(1(3(2(4(x1))))))))))	(24)
1(4(2(4(1(3(5(x1)))))))	→	4(4(3(3(5(0(0(0(2(5(x1))))))))))	(25)
1(5(5(4(0(2(5(x1)))))))	→	1(1(4(3(2(1(4(1(1(5(x1))))))))))	(26)
2(4(2(1(5(4(1(x1)))))))	→	0(1(0(4(0(3(0(5(4(1(x1))))))))))	(27)
4(2(5(0(1(4(2(x1)))))))	→	4(2(5(3(0(1(2(3(2(1(x1))))))))))	(28)
5(2(2(0(4(4(2(x1)))))))	→	2(0(1(1(2(4(5(5(0(2(x1))))))))))	(29)
5(2(2(0(5(4(0(x1)))))))	→	1(5(1(3(0(0(1(3(2(1(x1))))))))))	(30)
5(3(1(4(2(4(0(x1)))))))	→	5(5(3(1(1(3(0(1(5(2(x1))))))))))	(31)
5(5(1(4(4(2(5(x1)))))))	→	3(5(0(5(4(0(1(5(2(5(x1))))))))))	(32)

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:

1198	→	1190
1659	→	494
239	→	186
329	→	16
591	→	4
591	→	637
591	→	493
591	→	471
591	→	490
591	→	1678
1627	→	89
964	→	362
1940	→	1661
731	→	9
818	→	645
818	→	330
818	→	5
818	→	186
818	→	197
818	→	118
818	→	1826
1573	→	1563
486	→	471
486	→	1101
1863	→	1933
1579	→	89
1608	→	89
1335	→	571
1335	→	637
1335	→	471
1335	→	492
1335	→	581
1335	→	1684
685	→	4
685	→	571
685	→	637
685	→	471
685	→	492
685	→	581
685	→	1684
89	→	580
89	→	676
1674	→	1661
1057	→	1490
1057	→	1510
1057	→	1691
1057	→	1795
1680	→	1661
1333	→	1574
338	→	17
1762	→	639
1762	→	1852
1762	→	1927
791	→	1001
87	→	9
87	→	393
87	→	542
87	→	556
87	→	646
87	→	514
87	→	305
87	→	116
87	→	43
87	→	196
87	→	481
87	→	2
87	→	66
87	→	640
1117	→	1092
98	→	5
98	→	645
98	→	330
98	→	186
98	→	197
98	→	118
98	→	641
98	→	1826
286	→	1599
286	→	1817
874	→	216
874	→	1812
874	→	2011
880	→	867
1007	→	1753
10	→	450
10	→	1059
1169	→	1161
97	→	730
97	→	758
97	→	1048
97	→	1116
97	→	1315
1557	→	260
487	→	1673
487	→	1713
1688	→	1661
1794	→	628
1560	→	1915
1560	→	2006
640	→	558
640	→	409
640	→	646
640	→	514
640	→	305
640	→	116
640	→	43
640	→	196
640	→	481
640	→	2
640	→	9
640	→	66
640	→	1298
578	→	865
578	→	959
578	→	1172
448	→	712
448	→	734
448	→	1050
448	→	1282
303	→	1589
303	→	1811
1642	→	473
608	→	194
471	→	493
471	→	637
471	→	4
471	→	1484
471	→	1661
471	→	1676
1606	→	89
882	→	867
882	→	1215
530	→	502
530	→	961
1363	→	571
1363	→	637
1363	→	471
1363	→	492
1363	→	581
1363	→	1684
543	→	534
167	→	5
167	→	645
167	→	330
167	→	186
167	→	197
167	→	216
167	→	118
167	→	1826
167	→	1812
167	→	2011
998	→	610
1008	→	1576
1008	→	1805
472	→	601
472	→	628
472	→	119
472	→	531
472	→	269
472	→	88
472	→	86
472	→	185
472	→	491
472	→	1
511	→	5
511	→	216
511	→	1812
511	→	2011
502	→	560
502	→	582
502	→	965
502	→	1033
119	→	89
119	→	658
119	→	913
119	→	1010
1916	→	89
1575	→	89
1670	→	452
878	→	867
1870	→	2022
1870	→	2032
1870	→	2046
1532	→	89
491	→	1683
491	→	1729
638	→	1872
1724	→	560
1851	→	884
260	→	360
260	→	881
260	→	1052
260	→	3
1953	→	560
18	→	1
18	→	676
18	→	670
18	→	410
18	→	394
18	→	89
18	→	117
18	→	1610
18	→	1604
18	→	1768
978	→	414
1577	→	89
2047	→	118
3	→	41
3	→	157
3	→	240
3	→	286
3	→	487
3	→	512
1362	→	1527
1362	→	1529
1362	→	1558
1362	→	1572
1362	→	1935
939	→	928
333	→	652
600	→	3
600	→	360
600	→	412
600	→	260
218	→	186
772	→	735
1102	→	1093
1011	→	1002
500	→	367
1812	→	118
187	→	843
187	→	1297
1678	→	1661
1424	→	570
9	→	409
9	→	544
9	→	558
729	→	9
1706	→	547
1714	→	560
914	→	332
5	→	65
5	→	137
5	→	217
5	→	259
5	→	485
5	→	527
774	→	9
1200	→	1190
2041	→	630
95	→	894
95	→	909
95	→	1656
515	→	502
1999	→	118
671	→	659
1918	→	89
1764	→	570
361	→	977
241	→	186
692	→	590
692	→	1227
1134	→	582
1134	→	502
1134	→	529
1134	→	284
1134	→	139
1134	→	67
1134	→	238
1134	→	489
1134	→	6
1134	→	515
1134	→	1724
947	→	928
1768	→	570
1636	→	892
1970	→	495
1970	→	1034
1806	→	118
90	→	159
90	→	592
673	→	659
673	→	1266
1238	→	610
304	→	260
304	→	879
2007	→	118
1800	→	118
700	→	4
700	→	637
700	→	493
700	→	471
700	→	812
1530	→	89
1530	→	1641
1034	→	495
1	→	86
1	→	88
1	→	185
1	→	269
1	→	491
1	→	531
1936	→	194
1308	→	331
287	→	260
1009	→	637
1009	→	471
1009	→	501
1009	→	303
1009	→	118
1009	→	8
1009	→	215
1009	→	470
1009	→	4
1009	→	490
1009	→	1661
1009	→	1678
1730	→	560
1957	→	570
936	→	1671
936	→	1707
1298	→	640
305	→	1609
305	→	1825
549	→	1299
667	→	4
667	→	571
667	→	637
667	→	471
667	→	492
667	→	581
667	→	1684
1267	→	1257
332	→	678
1509	→	702
410	→	386
410	→	1336
1228	→	601
490	→	471
490	→	1114
392	→	267
1938	→	194
1426	→	571
1722	→	560
197	→	186
1173	→	1161
548	→	1827
590	→	1135
590	→	1679
1934	→	442
44	→	9
1283	→	638
1283	→	1307
480	→	4
480	→	637
480	→	471
480	→	490
480	→	1661
480	→	1678
677	→	659
677	→	2040
1515	→	702
1194	→	664
488	→	471
1700	→	502
796	→	1941
796	→	1954
687	→	1461
1676	→	1661
261	→	323
261	→	441
1598	→	89
1398	→	1354
86	→	1767
1592	→	89
675	→	659
269	→	1603
269	→	1819
1099	→	1765
1385	→	1354
268	→	166
1766	→	570
1499	→	9
186	→	330
186	→	411
186	→	645
186	→	821
1883	→	895
138	→	89
138	→	672
138	→	1012
138	→	1237
540	→	1035
1732	→	560
2005	→	118
532	→	502
532	→	963
1528	→	1517
976	→	388
1610	→	89
810	→	1205
639	→	1958
6	→	67
6	→	139
6	→	238
6	→	284
6	→	489
6	→	529
554	→	1170
1032	→	495
1240	→	611
1571	→	710
1051	→	1036
1051	→	1195
577	→	883
577	→	1353
577	→	1423
1456	→	637
1456	→	4
1456	→	493
1456	→	471
1456	→	812
1853	→	194
799	→	1498
799	→	1508
799	→	1699
799	→	1705
799	→	1799
1818	→	118
555	→	6
555	→	582
555	→	502
555	→	91
555	→	528
555	→	1732
1824	→	118
394	→	386
1234	→	603
386	→	609
1047	→	1036
1047	→	1197
1377	→	1354
1297	→	1956
270	→	260
270	→	877
615	→	607
699	→	1254
368	→	358
657	→	578
657	→	809
657	→	1448
485	→	1685
485	→	1731
2033	→	89
665	→	946
1337	→	664
2015	→	570
906	→	260
1684	→	1661
569	→	6
569	→	582
569	→	502
569	→	515
569	→	1724
1672	→	1661
117	→	89
117	→	670
2	→	43
2	→	116
2	→	196
2	→	305
2	→	481
2	→	514
1746	→	560
1060	→	1053
937	→	645
937	→	330
937	→	5
937	→	186
937	→	197
937	→	118
937	→	1826
797	→	1554
797	→	1560
797	→	1937
4	→	8
4	→	118
4	→	215
4	→	303
4	→	470
4	→	501
528	→	502
528	→	1031
941	→	928
449	→	1
449	→	676
449	→	672
449	→	331
449	→	89
449	→	138
449	→	628
449	→	119
449	→	601
449	→	472
449	→	1579
449	→	1590
449	→	1532
449	→	1918
876	→	867
1621	→	89
470	→	1675
470	→	1715
284	→	1591
284	→	1813
557	→	547
1761	→	1850
1761	→	1998
1761	→	2014
478	→	1160
479	→	927
479	→	1382
904	→	260
1814	→	118
802	→	791
66	→	9
359	→	5
359	→	645
359	→	330
359	→	186
359	→	197
359	→	452
359	→	118
359	→	1826
359	→	641
1748	→	560
602	→	693
481	→	1681
481	→	1723
1334	→	1496
1334	→	1514
1334	→	1697
1334	→	1797
1045	→	216
1045	→	1812
1045	→	2011
93	→	1239
1491	→	9
1692	→	502
306	→	260
800	→	645
800	→	330
800	→	5
800	→	186
800	→	197
2023	→	884
2011	→	118
1536	→	884
1600	→	89
1555	→	895
1698	→	502
581	→	571
581	→	975
581	→	1233
684	→	790
684	→	905
684	→	1516
684	→	1562
684	→	1658
636	→	5
636	→	645
636	→	330
636	→	186
636	→	197
636	→	118
636	→	641
636	→	1826
559	→	547
1871	→	1604
1871	→	1768
1871	→	1767
1871	→	1603
1871	→	1683
1871	→	491
1871	→	185
1871	→	86
1871	→	88
1871	→	269
1871	→	531
1871	→	1
989	→	451
759	→	735
1604	→	89
140	→	89
140	→	570
140	→	674
1216	→	595
1455	→	1793
1432	→	571
1497	→	9
1556	→	1917
1556	→	2010
1013	→	1002
1526	→	821
1526	→	411
1526	→	186
1526	→	197
1526	→	118
1526	→	641
1526	→	1826
1559	→	260
1623	→	89
1044	→	1620
1044	→	1807
736	→	1639
1873	→	1862
568	→	942
568	→	1374
635	→	1168
635	→	1973
1049	→	1036
1049	→	1199
1563	→	1628
1686	→	1661
902	→	709
960	→	361
962	→	362
42	→	9
216	→	186
216	→	527
216	→	259
216	→	137
216	→	65
216	→	217
216	→	485
216	→	5
216	→	638
1816	→	118
1316	→	118
579	→	2
579	→	558
579	→	409
579	→	646
579	→	9
579	→	66
579	→	542
579	→	393
579	→	556
579	→	87
1133	→	1622
1133	→	1803
1196	→	1190
1100	→	582
1100	→	502
1100	→	6
1100	→	91
1100	→	528
1100	→	1732
1314	→	118
847	→	683
158	→	89
158	→	668
1657	→	494
458	→	6
458	→	532
458	→	610
458	→	1730
893	→	638
893	→	821
893	→	411
893	→	5
893	→	186
893	→	216
893	→	1812
893	→	2011
572	→	686
909	→	1597
909	→	1815
1383	→	1354
905	→	1607
905	→	1823
17	→	944
17	→	1376
17	→	1535
160	→	352
683	→	1689
683	→	1747
945	→	928
945	→	1431
510	→	940
510	→	1384
1822	→	118
651	→	336
714	→	988
1136	→	1125
1523	→	1882
1361	→	1939
1361	→	1952
68	→	9
68	→	385
68	→	533
68	→	546
666	→	728
666	→	771
666	→	1046
666	→	1313
1928	→	361
703	→	990
215	→	1531
215	→	1556
492	→	471
928	→	1433
1796	→	186
1828	→	699
1682	→	1661
866	→	1327
285	→	260
285	→	875
722	→	676
722	→	670
722	→	1
722	→	89
722	→	117
722	→	1610
482	→	471
482	→	1092
1434	→	571
1058	→	471
744	→	410
744	→	394
744	→	676
744	→	670
744	→	89
744	→	117
744	→	1610
1708	→	560
489	→	1677
489	→	1721
1561	→	260
259	→	1578
259	→	1809
1959	→	570
711	→	676
711	→	670
711	→	89
711	→	117
711	→	672
711	→	138
711	→	410
711	→	394
711	→	331
711	→	1610
711	→	1579
711	→	1010
711	→	658
711	→	642
711	→	913
711	→	119
1798	→	118
358	→	1124
358	→	1660
1955	→	560
1804	→	118
541	→	448
1210	→	479
943	→	928
943	→	1425
195	→	5
195	→	216
195	→	638
195	→	241
195	→	239
195	→	1215
195	→	867
195	→	882
195	→	495
195	→	1034
195	→	1812
195	→	1818
195	→	1814
195	→	2011
1171	→	1161
412	→	1217
412	→	1862
1306	→	118
903	→	1605
903	→	1821
1375	→	1354
910	→	260
1942	→	1661
418	→	165
1218	→	594
669	→	659
1716	→	560
822	→	811
194	→	801
194	→	903
1558	→	1913
1558	→	2004
1826	→	118
966	→	362
1167	→	16
721	→	1533
721	→	1626
721	→	1801
1511	→	702
1263	→	645
1263	→	330
1263	→	5
1263	→	186
1263	→	197
1263	→	118
1263	→	641
1263	→	1826
1590	→	89
1485	→	702
1810	→	118
644	→	193
599	→	938
599	→	1397
1802	→	118
1300	→	650
94	→	1687
94	→	1745
656	→	701
656	→	773
656	→	1188
656	→	1305
1640	→	991
1262	→	1763
1262	→	1960
1914	→	89
1462	→	696
1820	→	118
1534	→	884
1690	→	1661
1808	→	118
545	→	534
1115	→	1093
513	→	502
1974	→	1961
4₁(507)	→	508
4₁(355)	→	356
4₁(1490)	→	1491
4₁(263)	→	264
4₁(639)	→	640
4₁(728)	→	729
4₁(537)	→	538
4₁(1163)	→	1164
4₁(798)	→	799
4₁(634)	→	635
4₁(606)	→	607
4₁(1261)	→	1262
4₁(846)	→	847
4₁(1461)	→	1462
4₁(533)	→	534
4₁(1005)	→	1006
4₁(450)	→	451
4₁(1003)	→	1004
4₁(650)	→	651
4₁(1007)	→	1008
4₁(8)	→	9
4₁(933)	→	934
4₁(1498)	→	1499
4₁(730)	→	731
4₁(585)	→	586
4₁(476)	→	477
4₁(645)	→	646
4₁(1451)	→	1452
4₁(65)	→	66
4₁(67)	→	68
4₁(497)	→	498
4₁(544)	→	545
4₁(86)	→	87
4₁(635)	→	636
4₁(96)	→	97
4₁(1496)	→	1497
4₁(795)	→	796
4₁(93)	→	94
4₁(1192)	→	1193
4₁(712)	→	713
4₁(1262)	→	1263
4₁(560)	→	561
4₁(1041)	→	1042
4₁(554)	→	555
4₁(643)	→	644
4₁(661)	→	662
4₁(816)	→	817
4₁(1053)	→	1054
4₁(1756)	→	1757
4₁(165)	→	166
4₁(1099)	→	1100
4₁(1329)	→	1330
4₁(474)	→	475
4₁(868)	→	869
4₁(695)	→	696
4₁(536)	→	537
4₁(578)	→	579
4₁(773)	→	774
4₁(366)	→	367
4₁(1297)	→	1298
4₁(1054)	→	1055
4₁(1125)	→	1126
4₁(191)	→	192
4₁(41)	→	42
4₁(478)	→	479
4₁(43)	→	44
4₁(572)	→	573
4₁(542)	→	543
4₁(988)	→	989
4₂(1484)	→	1485
4₂(887)	→	888
4₂(1973)	→	1974
4₂(1665)	→	1666
4₂(701)	→	702
4₂(771)	→	772
4₂(1514)	→	1515
4₂(1635)	→	1636
4₂(1521)	→	1522
4₂(1510)	→	1511
4₂(1524)	→	1525
4₂(758)	→	759
4₂(1960)	→	1961
4₂(734)	→	735
4₂(990)	→	991
4₂(1639)	→	1640
4₂(1508)	→	1509
0₂(1850)	→	1851
0₂(898)	→	899
0₂(1628)	→	1629
0₂(2022)	→	2023
0₂(1966)	→	1967
0₂(895)	→	896
0₂(894)	→	895
0₂(884)	→	885
0₂(743)	→	744
0₂(702)	→	703
0₂(1535)	→	1536
0₂(1533)	→	1534
0₂(1569)	→	1570
0₂(735)	→	736
0₂(994)	→	995
0₂(900)	→	901
0₂(740)	→	741
0₂(883)	→	884
0₂(1554)	→	1555
0₂(707)	→	708
0₂(737)	→	738
0₂(1968)	→	1969
0₂(710)	→	711
0₂(704)	→	705
0₂(886)	→	887
0₂(741)	→	742
0₂(708)	→	709
0₂(1664)	→	1665
0₂(1882)	→	1883
3₂(995)	→	996
3₂(1629)	→	1630
3₂(1962)	→	1963
3₂(1564)	→	1565
3₂(1661)	→	1662
3₂(1633)	→	1634
3₂(899)	→	900
3₂(1631)	→	1632
3₂(892)	→	893
3₂(1518)	→	1519
3₂(1568)	→	1569
3₂(891)	→	892
3₂(1630)	→	1631
3₂(992)	→	993
3₂(1520)	→	1521
3₂(1964)	→	1965
3₂(1967)	→	1968
3₂(1566)	→	1567
3₂(997)	→	998
3₂(1632)	→	1633
3₂(996)	→	997
2₁(1760)	→	1761
2₁(1591)	→	1592
2₁(1915)	→	1916
2₁(1001)	→	1002
2₁(1207)	→	1208
2₁(91)	→	92
2₁(641)	→	642
2₁(576)	→	577
2₁(1036)	→	1037
2₁(549)	→	550
2₁(540)	→	541
2₁(330)	→	331
2₁(1767)	→	1768
2₁(1574)	→	1575
2₁(1622)	→	1623
2₁(1127)	→	1128
2₁(495)	→	496
2₁(1354)	→	1355
2₁(594)	→	595
2₁(662)	→	663
2₁(1763)	→	1764
2₁(790)	→	791
2₁(1170)	→	1171
2₁(137)	→	138
2₁(1958)	→	1959
2₁(589)	→	590
2₁(1330)	→	1331
2₁(1599)	→	1600
2₁(1010)	→	1011
2₁(391)	→	392
2₁(161)	→	162
2₁(927)	→	928
2₁(1765)	→	1766
2₁(1753)	→	1754
2₁(1215)	→	1216
2₁(445)	→	446
2₁(714)	→	715
2₁(812)	→	813
2₁(942)	→	943
2₁(1094)	→	1095
2₁(1626)	→	1627
2₁(453)	→	454
2₁(1793)	→	1794
2₁(1042)	→	1043
2₁(1334)	→	1335
2₁(1307)	→	1308
2₁(1160)	→	1161
2₁(472)	→	473
2₁(1605)	→	1606
2₁(793)	→	794
2₁(1529)	→	1530
2₁(946)	→	947
2₁(332)	→	333
2₁(1172)	→	1173
2₁(801)	→	802
2₁(799)	→	800
2₁(1609)	→	1610
2₁(139)	→	140
2₁(1168)	→	1169
2₁(385)	→	386
2₁(1576)	→	1577
2₁(1603)	→	1604
2₁(552)	→	553
2₁(586)	→	587
2₁(1129)	→	1130
2₁(562)	→	563
2₁(393)	→	394
2₁(564)	→	565
2₁(1620)	→	1621
2₁(409)	→	410
2₁(88)	→	89
2₁(442)	→	443
2₁(157)	→	158
2₁(444)	→	445
2₁(1578)	→	1579
2₁(2014)	→	2015
2₁(508)	→	509
2₁(1607)	→	1608
2₁(10)	→	11
2₁(1531)	→	1532
2₁(935)	→	936
2₁(938)	→	939
2₁(1641)	→	1642
2₁(1597)	→	1598
2₁(1012)	→	1013
2₁(118)	→	119
2₁(448)	→	449
2₁(1057)	→	1058
2₁(1227)	→	1228
2₁(188)	→	189
2₁(1097)	→	1098
2₁(1423)	→	1424
2₁(720)	→	721
2₁(1864)	→	1865
2₁(1193)	→	1194
2₁(940)	→	941
2₁(1589)	→	1590
2₁(944)	→	945
2₁(471)	→	472
2₁(843)	→	844
2₁(2032)	→	2033
2₁(1868)	→	1869
2₁(328)	→	329
2₁(502)	→	503
2₁(357)	→	358
2₁(1956)	→	1957
2₁(97)	→	98
2₁(498)	→	499
2₁(656)	→	657
2₁(1913)	→	1914
2₁(116)	→	117
2₁(324)	→	325
2₁(1917)	→	1918
2₁(1254)	→	1255
2₁(666)	→	667
2₁(1869)	→	1870
2₁(16)	→	17
1₀(3)	→	5
1₀(6)	→	5
1₀(5)	→	5
1₀(4)	→	5
1₀(2)	→	5
1₀(1)	→	5
3₀(2)	→	6
3₀(6)	→	6
3₀(4)	→	6
3₀(1)	→	6
3₀(3)	→	6
3₀(5)	→	6
5₂(1939)	→	1940
5₂(1660)	→	1661
5₂(1522)	→	1523
5₂(1673)	→	1674
5₂(1685)	→	1686
5₂(1687)	→	1688
5₂(706)	→	707
5₂(1941)	→	1942
5₂(1669)	→	1670
5₂(1677)	→	1678
5₂(739)	→	740
5₂(1679)	→	1680
5₂(1671)	→	1672
5₂(1689)	→	1690
5₂(1681)	→	1682
5₂(896)	→	897
5₂(1675)	→	1676
5₂(1567)	→	1568
5₂(1683)	→	1684
5₀(1)	→	4
5₀(6)	→	4
5₀(3)	→	4
5₀(5)	→	4
5₀(2)	→	4
5₀(4)	→	4
3₁(415)	→	416
3₁(699)	→	700
3₁(690)	→	691
3₁(1952)	→	1953
3₁(1747)	→	1748
3₁(1233)	→	1234
3₁(1721)	→	1722
3₁(1035)	→	1036
3₁(794)	→	795
3₁(1050)	→	1051
3₁(512)	→	513
3₁(529)	→	530
3₁(1197)	→	1198
3₁(614)	→	615
3₁(1697)	→	1698
3₁(1713)	→	1714
3₁(1731)	→	1732
3₁(553)	→	554
3₁(582)	→	583
3₁(611)	→	612
3₁(1260)	→	1261
3₁(1190)	→	1191
3₁(873)	→	874
3₁(1935)	→	1936
3₁(335)	→	336
3₁(414)	→	415
3₁(687)	→	688
3₁(493)	→	494
3₁(1098)	→	1099
3₁(333)	→	334
3₁(475)	→	476
3₁(1188)	→	1189
3₁(575)	→	576
3₁(913)	→	914
3₁(365)	→	366
3₁(1937)	→	1938
3₁(1046)	→	1047
3₁(602)	→	603
3₁(90)	→	91
3₁(1359)	→	1360
3₁(1259)	→	1260
3₁(360)	→	361
3₁(1699)	→	1700
3₁(977)	→	978
3₁(583)	→	584
3₁(1658)	→	1659
3₁(92)	→	93
3₁(166)	→	167
3₁(1455)	→	1456
3₁(681)	→	682
3₁(527)	→	528
3₁(1048)	→	1049
3₁(452)	→	453
3₁(1002)	→	1003
3₁(566)	→	567
3₁(872)	→	873
3₁(817)	→	818
3₁(1745)	→	1746
3₁(1093)	→	1094
3₁(1954)	→	1955
3₁(1199)	→	1200
3₁(267)	→	268
3₁(814)	→	815
3₁(416)	→	417
3₁(1237)	→	1238
3₁(1723)	→	1724
3₁(648)	→	649
3₁(413)	→	414
3₁(1656)	→	1657
3₁(190)	→	191
3₁(163)	→	164
3₁(1729)	→	1730
3₁(548)	→	549
3₁(1195)	→	1196
3₁(514)	→	515
3₁(473)	→	474
3₁(1715)	→	1716
3₁(1927)	→	1928
3₁(1707)	→	1708
3₁(633)	→	634
3₁(326)	→	327
3₁(455)	→	456
3₁(331)	→	332
3₁(642)	→	643
3₁(531)	→	532
3₁(1355)	→	1356
3₁(1004)	→	1005
3₁(1759)	→	1760
3₁(609)	→	610
3₁(1124)	→	1125
3₁(457)	→	458
3₁(1166)	→	1167
3₁(959)	→	960
3₁(412)	→	413
3₁(1189)	→	1190
3₁(654)	→	655
3₁(1131)	→	1132
3₁(632)	→	633
3₁(792)	→	793
3₁(501)	→	502
3₁(1135)	→	1136
3₁(845)	→	846
3₁(456)	→	457
3₁(1691)	→	1692
3₁(1866)	→	1867
5₁(601)	→	602
5₁(936)	→	937
5₁(646)	→	647
5₁(539)	→	540
5₁(1425)	→	1426
5₁(1448)	→	1449
5₁(353)	→	354
5₁(717)	→	718
5₁(1754)	→	1755
5₁(1454)	→	1455
5₁(683)	→	684
5₁(603)	→	604
5₁(1758)	→	1759
5₁(1039)	→	1040
5₁(929)	→	930
5₁(485)	→	486
5₁(94)	→	95
5₁(1258)	→	1259
5₁(796)	→	797
5₁(491)	→	492
5₁(388)	→	389
5₁(691)	→	692
5₁(481)	→	482
5₁(1208)	→	1209
5₁(595)	→	596
5₁(655)	→	656
5₁(1705)	→	1706
5₁(580)	→	581
5₁(590)	→	591
5₁(811)	→	812
5₁(489)	→	490
5₁(1328)	→	1329
5₁(558)	→	559
5₁(570)	→	571
5₁(574)	→	575
5₁(698)	→	699
5₁(192)	→	193
5₁(810)	→	811
5₁(364)	→	365
5₁(386)	→	387
5₁(470)	→	471
5₁(447)	→	448
5₁(696)	→	697
5₁(631)	→	632
5₁(1165)	→	1166
5₁(358)	→	359
5₁(1452)	→	1453
5₁(1056)	→	1057
5₁(659)	→	660
5₁(1863)	→	1864
5₁(334)	→	335
5₁(1161)	→	1162
5₁(1327)	→	1328
5₁(535)	→	536
5₁(1116)	→	1117
5₁(487)	→	488
5₁(1059)	→	1060
5₁(546)	→	547
5₁(505)	→	506
5₁(1052)	→	1053
5₁(1361)	→	1362
5₁(1433)	→	1434
5₁(323)	→	324
5₁(13)	→	14
5₁(821)	→	822
5₁(660)	→	661
5₁(556)	→	557
5₁(1827)	→	1828
5₁(1431)	→	1432
5₁(931)	→	932
5₁(159)	→	160
5₁(160)	→	161
4₀(3)	→	2
4₀(5)	→	2
4₀(2)	→	2
4₀(4)	→	2
4₀(1)	→	2
4₀(6)	→	2
0₀(2)	→	3
0₀(4)	→	3
0₀(3)	→	3
0₀(6)	→	3
0₀(1)	→	3
0₀(5)	→	3
1₁(689)	→	690
1₁(186)	→	187
1₁(1815)	→	1816
1₁(187)	→	188
1₁(584)	→	585
1₁(217)	→	218
1₁(266)	→	267
1₁(509)	→	510
1₁(1353)	→	1354
1₁(1998)	→	1999
1₁(2006)	→	2007
1₁(565)	→	566
1₁(1801)	→	1802
1₁(1805)	→	1806
1₁(928)	→	929
1₁(1162)	→	1163
1₁(1376)	→	1377
1₁(610)	→	611
1₁(1755)	→	1756
1₁(1209)	→	1210
1₁(791)	→	792
1₁(652)	→	653
1₁(879)	→	880
1₁(1362)	→	1363
1₁(1811)	→	1812
1₁(684)	→	685
1₁(716)	→	717
1₁(640)	→	641
1₁(2010)	→	2011
1₁(1449)	→	1450
1₁(1031)	→	1032
1₁(1239)	→	1240
1₁(1331)	→	1332
1₁(1095)	→	1096
1₁(809)	→	810
1₁(443)	→	444
1₁(390)	→	391
1₁(587)	→	588
1₁(1037)	→	1038
1₁(12)	→	13
1₁(367)	→	368
1₁(871)	→	872
1₁(89)	→	90
1₁(193)	→	194
1₁(1130)	→	1131
1₁(1282)	→	1283
1₁(869)	→	870
1₁(1305)	→	1306
1₁(494)	→	495
1₁(612)	→	613
1₁(1360)	→	1361
1₁(499)	→	500
1₁(1191)	→	1192
1₁(682)	→	683
1₁(567)	→	568
1₁(261)	→	262
1₁(1206)	→	1207
1₁(1795)	→	1796
1₁(797)	→	798
1₁(196)	→	197
1₁(1819)	→	1820
1₁(881)	→	882
1₁(1807)	→	1808
1₁(1821)	→	1822
1₁(215)	→	216
1₁(866)	→	867
1₁(663)	→	664
1₁(1315)	→	1316
1₁(1809)	→	1810
1₁(240)	→	241
1₁(1043)	→	1044
1₁(1823)	→	1824
1₁(1384)	→	1385
1₁(1374)	→	1375
1₁(1132)	→	1133
1₁(605)	→	606
1₁(337)	→	338
1₁(1799)	→	1800
1₁(1382)	→	1383
1₁(1797)	→	1798
1₁(688)	→	689
1₁(2004)	→	2005
1₁(678)	→	679
1₁(638)	→	639
1₁(2046)	→	2047
1₁(265)	→	266
1₁(238)	→	239
1₁(593)	→	594
1₁(1356)	→	1357
1₁(598)	→	599
1₁(875)	→	876
1₁(417)	→	418
1₁(1336)	→	1337
1₁(95)	→	96
1₁(877)	→	878
1₁(550)	→	551
1₁(637)	→	638
1₁(1033)	→	1034
1₁(870)	→	871
1₁(1397)	→	1398
1₁(194)	→	195
1₁(1813)	→	1814
1₁(185)	→	186
1₁(571)	→	572
1₁(596)	→	597
1₁(664)	→	665
1₁(1217)	→	1218
1₁(264)	→	265
1₁(1825)	→	1826
1₁(1332)	→	1333
1₁(693)	→	694
1₁(451)	→	452
1₁(1803)	→	1804
1₁(1817)	→	1818
1₁(503)	→	504
1₁(1313)	→	1314
0₁(1055)	→	1056
0₁(441)	→	442
0₁(1852)	→	1853
0₁(592)	→	593
0₁(1255)	→	1256
0₁(11)	→	12
0₁(1126)	→	1127
0₁(930)	→	931
0₁(327)	→	328
0₁(305)	→	306
0₁(1040)	→	1041
0₁(362)	→	363
0₁(2040)	→	2041
0₁(815)	→	816
0₁(1038)	→	1039
0₁(538)	→	539
0₁(573)	→	574
0₁(1867)	→	1868
0₁(676)	→	677
0₁(653)	→	654
0₁(965)	→	966
0₁(1101)	→	1102
0₁(1862)	→	1863
0₁(867)	→	868
0₁(17)	→	18
0₁(1266)	→	1267
0₁(905)	→	906
0₁(686)	→	687
0₁(1114)	→	1115
0₁(1092)	→	1093
0₁(813)	→	814
0₁(597)	→	598
0₁(551)	→	552
0₁(1556)	→	1557
0₁(665)	→	666
0₁(1133)	→	1134
0₁(1870)	→	1871
0₁(1933)	→	1934
0₁(647)	→	648
0₁(649)	→	650
0₁(510)	→	511
0₁(411)	→	412
0₁(1205)	→	1206
0₁(1865)	→	1866
0₁(1872)	→	1873
0₁(1757)	→	1758
0₁(670)	→	671
0₁(1560)	→	1561
0₁(718)	→	719
0₁(363)	→	364
0₁(1256)	→	1257
0₁(903)	→	904
0₁(561)	→	562
0₁(1299)	→	1300
0₁(1357)	→	1358
0₁(713)	→	714
0₁(1096)	→	1097
0₁(1358)	→	1359
0₁(613)	→	614
0₁(961)	→	962
0₁(479)	→	480
0₁(336)	→	337
0₁(506)	→	507
0₁(387)	→	388
0₁(607)	→	608
0₁(269)	→	270
0₁(1164)	→	1165
0₁(504)	→	505
0₁(1453)	→	1454
0₁(680)	→	681
0₁(629)	→	630
0₁(454)	→	455
0₁(694)	→	695
0₁(588)	→	589
0₁(356)	→	357
0₁(1558)	→	1559
0₁(1044)	→	1045
0₁(668)	→	669
0₁(477)	→	478
0₁(604)	→	605
0₁(354)	→	355
0₁(14)	→	15
0₁(1450)	→	1451
0₁(679)	→	680
0₁(599)	→	600
0₁(932)	→	933
0₁(563)	→	564
0₁(1761)	→	1762
0₁(658)	→	659
0₁(844)	→	845
0₁(1257)	→	1258
0₁(1333)	→	1334
0₁(262)	→	263
0₁(164)	→	165
0₁(697)	→	698
0₁(975)	→	976
0₁(865)	→	866
0₁(934)	→	935
0₁(361)	→	362
0₁(286)	→	287
0₁(909)	→	910
0₁(389)	→	390
0₁(715)	→	716
0₁(674)	→	675
0₁(284)	→	285
0₁(15)	→	16
0₁(325)	→	326
0₁(963)	→	964
0₁(547)	→	548
0₁(628)	→	629
0₁(672)	→	673
0₁(721)	→	722
0₁(577)	→	578
0₁(496)	→	497
0₁(1008)	→	1009
0₁(719)	→	720
0₁(303)	→	304
0₁(568)	→	569
0₁(259)	→	260
0₁(534)	→	535
0₁(446)	→	447
0₁(630)	→	631
0₁(1128)	→	1129
0₁(352)	→	353
0₁(9)	→	10
0₁(260)	→	261
0₁(162)	→	163
0₁(189)	→	190
0₁(1006)	→	1007
1₂(1572)	→	1573
1₂(1662)	→	1663
1₂(1517)	→	1518
1₂(1562)	→	1563
1₂(889)	→	890
1₂(991)	→	992
1₂(1570)	→	1571
1₂(1634)	→	1635
1₂(1969)	→	1970
1₂(888)	→	889
1₂(738)	→	739
1₂(705)	→	706
1₂(1667)	→	1668
1₂(1965)	→	1966
1₂(1668)	→	1669
1₂(890)	→	891
1₂(1963)	→	1964
1₂(885)	→	886
1₂(1523)	→	1524
2₀(1)	→	1
2₀(6)	→	1
2₀(5)	→	1
2₀(2)	→	1
2₀(3)	→	1
2₀(4)	→	1
2₂(1527)	→	1528
2₂(1565)	→	1566
2₂(1516)	→	1517
2₂(736)	→	737
2₂(709)	→	710
2₂(742)	→	743
2₂(1666)	→	1667
2₂(703)	→	704
2₂(901)	→	902
2₂(1663)	→	1664
2₂(1525)	→	1526
2₂(1961)	→	1962
2₂(993)	→	994
2₂(897)	→	898
2₂(1519)	→	1520
2₂(1563)	→	1564

The automaton is closed under rewriting as it is compatible.