Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4943)

The rewrite relation of the following TRS is considered.

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

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:

503	→	620
1389	→	530
1067	→	523
239	→	191
587	→	575
486	→	1217
1335	→	1551
1335	→	1591
1703	→	856
685	→	909
1513	→	856
589	→	575
1441	→	764
1680	→	1690
1680	→	1696
1680	→	1700
1680	→	1704
750	→	729
1056	→	513
1463	→	9
1697	→	9
658	→	785
658	→	826
658	→	846
1648	→	163
98	→	960
98	→	989
1624	→	638
1624	→	1668
794	→	1629
1630	→	529
1630	→	1647
10	→	466
10	→	720
1163	→	1396
387	→	359
1691	→	764
289	→	259
1379	→	529
537	→	432
1638	→	529
1638	→	1641
432	→	1278
640	→	652
1479	→	9
1409	→	170
1642	→	163
471	→	333
530	→	669
628	→	4
628	→	425
628	→	601
628	→	359
628	→	588
628	→	407
628	→	261
628	→	1616
511	→	4
511	→	755
511	→	407
511	→	684
511	→	425
511	→	261
511	→	574
511	→	1616
659	→	4
659	→	601
659	→	359
659	→	574
659	→	389
122	→	92
461	→	424
461	→	749
668	→	4
668	→	601
668	→	359
668	→	720
668	→	466
668	→	10
668	→	586
668	→	370
668	→	494
1408	→	1438
1408	→	1470
1408	→	1490
1408	→	1512
260	→	512
676	→	667
18	→	1
18	→	327
18	→	520
18	→	241
18	→	630
547	→	3
547	→	473
547	→	572
547	→	9
547	→	90
547	→	482
978	→	961
1141	→	604
1395	→	9
41	→	1635
3	→	89
3	→	160
3	→	200
3	→	310
3	→	369
3	→	464
583	→	5
583	→	610
583	→	259
583	→	309
583	→	702
583	→	311
1411	→	170
499	→	1274
218	→	191
1574	→	990
691	→	432
1628	→	660
1011	→	426
617	→	1557
405	→	359
1294	→	162
1074	→	1621
1074	→	1674
564	→	539
9	→	481
9	→	572
5	→	67
5	→	143
5	→	217
5	→	290
5	→	358
5	→	462
199	→	170
1681	→	170
361	→	1309
241	→	191
1618	→	574
618	→	1238
618	→	1394
618	→	1426
1220	→	639
1636	→	529
1636	→	1643
1275	→	529
90	→	9
90	→	1146
1344	→	1327
99	→	926
99	→	1076
942	→	330
700	→	3
700	→	572
700	→	563
700	→	9
700	→	611
700	→	472
700	→	68
700	→	764
700	→	1469
700	→	1461
1403	→	9
1416	→	1440
1416	→	1476
1416	→	1496
1416	→	1514
631	→	1059
1	→	41
1	→	121
1	→	240
1	→	258
1	→	386
1	→	434
1471	→	9
1308	→	162
1019	→	9
1730	→	611
936	→	328
936	→	638
936	→	162
936	→	730
936	→	92
936	→	122
936	→	1636
840	→	866
840	→	1068
840	→	1219
1656	→	561
549	→	539
667	→	1162
667	→	1240
667	→	1432
1267	→	661
969	→	1579
969	→	1627
101	→	2
101	→	753
101	→	751
101	→	260
101	→	424
101	→	463
1338	→	1328
1387	→	530
1507	→	92
197	→	1372
1173	→	1165
44	→	9
44	→	561
44	→	1038
1312	→	360
480	→	473
1515	→	856
1029	→	1337
609	→	100
970	→	387
970	→	458
970	→	288
970	→	123
970	→	43
970	→	190
970	→	388
970	→	4
970	→	486
761	→	1116
761	→	1326
761	→	1408
1616	→	574
748	→	729
1683	→	424
1676	→	1688
1676	→	1694
1676	→	1698
1676	→	1702
573	→	539
573	→	701
735	→	726
1232	→	1462
1232	→	1484
1232	→	1506
1592	→	538
675	→	1293
269	→	1535
269	→	1589
309	→	259
1669	→	530
1654	→	561
1373	→	529
1622	→	638
170	→	1028
170	→	1124
170	→	1410
1212	→	630
562	→	539
562	→	692
562	→	1066
562	→	1172
161	→	92
201	→	191
268	→	6
268	→	638
268	→	162
268	→	730
268	→	328
268	→	92
268	→	122
268	→	1636
1499	→	92
1127	→	1117
619	→	1
619	→	629
619	→	485
619	→	191
619	→	752
619	→	754
619	→	216
1410	→	1454
1410	→	1478
1410	→	1498
1410	→	1518
1277	→	529
1277	→	1303
1170	→	1617
1170	→	1655
1170	→	1680
702	→	693
1564	→	912
407	→	359
407	→	588
976	→	961
311	→	259
389	→	359
389	→	574
389	→	1010
389	→	1020
1699	→	92
1310	→	687
1084	→	1649
171	→	1
171	→	629
171	→	485
171	→	191
171	→	729
171	→	754
171	→	216
171	→	750
171	→	218
810	→	9
1477	→	9
639	→	941
6	→	8
6	→	91
6	→	238
6	→	308
6	→	404
6	→	423
1075	→	344
519	→	510
726	→	1209
773	→	327
773	→	520
773	→	241
773	→	630
1336	→	572
1336	→	563
1336	→	9
1336	→	3
1336	→	611
1336	→	472
1336	→	68
627	→	1126
627	→	1343
627	→	1416
921	→	730
921	→	638
921	→	162
921	→	328
921	→	92
921	→	122
921	→	1636
345	→	1
345	→	629
345	→	485
345	→	191
345	→	752
345	→	754
345	→	216
1417	→	170
1397	→	720
1302	→	163
1037	→	755
1037	→	407
1037	→	4
1037	→	684
1037	→	425
1037	→	574
1037	→	1616
1092	→	538
1701	→	92
124	→	92
1279	→	529
1279	→	1301
336	→	2
336	→	660
336	→	435
336	→	337
336	→	192
336	→	728
336	→	602
336	→	495
336	→	459
270	→	259
270	→	462
270	→	290
270	→	143
270	→	67
270	→	217
270	→	358
270	→	5
270	→	309
433	→	3
433	→	473
433	→	572
433	→	9
433	→	90
433	→	482
433	→	42
433	→	521
699	→	911
699	→	1091
368	→	4
368	→	387
368	→	486
368	→	405
923	→	912
873	→	100
999	→	486
999	→	601
999	→	359
999	→	387
1036	→	1637
2	→	65
2	→	141
2	→	215
2	→	269
2	→	406
2	→	460
1060	→	525
787	→	1014
11	→	1016
797	→	786
4	→	43
4	→	123
4	→	190
4	→	288
4	→	388
4	→	458
528	→	510
463	→	424
463	→	751
463	→	260
463	→	2
344	→	924
344	→	1087
582	→	922
582	→	1089
1650	→	162
827	→	816
1425	→	424
501	→	170
478	→	168
425	→	684
425	→	755
425	→	897
959	→	338
754	→	729
1015	→	467
66	→	9
66	→	548
359	→	601
1505	→	92
602	→	575
1461	→	764
795	→	327
795	→	520
795	→	241
795	→	1
972	→	961
535	→	1223
1491	→	92
1125	→	1117
1125	→	1311
925	→	912
1536	→	927
581	→	971
581	→	1573
1705	→	856
169	→	763
169	→	809
169	→	839
169	→	855
100	→	796
100	→	815
100	→	848
100	→	1520
1296	→	163
335	→	973
335	→	1571
1455	→	764
1497	→	92
944	→	331
1013	→	428
1013	→	1022
1247	→	1224
1247	→	1380
1021	→	487
370	→	359
370	→	586
1085	→	1623
1085	→	1670
1085	→	1682
1239	→	1224
1239	→	1386
42	→	9
42	→	479
42	→	538
42	→	3
216	→	191
216	→	434
216	→	258
216	→	121
216	→	41
216	→	240
216	→	386
216	→	1
1675	→	9
752	→	729
637	→	367
709	→	699
709	→	1018
856	→	874
847	→	840
1572	→	990
825	→	630
825	→	191
825	→	241
1090	→	1077
531	→	703
17	→	1276
1644	→	163
683	→	667
510	→	1280
727	→	582
164	→	677
1433	→	424
1439	→	764
1439	→	1721
1523	→	856
1017	→	476
424	→	502
424	→	753
68	→	9
68	→	472
68	→	563
462	→	1460
462	→	1468
462	→	1504
462	→	1522
762	→	582
762	→	1211
267	→	977
1153	→	613
215	→	1615
215	→	1653
215	→	1676
492	→	198
974	→	961
1419	→	424
1469	→	9
865	→	260
1677	→	170
1695	→	9
142	→	92
482	→	473
1058	→	514
1281	→	529
1281	→	1295
465	→	424
465	→	747
465	→	1055
465	→	1152
259	→	493
259	→	610
92	→	162
92	→	529
92	→	638
1210	→	630
575	→	1012
1171	→	425
1171	→	601
1171	→	359
1171	→	458
1171	→	288
1171	→	123
1171	→	43
1171	→	190
1171	→	388
1171	→	4
1171	→	588
1171	→	407
1171	→	261
1171	→	1616
1233	→	601
1233	→	359
1233	→	458
1233	→	288
1233	→	123
1233	→	43
1233	→	190
1233	→	388
1233	→	4
1233	→	574
1233	→	389
910	→	263
367	→	975
367	→	1268
546	→	1246
546	→	1402
546	→	1424
144	→	92
1218	→	632
266	→	1378
266	→	1418
1241	→	1224
1241	→	1388
1269	→	660
680	→	1524
1552	→	912
1558	→	912
1671	→	9
1689	→	764
1023	→	497
1304	→	163
682	→	1563
1521	→	856
1088	→	1077
845	→	580
1590	→	538
1485	→	764
1123	→	334
1580	→	359
644	→	635
191	→	327
191	→	485
191	→	520
191	→	629
1147	→	612
192	→	337
192	→	660
192	→	943
849	→	840
1381	→	530
661	→	1057
661	→	1140
1039	→	1030
291	→	259
459	→	424
459	→	728
459	→	958
459	→	1266
1086	→	473
1086	→	572
1086	→	9
1086	→	464
1086	→	310
1086	→	160
1086	→	89
1086	→	200
1086	→	369
1086	→	3
1086	→	90
1086	→	482
883	→	729
883	→	754
1534	→	753
1534	→	424
1534	→	1433
1534	→	913
1427	→	424
545	→	1307
435	→	424
513	→	603
898	→	194
1519	→	856
2₁(1122)	→	1123
2₁(871)	→	872
2₁(507)	→	508
2₁(1378)	→	1379
2₁(123)	→	124
2₁(1274)	→	1275
2₁(625)	→	626
2₁(1038)	→	1039
2₁(1623)	→	1624
2₁(579)	→	580
2₁(622)	→	623
2₁(657)	→	658
2₁(540)	→	541
2₁(965)	→	966
2₁(527)	→	528
2₁(958)	→	959
2₁(1332)	→	1333
2₁(1165)	→	1166
2₁(1490)	→	1491
2₁(263)	→	264
2₁(1333)	→	1334
2₁(466)	→	467
2₁(141)	→	142
2₁(1311)	→	1312
2₁(1230)	→	1231
2₁(1238)	→	1239
2₁(962)	→	963
2₁(1227)	→	1228
2₁(335)	→	336
2₁(1081)	→	1082
2₁(160)	→	161
2₁(656)	→	657
2₁(360)	→	361
2₁(684)	→	685
2₁(195)	→	196
2₁(848)	→	849
2₁(654)	→	655
2₁(580)	→	581
2₁(327)	→	328
2₁(91)	→	92
2₁(1228)	→	1229
2₁(607)	→	608
2₁(696)	→	697
2₁(167)	→	168
2₁(143)	→	144
2₁(1168)	→	1169
2₁(846)	→	847
2₁(1635)	→	1636
2₁(1498)	→	1499
2₁(513)	→	514
2₁(1152)	→	1153
2₁(1637)	→	1638
2₁(1033)	→	1034
2₁(198)	→	199
2₁(1014)	→	1015
2₁(342)	→	343
2₁(1012)	→	1013
2₁(841)	→	842
2₁(839)	→	840
2₁(497)	→	498
2₁(840)	→	841
2₁(1496)	→	1497
2₁(93)	→	94
2₁(734)	→	735
2₁(581)	→	582
2₁(729)	→	730
2₁(1649)	→	1650
2₁(1331)	→	1332
2₁(1276)	→	1277
2₁(1372)	→	1373
2₁(341)	→	342
2₁(163)	→	164
2₁(427)	→	428
2₁(643)	→	644
2₁(495)	→	496
2₁(503)	→	504
2₁(697)	→	698
2₁(1231)	→	1232
2₁(367)	→	368
2₁(469)	→	470
2₁(758)	→	759
2₁(92)	→	93
2₁(1698)	→	1699
2₁(1293)	→	1294
2₁(686)	→	687
2₁(1246)	→	1247
2₁(1280)	→	1281
2₁(704)	→	705
2₁(695)	→	696
2₁(1621)	→	1622
2₁(1278)	→	1279
2₁(1700)	→	1701
2₁(1504)	→	1505
2₁(723)	→	724
2₁(867)	→	868
2₁(961)	→	962
2₁(1506)	→	1507
2₁(267)	→	268
2₁(98)	→	99
2₁(337)	→	338
2₁(1079)	→	1080
2₁(1057)	→	1058
2₁(1240)	→	1241
2₁(97)	→	98
2₁(334)	→	335
2₁(261)	→	262
2₁(1629)	→	1630
2₁(363)	→	364
2₁(969)	→	970
2₁(612)	→	613
2₁(1223)	→	1224
2₁(685)	→	686
2₁(1307)	→	1308
2₁(542)	→	543
2₁(359)	→	360
2₁(653)	→	654
2₁(121)	→	122
2₁(1029)	→	1030
2₁(663)	→	664
2₁(1309)	→	1310
2₁(491)	→	492
5₂(1728)	→	1729
5₂(1557)	→	1558
5₂(911)	→	912
5₂(924)	→	925
5₂(1729)	→	1730
5₂(863)	→	864
5₂(922)	→	923
5₂(1551)	→	1552
5₂(1724)	→	1725
5₂(993)	→	994
5₂(1723)	→	1724
5₂(992)	→	993
5₂(1535)	→	1536
5₂(926)	→	927
5₂(1563)	→	1564
5₂(1532)	→	1533
5₂(1722)	→	1723
1₂(822)	→	823
1₂(997)	→	998
1₂(770)	→	771
1₂(769)	→	770
1₂(1721)	→	1722
1₂(882)	→	883
1₂(821)	→	822
2₂(916)	→	917
2₂(855)	→	856
2₂(920)	→	921
2₂(1704)	→	1705
2₂(990)	→	991
2₂(856)	→	857
2₂(879)	→	880
2₂(991)	→	992
2₂(1524)	→	1525
2₂(861)	→	862
2₂(875)	→	876
2₂(1525)	→	1526
2₂(857)	→	858
2₂(1526)	→	1527
2₂(1530)	→	1531
2₂(994)	→	995
2₂(1518)	→	1519
2₂(1514)	→	1515
2₂(862)	→	863
2₂(1726)	→	1727
2₂(1520)	→	1521
2₂(931)	→	932
2₂(1702)	→	1703
2₂(1512)	→	1513
2₂(1725)	→	1726
2₂(935)	→	936
2₂(998)	→	999
2₂(1727)	→	1728
2₂(914)	→	915
2₂(1531)	→	1532
2₂(929)	→	930
2₂(1522)	→	1523
0₁(1232)	→	1233
0₁(941)	→	942
0₁(576)	→	577
0₁(870)	→	871
0₁(331)	→	332
0₁(677)	→	678
0₁(467)	→	468
0₁(529)	→	530
0₁(1682)	→	1683
0₁(423)	→	424
0₁(680)	→	681
0₁(842)	→	843
0₁(660)	→	661
0₁(1117)	→	1118
0₁(494)	→	495
0₁(1380)	→	1381
0₁(533)	→	534
0₁(1680)	→	1681
0₁(1388)	→	1389
0₁(11)	→	12
0₁(613)	→	614
0₁(601)	→	602
0₁(1059)	→	1060
0₁(434)	→	435
0₁(468)	→	469
0₁(262)	→	263
0₁(756)	→	757
0₁(721)	→	722
0₁(1432)	→	1433
0₁(1410)	→	1411
0₁(191)	→	192
0₁(426)	→	427
0₁(793)	→	794
0₁(332)	→	333
0₁(169)	→	170
0₁(1119)	→	1120
0₁(1172)	→	1173
0₁(1676)	→	1677
0₁(1627)	→	1628
0₁(690)	→	691
0₁(166)	→	167
0₁(333)	→	334
0₁(1146)	→	1147
0₁(524)	→	525
0₁(621)	→	622
0₁(586)	→	587
0₁(1416)	→	1417
0₁(460)	→	461
0₁(94)	→	95
0₁(966)	→	967
0₁(1386)	→	1387
0₁(12)	→	13
0₁(464)	→	465
0₁(1268)	→	1269
0₁(1426)	→	1427
0₁(259)	→	260
0₁(611)	→	612
0₁(658)	→	659
0₁(1424)	→	1425
0₁(678)	→	679
0₁(488)	→	489
0₁(1668)	→	1669
0₁(1408)	→	1409
0₁(732)	→	733
0₁(574)	→	575
0₁(364)	→	365
0₁(1266)	→	1267
0₁(720)	→	721
0₁(909)	→	910
0₁(343)	→	344
0₁(788)	→	789
0₁(338)	→	339
0₁(462)	→	463
0₁(588)	→	589
0₁(512)	→	513
0₁(1055)	→	1056
0₁(329)	→	330
0₁(671)	→	672
0₁(458)	→	459
0₁(498)	→	499
0₁(1164)	→	1165
0₁(1068)	→	1069
0₁(1418)	→	1419
0₁(666)	→	667
0₁(100)	→	101
0₁(789)	→	790
0₁(1072)	→	1073
0₁(16)	→	17
5₀(3)	→	5
5₀(6)	→	5
5₀(5)	→	5
5₀(4)	→	5
5₀(2)	→	5
5₀(1)	→	5
2₀(2)	→	6
2₀(6)	→	6
2₀(4)	→	6
2₀(1)	→	6
2₀(3)	→	6
2₀(5)	→	6
3₂(859)	→	860
3₂(1571)	→	1572
3₂(989)	→	990
3₂(816)	→	817
3₂(934)	→	935
3₂(880)	→	881
3₂(1528)	→	1529
3₂(928)	→	929
3₂(764)	→	765
3₂(919)	→	920
3₂(765)	→	766
3₂(817)	→	818
3₂(913)	→	914
3₂(1573)	→	1574
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
5₁(699)	→	700
5₁(617)	→	618
5₁(694)	→	695
5₁(1334)	→	1335
5₁(99)	→	100
5₁(582)	→	583
5₁(692)	→	693
5₁(344)	→	345
5₁(1329)	→	1330
5₁(362)	→	363
5₁(689)	→	690
5₁(269)	→	270
5₁(682)	→	683
5₁(616)	→	617
5₁(536)	→	537
5₁(288)	→	289
5₁(964)	→	965
5₁(290)	→	291
5₁(1328)	→	1329
5₁(1335)	→	1336
5₁(701)	→	702
5₁(308)	→	309
5₁(310)	→	311
5₁(963)	→	964
5₁(726)	→	727
5₁(698)	→	699
5₁(361)	→	362
5₁(1330)	→	1331
5₁(693)	→	694
5₁(258)	→	259
1₁(751)	→	752
1₁(1071)	→	1072
1₁(517)	→	518
1₁(572)	→	573
1₁(1219)	→	1220
1₁(366)	→	367
1₁(509)	→	510
1₁(532)	→	533
1₁(629)	→	630
1₁(753)	→	754
1₁(328)	→	329
1₁(577)	→	578
1₁(687)	→	688
1₁(707)	→	708
1₁(200)	→	201
1₁(705)	→	706
1₁(561)	→	562
1₁(490)	→	491
1₁(531)	→	532
1₁(681)	→	682
1₁(728)	→	729
1₁(1166)	→	1167
1₁(1016)	→	1017
1₁(1120)	→	1121
1₁(1169)	→	1170
1₁(792)	→	793
1₁(475)	→	476
1₁(238)	→	239
1₁(429)	→	430
1₁(968)	→	969
1₁(1226)	→	1227
1₁(749)	→	750
1₁(190)	→	191
1₁(217)	→	218
1₁(627)	→	628
1₁(215)	→	216
1₁(634)	→	635
1₁(1070)	→	1071
1₁(755)	→	756
1₁(14)	→	15
1₁(522)	→	523
1₁(470)	→	471
1₁(1163)	→	1164
1₁(1035)	→	1036
1₁(240)	→	241
1₁(725)	→	726
1₁(430)	→	431
1₁(521)	→	522
1₁(1211)	→	1212
1₁(761)	→	762
1₁(170)	→	171
1₁(623)	→	624
1₁(1327)	→	1328
1₁(1209)	→	1210
1₁(620)	→	621
1₁(635)	→	636
1₁(1170)	→	1171
1₁(652)	→	653
1₁(760)	→	761
1₁(1224)	→	1225
1₁(1225)	→	1226
1₁(747)	→	748
1₁(1337)	→	1338
1₁(15)	→	16
1₁(626)	→	627
1₁(1066)	→	1067
1₁(791)	→	792
1₁(516)	→	517
1₁(563)	→	564
1₁(639)	→	640
1₁(638)	→	639
1₁(706)	→	707
1₁(548)	→	549
1₁(1077)	→	1078
1₁(538)	→	539
0₀(3)	→	2
0₀(5)	→	2
0₀(2)	→	2
0₀(4)	→	2
0₀(1)	→	2
0₀(6)	→	2
4₀(2)	→	3
4₀(4)	→	3
4₀(3)	→	3
4₀(6)	→	3
4₀(1)	→	3
4₀(5)	→	3
3₁(534)	→	535
3₁(672)	→	673
3₁(431)	→	432
3₁(266)	→	267
3₁(615)	→	616
3₁(523)	→	524
3₁(670)	→	671
3₁(489)	→	490
3₁(9)	→	10
3₁(731)	→	732
3₁(843)	→	844
3₁(618)	→	619
3₁(543)	→	544
3₁(640)	→	641
3₁(477)	→	478
3₁(1010)	→	1011
3₁(975)	→	976
3₁(1396)	→	1397
3₁(973)	→	974
3₁(1615)	→	1616
3₁(960)	→	961
3₁(632)	→	633
3₁(787)	→	788
3₁(667)	→	668
3₁(1617)	→	1618
3₁(506)	→	507
3₁(473)	→	474
3₁(630)	→	631
3₁(493)	→	494
3₁(369)	→	370
3₁(425)	→	426
3₁(674)	→	675
3₁(733)	→	734
3₁(971)	→	972
3₁(977)	→	978
3₁(578)	→	579
3₁(1083)	→	1084
3₁(1032)	→	1033
3₁(1074)	→	1075
3₁(168)	→	169
3₁(1073)	→	1074
3₁(1140)	→	1141
3₁(404)	→	405
3₁(514)	→	515
3₁(428)	→	429
3₁(358)	→	359
3₁(196)	→	197
3₁(722)	→	723
3₁(406)	→	407
3₁(518)	→	519
3₁(1085)	→	1086
3₁(544)	→	545
3₁(1579)	→	1580
3₁(631)	→	632
3₁(386)	→	387
3₁(485)	→	486
3₁(603)	→	604
3₁(474)	→	475
3₁(388)	→	389
3₁(424)	→	425
3₁(1126)	→	1127
3₁(1082)	→	1083
3₁(1116)	→	1117
3₁(703)	→	704
3₁(1124)	→	1125
3₁(10)	→	11
3₁(515)	→	516
3₁(340)	→	341
3₁(633)	→	634
3₁(757)	→	758
3₁(197)	→	198
3₁(535)	→	536
3₁(95)	→	96
3₁(614)	→	615
3₁(786)	→	787
3₁(664)	→	665
3₁(525)	→	526
3₁(1121)	→	1122
3₁(1217)	→	1218
3₁(642)	→	643
3₁(679)	→	680
3₁(872)	→	873
3₁(260)	→	261
3₁(669)	→	670
3₁(546)	→	547
3₁(192)	→	193
4₁(165)	→	166
4₁(1295)	→	1296
4₁(194)	→	195
4₁(65)	→	66
4₁(662)	→	663
4₁(1089)	→	1090
4₁(505)	→	506
4₁(539)	→	540
4₁(708)	→	709
4₁(41)	→	42
4₁(17)	→	18
4₁(675)	→	676
4₁(499)	→	500
4₁(1018)	→	1019
4₁(1478)	→	1479
4₁(89)	→	90
4₁(665)	→	666
4₁(759)	→	760
4₁(1118)	→	1119
4₁(796)	→	797
4₁(510)	→	511
4₁(486)	→	487
4₁(610)	→	611
4₁(1655)	→	1656
4₁(641)	→	642
4₁(868)	→	869
4₁(1653)	→	1654
4₁(1402)	→	1403
4₁(1022)	→	1023
4₁(1301)	→	1302
4₁(500)	→	501
4₁(1078)	→	1079
4₁(502)	→	503
4₁(943)	→	944
4₁(472)	→	473
4₁(264)	→	265
4₁(1087)	→	1088
4₁(1470)	→	1471
4₁(730)	→	731
4₁(1091)	→	1092
4₁(608)	→	609
4₁(479)	→	480
4₁(1020)	→	1021
4₁(1647)	→	1648
4₁(785)	→	786
4₁(476)	→	477
4₁(13)	→	14
4₁(504)	→	505
4₁(1326)	→	1327
4₁(1229)	→	1230
4₁(1034)	→	1035
4₁(724)	→	725
4₁(575)	→	576
4₁(96)	→	97
4₁(67)	→	68
4₁(526)	→	527
4₁(604)	→	605
4₁(193)	→	194
4₁(688)	→	689
4₁(967)	→	968
4₁(1674)	→	1675
4₁(1076)	→	1077
4₁(1162)	→	1163
4₁(844)	→	845
4₁(866)	→	867
4₁(1641)	→	1642
4₁(1476)	→	1477
4₁(790)	→	791
4₁(869)	→	870
4₁(164)	→	165
4₁(606)	→	607
4₁(661)	→	662
4₁(605)	→	606
4₁(897)	→	898
4₁(365)	→	366
4₁(624)	→	625
4₁(1643)	→	1644
4₁(339)	→	340
4₁(530)	→	531
4₁(1028)	→	1029
4₁(1468)	→	1469
4₁(1462)	→	1463
4₁(520)	→	521
4₁(432)	→	433
4₁(1303)	→	1304
4₁(265)	→	266
4₁(636)	→	637
4₁(1696)	→	1697
4₁(1031)	→	1032
4₁(655)	→	656
4₁(809)	→	810
4₁(1084)	→	1085
4₁(1069)	→	1070
4₁(1080)	→	1081
4₁(1589)	→	1590
4₁(673)	→	674
4₁(1036)	→	1037
4₁(496)	→	497
4₁(330)	→	331
4₁(508)	→	509
4₁(794)	→	795
4₁(541)	→	542
4₁(43)	→	44
4₁(1591)	→	1592
4₁(1394)	→	1395
4₁(487)	→	488
4₁(1670)	→	1671
4₁(1343)	→	1344
4₁(1030)	→	1031
4₁(481)	→	482
4₁(1694)	→	1695
4₁(8)	→	9
4₁(162)	→	163
4₁(545)	→	546
4₁(1167)	→	1168
0₂(881)	→	882
0₂(864)	→	865
0₂(995)	→	996
0₂(819)	→	820
0₂(927)	→	928
0₂(771)	→	772
0₂(915)	→	916
0₂(818)	→	819
0₂(1533)	→	1534
0₂(878)	→	879
0₂(930)	→	931
0₂(823)	→	824
0₂(912)	→	913
0₂(858)	→	859
0₂(1527)	→	1528
0₂(766)	→	767
0₂(767)	→	768
1₀(1)	→	1
1₀(6)	→	1
1₀(5)	→	1
1₀(2)	→	1
1₀(3)	→	1
1₀(4)	→	1
4₂(768)	→	769
4₂(1440)	→	1441
4₂(1529)	→	1530
4₂(1690)	→	1691
4₂(763)	→	764
4₂(918)	→	919
4₂(860)	→	861
4₂(1438)	→	1439
4₂(1454)	→	1455
4₂(877)	→	878
4₂(772)	→	773
4₂(996)	→	997
4₂(874)	→	875
4₂(815)	→	816
4₂(876)	→	877
4₂(824)	→	825
4₂(820)	→	821
4₂(1688)	→	1689
4₂(1484)	→	1485
4₂(932)	→	933
4₂(826)	→	827
4₂(917)	→	918
4₂(933)	→	934
4₂(1460)	→	1461

The automaton is closed under rewriting as it is compatible.