Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4979)

The rewrite relation of the following TRS is considered.

0(0(x1))	→	0(4(4(5(1(1(3(1(2(1(x1))))))))))	(1)
4(0(x1))	→	4(4(2(3(0(2(4(2(3(4(x1))))))))))	(2)
0(0(1(x1)))	→	0(4(1(3(0(2(1(5(0(1(x1))))))))))	(3)
4(0(0(x1)))	→	2(2(2(3(0(0(4(4(2(1(x1))))))))))	(4)
0(0(5(2(x1))))	→	2(3(4(3(0(2(3(0(5(3(x1))))))))))	(5)
1(1(0(0(x1))))	→	1(3(3(3(4(4(3(2(5(0(x1))))))))))	(6)
4(0(0(1(x1))))	→	2(2(2(3(3(0(2(3(5(1(x1))))))))))	(7)
5(0(0(4(x1))))	→	2(5(4(5(2(1(2(3(0(4(x1))))))))))	(8)
5(0(1(5(x1))))	→	3(5(3(4(4(3(2(2(1(5(x1))))))))))	(9)
0(3(3(5(4(x1)))))	→	0(3(3(2(4(3(3(0(3(4(x1))))))))))	(10)
1(0(0(0(0(x1)))))	→	1(2(0(1(0(2(3(2(1(0(x1))))))))))	(11)
1(0(1(0(1(x1)))))	→	3(5(5(4(4(1(3(1(3(2(x1))))))))))	(12)
3(0(0(3(5(x1)))))	→	3(3(3(4(5(2(3(3(2(4(x1))))))))))	(13)
3(0(0(4(0(x1)))))	→	3(3(0(5(5(3(2(2(5(0(x1))))))))))	(14)
4(0(3(4(0(x1)))))	→	2(3(0(3(2(3(5(5(4(0(x1))))))))))	(15)
5(0(0(0(3(x1)))))	→	5(1(4(2(3(0(0(2(1(3(x1))))))))))	(16)
1(2(0(0(1(3(x1))))))	→	0(4(2(5(2(2(3(4(4(3(x1))))))))))	(17)
2(0(0(1(0(0(x1))))))	→	2(4(4(1(0(5(5(2(1(1(x1))))))))))	(18)
2(0(5(5(0(1(x1))))))	→	2(3(1(4(3(1(3(3(5(1(x1))))))))))	(19)
2(4(1(5(1(0(x1))))))	→	1(0(3(1(4(5(0(5(4(4(x1))))))))))	(20)
2(5(5(4(1(0(x1))))))	→	2(5(5(1(1(1(4(2(3(0(x1))))))))))	(21)
3(5(2(5(5(1(x1))))))	→	2(1(3(4(5(1(4(0(4(1(x1))))))))))	(22)
4(1(0(3(4(3(x1))))))	→	4(1(4(5(4(1(2(0(1(3(x1))))))))))	(23)
5(0(0(0(0(0(x1))))))	→	4(5(3(4(0(4(1(4(0(0(x1))))))))))	(24)
0(0(0(0(5(1(0(x1)))))))	→	3(0(5(0(5(5(0(4(0(2(x1))))))))))	(25)
0(3(5(0(0(5(2(x1)))))))	→	2(1(4(4(3(2(5(1(4(3(x1))))))))))	(26)
0(4(5(2(5(5(5(x1)))))))	→	0(4(1(4(0(1(3(2(2(3(x1))))))))))	(27)
1(0(1(4(3(5(5(x1)))))))	→	3(3(0(3(5(4(3(4(0(1(x1))))))))))	(28)
1(5(1(0(0(4(3(x1)))))))	→	4(4(1(1(4(0(4(3(0(3(x1))))))))))	(29)
2(0(0(4(5(1(3(x1)))))))	→	1(0(2(1(4(3(0(4(4(2(x1))))))))))	(30)
3(0(0(5(5(1(3(x1)))))))	→	2(4(5(2(4(4(2(0(0(3(x1))))))))))	(31)
4(0(0(4(0(3(4(x1)))))))	→	3(3(3(3(0(1(5(4(0(4(x1))))))))))	(32)
4(2(4(0(0(1(5(x1)))))))	→	2(3(4(1(3(0(1(2(3(2(x1))))))))))	(33)
4(3(0(4(0(3(4(x1)))))))	→	4(2(4(2(4(4(0(3(0(4(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 3. This is shown by the following automaton.

final states:

{7}

transitions:

78	→	732
1659	→	318
1693	→	398
221	→	1052
221	→	1213
221	→	1385
221	→	1389
221	→	1408
1627	→	207
494	→	780
733	→	48
61	→	7
61	→	254
61	→	106
61	→	170
61	→	31
61	→	206
61	→	205
61	→	305
61	→	306
61	→	77
61	→	307
61	→	120
61	→	78
61	→	375
61	→	318
61	→	152
61	→	367
61	→	227
61	→	213
61	→	342
61	→	67
61	→	368
61	→	376
61	→	553
61	→	538
61	→	683
61	→	1693
61	→	1687
61	→	248
61	→	102
61	→	1593
102	→	248
32	→	130
731	→	372
29	→	7
29	→	142
29	→	276
29	→	77
29	→	306
29	→	368
29	→	284
29	→	100
29	→	45
29	→	235
29	→	20
29	→	107
29	→	493
29	→	286
1579	→	1785
1394	→	375
128	→	1393
1257	→	1444
1257	→	1457
1257	→	1474
1257	→	1521
1257	→	1658
1496	→	538
860	→	1579
152	→	318
152	→	375
1109	→	1684
214	→	297
1475	→	1717
1653	→	308
1691	→	375
487	→	20
1733	→	1798
432	→	824
1578	→	67
1237	→	1433
1409	→	152
374	→	38
1473	→	828
1782	→	375
129	→	7
129	→	120
129	→	47
129	→	78
129	→	284
129	→	100
129	→	143
129	→	45
129	→	235
129	→	20
129	→	67
129	→	305
129	→	205
129	→	306
129	→	142
129	→	276
129	→	77
129	→	307
129	→	254
129	→	106
129	→	170
129	→	31
129	→	206
129	→	493
129	→	553
129	→	538
326	→	128
1784	→	375
1498	→	1729
1593	→	102
1386	→	342
84	→	1391
136	→	1680
1273	→	152
1273	→	151
1273	→	76
1273	→	30
1273	→	19
1273	→	66
1273	→	119
1273	→	7
1273	→	171
1273	→	1687
1107	→	1668
502	→	306
502	→	397
1625	→	170
547	→	206
547	→	553
547	→	307
1395	→	1461
643	→	31
1577	→	1781
120	→	1592
39	→	1602
184	→	177
1483	→	537
333	→	291
382	→	261
1033	→	1688
1324	→	1519
1062	→	47
626	→	421
1710	→	1603
1258	→	284
1258	→	100
1258	→	7
1258	→	45
1258	→	235
1258	→	20
1258	→	493
564	→	1727
1325	→	1308
861	→	205
861	→	305
861	→	306
861	→	19
861	→	66
861	→	119
861	→	151
861	→	76
861	→	30
861	→	7
861	→	77
108	→	419
1340	→	1537
1714	→	170
1629	→	230
1567	→	1783
1681	→	375
692	→	320
55	→	503
255	→	1628
243	→	60
1110	→	284
1110	→	100
1110	→	143
1110	→	151
1110	→	76
1110	→	30
1110	→	19
1110	→	66
1110	→	119
1110	→	7
1110	→	45
1110	→	235
1110	→	20
1110	→	493
20	→	45
20	→	100
20	→	235
20	→	284
304	→	39
107	→	403
31	→	106
31	→	170
31	→	254
31	→	1626
1601	→	1053
1599	→	1013
1034	→	120
1034	→	7
1034	→	78
40	→	7
40	→	170
40	→	31
40	→	285
40	→	120
40	→	78
40	→	20
40	→	121
40	→	327
40	→	228
40	→	538
40	→	48
40	→	733
40	→	493
40	→	617
40	→	1054
40	→	1675
1726	→	171
826	→	1463
1443	→	1239
1730	→	1718
654	→	287
305	→	552
1687	→	375
1022	→	78
1022	→	47
977	→	120
977	→	151
977	→	76
977	→	30
977	→	19
977	→	66
977	→	119
977	→	7
127	→	1194
222	→	7
101	→	151
101	→	76
101	→	30
101	→	19
101	→	66
101	→	119
101	→	7
101	→	78
1507	→	1250
60	→	851
1645	→	277
1661	→	318
677	→	404
402	→	242
761	→	500
1522	→	31
1547	→	1342
536	→	397
573	→	170
573	→	31
573	→	538
573	→	206
573	→	404
573	→	307
573	→	553
573	→	287
261	→	1263
261	→	1339
261	→	1446
261	→	1497
76	→	492
76	→	537
86	→	7
86	→	284
86	→	100
86	→	236
86	→	45
86	→	235
86	→	20
86	→	143
86	→	152
86	→	171
86	→	493
86	→	1673
86	→	1687
86	→	1693
253	→	74
1348	→	1690
79	→	179
309	→	693
1669	→	45
562	→	307
21	→	53
21	→	1027
21	→	1237
21	→	1614
1214	→	1195
1214	→	1324
1564	→	754
150	→	85
178	→	128
346	→	593
976	→	1567
788	→	307
277	→	1674
1685	→	375
1256	→	1598
404	→	1646
1032	→	1624
1667	→	342
153	→	413
1456	→	396
1456	→	1396
1351	→	1340
52	→	27
75	→	60
105	→	57
292	→	60
283	→	113
368	→	396
67	→	213
67	→	227
67	→	342
67	→	367
67	→	151
67	→	76
67	→	30
67	→	19
67	→	66
67	→	119
67	→	7
67	→	277
538	→	31
538	→	285
538	→	628
538	→	1623
485	→	217
1242	→	85
1647	→	288
313	→	39
28	→	430
28	→	486
28	→	563
28	→	642
28	→	1350
1392	→	375
212	→	74
1635	→	254
1621	→	170
1786	→	375
501	→	1525
419	→	616
425	→	39
440	→	142
440	→	276
440	→	77
440	→	349
440	→	306
440	→	46
440	→	397
440	→	396
440	→	368
45	→	627
754	→	961
1108	→	1620
281	→	1731
318	→	682
66	→	1686
1390	→	45
106	→	667
114	→	60
348	→	51
306	→	1692
85	→	753
85	→	1100
85	→	1249
85	→	1395
1201	→	177
1458	→	20
77	→	142
77	→	205
77	→	276
77	→	305
1315	→	367
1315	→	227
1315	→	7
1315	→	213
1315	→	342
1315	→	67
1315	→	248
1315	→	102
1315	→	1593
100	→	1600
100	→	1622
100	→	1666
100	→	1672
100	→	1694
1455	→	1707
1432	→	784
282	→	1306
1526	→	553
1623	→	170
7	→	19
7	→	30
7	→	66
7	→	76
7	→	119
7	→	151
1712	→	130
370	→	721
234	→	27
137	→	28
1307	→	1508
46	→	349
46	→	1650
1675	→	370
1305	→	277
637	→	350
1396	→	396
1384	→	327
1314	→	1577
158	→	1387
278	→	971
1272	→	1563
1272	→	1616
1272	→	1644
1349	→	305
1349	→	205
1349	→	306
1349	→	151
1349	→	76
1349	→	30
1349	→	19
1349	→	66
1349	→	119
1349	→	7
1349	→	142
1349	→	276
1349	→	77
159	→	127
206	→	1652
703	→	311
832	→	206
832	→	553
832	→	307
832	→	350
215	→	475
974	→	1709
285	→	644
1695	→	152
1708	→	431
1445	→	431
1271	→	1634
1271	→	1660
782	→	1422
1741	→	248
1741	→	102
1741	→	1593
1651	→	299
1520	→	1509
852	→	1383
367	→	526
1518	→	1309
418	→	73
1388	→	45
1568	→	67
354	→	183
1558	→	553
603	→	51
603	→	348
27	→	1012
1689	→	375
1615	→	145
966	→	784
439	→	1459
439	→	1495
439	→	1548
975	→	1711
975	→	1713
1580	→	67
262	→	85
262	→	1304
1617	→	152
1460	→	493
228	→	327
1462	→	431
408	→	176
1611	→	439
1673	→	45
1808	→	1735
513	→	57
1728	→	1718
3₁(57)	→	58
3₁(1031)	→	1032
3₁(260)	→	261
3₁(126)	→	127
3₁(123)	→	124
3₁(36)	→	37
3₁(350)	→	351
3₁(1197)	→	1198
3₁(82)	→	83
3₁(210)	→	211
3₁(74)	→	75
3₁(1579)	→	1580
3₁(104)	→	105
3₁(1348)	→	1349
3₁(1567)	→	1568
3₁(208)	→	209
3₁(344)	→	345
3₁(1251)	→	1252
3₁(851)	→	852
3₁(1644)	→	1645
3₁(22)	→	23
3₁(290)	→	291
3₁(1304)	→	1305
3₁(1312)	→	1313
3₁(859)	→	860
3₁(79)	→	80
3₁(1577)	→	1578
3₁(1592)	→	1593
3₁(1614)	→	1615
3₁(136)	→	137
3₁(248)	→	249
3₁(407)	→	408
3₁(1628)	→	1629
3₁(1103)	→	1104
3₁(1033)	→	1034
3₁(154)	→	155
3₁(854)	→	855
3₁(101)	→	102
3₁(107)	→	108
3₁(1270)	→	1271
3₁(66)	→	67
3₁(857)	→	858
3₁(378)	→	379
3₁(276)	→	277
3₁(1711)	→	1712
3₁(1196)	→	1197
3₁(1101)	→	1102
3₁(1385)	→	1386
3₁(1666)	→	1667
3₁(144)	→	145
3₁(172)	→	173
3₁(180)	→	181
3₁(311)	→	312
3₁(1028)	→	1029
3₁(50)	→	51
3₁(131)	→	132
3₁(176)	→	177
3₁(177)	→	178
3₁(135)	→	136
3₁(128)	→	129
3₁(1109)	→	1110
3₁(330)	→	331
3₁(250)	→	251
3₁(84)	→	85
3₁(171)	→	172
3₁(416)	→	417
3₁(31)	→	32
3₁(1239)	→	1240
3₁(353)	→	354
3₁(368)	→	369
3₁(217)	→	218
3₁(132)	→	133
3₁(229)	→	230
3₁(83)	→	84
3₁(152)	→	153
3₁(69)	→	70
3₁(72)	→	73
1₂(479)	→	480
1₂(1735)	→	1736
1₂(1446)	→	1447
1₂(756)	→	757
1₂(492)	→	493
1₂(434)	→	435
1₂(1450)	→	1451
1₂(1053)	→	1054
1₂(1739)	→	1740
1₂(528)	→	529
1₂(1435)	→	1436
1₂(507)	→	508
1₂(1731)	→	1732
1₂(1433)	→	1434
1₂(503)	→	504
1₂(494)	→	495
1₂(1437)	→	1438
1₂(1461)	→	1462
1₂(480)	→	481
1₂(430)	→	431
1₂(505)	→	506
1₂(508)	→	509
1₂(1448)	→	1449
1₂(1459)	→	1460
1₂(496)	→	497
1₂(1451)	→	1452
1₂(1444)	→	1445
1₂(530)	→	531
1₂(526)	→	527
1₂(435)	→	436
1₂(760)	→	761
1₂(753)	→	754
1₂(1725)	→	1726
1₂(477)	→	478
1₂(1016)	→	1017
1₂(1438)	→	1439
1₂(531)	→	532
1₂(1563)	→	1564
1₂(432)	→	433
1₂(475)	→	476
1₂(1722)	→	1723
1₂(497)	→	498
1₂(1707)	→	1708
3₂(699)	→	700
3₂(759)	→	760
3₂(569)	→	570
3₂(965)	→	966
3₂(962)	→	963
3₂(673)	→	674
3₂(1014)	→	1015
3₂(1605)	→	1606
3₂(1503)	→	1504
3₂(1610)	→	1611
3₂(683)	→	684
3₂(617)	→	618
3₂(1538)	→	1539
3₂(538)	→	539
3₂(529)	→	530
3₂(828)	→	829
3₂(668)	→	669
3₂(1498)	→	1499
3₂(478)	→	479
3₂(594)	→	595
3₂(1449)	→	1450
3₂(495)	→	496
3₂(1606)	→	1607
3₂(553)	→	554
3₂(1059)	→	1060
3₂(628)	→	629
3₂(1436)	→	1437
3₂(1543)	→	1544
3₂(722)	→	723
3₂(1609)	→	1610
3₂(650)	→	651
3₂(1514)	→	1515
3₂(1738)	→	1739
3₂(688)	→	689
3₂(1480)	→	1481
3₂(558)	→	559
3₂(1723)	→	1724
3₂(1475)	→	1476
3₂(543)	→	544
3₂(564)	→	565
3₂(633)	→	634
3₂(1056)	→	1057
3₂(1509)	→	1510
3₂(694)	→	695
3₂(727)	→	728
3₂(784)	→	785
3₂(599)	→	600
3₂(645)	→	646
3₂(1061)	→	1062
3₂(506)	→	507
3₂(622)	→	623
3₂(1603)	→	1604
3₂(433)	→	434
5₂(436)	→	437
5₂(1020)	→	1021
5₂(1736)	→	1737
5₂(961)	→	962
5₂(481)	→	482
5₂(1052)	→	1053
5₂(1452)	→	1453
5₂(1018)	→	1019
5₂(1720)	→	1721
5₂(1439)	→	1440
5₂(1718)	→	1719
5₂(498)	→	499
5₂(509)	→	510
5₂(755)	→	756
5₂(532)	→	533
5₂(1060)	→	1061
5₂(1600)	→	1601
0₃(1472)	→	1473
0₃(1803)	→	1804
0₃(1431)	→	1432
0₃(1553)	→	1554
5₁(282)	→	283
5₁(322)	→	323
5₁(1344)	→	1345
5₁(221)	→	222
5₁(113)	→	114
5₁(1107)	→	1108
5₁(255)	→	256
5₁(158)	→	159
5₁(401)	→	402
5₁(1310)	→	1311
5₁(174)	→	175
5₁(1267)	→	1268
5₁(207)	→	208
5₁(1626)	→	1627
5₁(352)	→	353
5₁(1343)	→	1344
5₁(312)	→	313
5₁(404)	→	405
5₁(1265)	→	1266
5₁(257)	→	258
5₁(232)	→	233
5₁(67)	→	68
5₁(973)	→	974
5₁(46)	→	47
5₁(119)	→	120
5₁(77)	→	78
5₁(1032)	→	1033
5₁(321)	→	322
5₁(237)	→	238
5₁(127)	→	128
5₁(975)	→	976
5₁(182)	→	183
5₁(206)	→	207
5₁(25)	→	26
5₁(238)	→	239
5₁(1108)	→	1109
5₁(328)	→	329
5₁(1346)	→	1347
5₁(1199)	→	1200
5₁(111)	→	112
5₁(324)	→	325
5₁(852)	→	853
5₁(301)	→	302
5₁(1254)	→	1255
5₁(100)	→	101
5₁(288)	→	289
5₁(181)	→	182
3₀(7)	→	7
3₃(1549)	→	1550
3₃(1799)	→	1800
3₃(1554)	→	1555
3₃(1804)	→	1805
3₃(1425)	→	1426
3₃(1466)	→	1467
5₃(1428)	→	1429
5₃(1469)	→	1470
2₀(7)	→	7
0₂(758)	→	759
0₂(1542)	→	1543
0₂(1013)	→	1014
0₂(964)	→	965
0₂(501)	→	502
0₂(687)	→	688
0₂(542)	→	543
0₂(1733)	→	1734
0₂(598)	→	599
0₂(782)	→	783
0₂(754)	→	755
0₂(632)	→	633
0₂(1455)	→	1456
0₂(1479)	→	1480
0₂(783)	→	784
0₂(1502)	→	1503
0₂(726)	→	727
0₂(827)	→	828
0₂(1724)	→	1725
0₂(1442)	→	1443
0₂(557)	→	558
0₂(484)	→	485
0₂(1513)	→	1514
0₂(698)	→	699
0₂(1719)	→	1720
0₂(649)	→	650
0₂(568)	→	569
0₂(439)	→	440
0₂(672)	→	673
0₂(1604)	→	1605
0₂(535)	→	536
0₂(621)	→	622
0₂(512)	→	513
0₂(826)	→	827
2₃(1550)	→	1551
2₃(1464)	→	1465
2₃(1423)	→	1424
2₃(1800)	→	1801
2₃(1802)	→	1803
2₃(1552)	→	1553
2₃(1555)	→	1556
2₃(1805)	→	1806
1₀(7)	→	7
4₁(125)	→	126
4₁(286)	→	287
4₁(423)	→	424
4₁(1030)	→	1031
4₁(112)	→	113
4₁(399)	→	400
4₁(1622)	→	1623
4₁(375)	→	376
4₁(1620)	→	1621
4₁(1713)	→	1714
4₁(227)	→	228
4₁(278)	→	279
4₁(1200)	→	1201
4₁(974)	→	975
4₁(349)	→	350
4₁(1256)	→	1257
4₁(53)	→	54
4₁(124)	→	125
4₁(26)	→	27
4₁(369)	→	370
4₁(27)	→	28
4₁(1306)	→	1307
4₁(1241)	→	1242
4₁(242)	→	243
4₁(1268)	→	1269
4₁(1311)	→	1312
4₁(241)	→	242
4₁(157)	→	158
4₁(54)	→	55
4₁(351)	→	352
4₁(284)	→	285
4₁(1624)	→	1625
4₁(376)	→	377
4₁(39)	→	40
4₁(1674)	→	1675
4₁(403)	→	404
4₁(858)	→	859
4₁(420)	→	421
4₁(156)	→	157
4₁(251)	→	252
4₁(289)	→	290
4₁(1308)	→	1309
4₁(1213)	→	1214
4₁(347)	→	348
4₁(319)	→	320
4₁(1029)	→	1030
4₁(1264)	→	1265
4₁(1250)	→	1251
4₁(80)	→	81
4₁(30)	→	31
4₁(1263)	→	1264
4₁(306)	→	307
4₁(133)	→	134
4₁(308)	→	309
4₁(81)	→	82
4₁(219)	→	220
4₁(302)	→	303
4₁(310)	→	311
4₁(1249)	→	1250
4₁(379)	→	380
4₁(1341)	→	1342
4₁(175)	→	176
4₁(254)	→	255
4₁(1634)	→	1635
4₁(1383)	→	1384
4₁(38)	→	39
4₁(300)	→	301
4₁(331)	→	332
4₁(642)	→	643
4₁(332)	→	333
4₁(205)	→	206
4₁(33)	→	34
4₁(228)	→	229
4₁(1194)	→	1195
4₁(398)	→	399
4₁(1521)	→	1522
4₁(73)	→	74
4₁(1106)	→	1107
4₁(258)	→	259
4₁(371)	→	372
4₁(421)	→	422
4₁(1105)	→	1106
2₁(1339)	→	1340
2₁(179)	→	180
2₁(70)	→	71
2₁(59)	→	60
2₁(1781)	→	1782
2₁(121)	→	122
2₁(236)	→	237
2₁(48)	→	49
2₁(1100)	→	1101
2₁(860)	→	861
2₁(60)	→	61
2₁(230)	→	231
2₁(1252)	→	1253
2₁(20)	→	21
2₁(233)	→	234
2₁(1393)	→	1394
2₁(1314)	→	1315
2₁(1684)	→	1685
2₁(972)	→	973
2₁(342)	→	343
2₁(413)	→	414
2₁(34)	→	35
2₁(381)	→	382
2₁(32)	→	33
2₁(1692)	→	1693
2₁(277)	→	278
2₁(173)	→	174
2₁(214)	→	215
2₁(1240)	→	1241
2₁(145)	→	146
2₁(1690)	→	1691
2₁(1680)	→	1681
2₁(1650)	→	1651
2₁(1694)	→	1695
2₁(151)	→	152
2₁(1391)	→	1392
2₁(1255)	→	1256
2₁(218)	→	219
2₁(1783)	→	1784
2₁(855)	→	856
2₁(1408)	→	1409
2₁(1785)	→	1786
2₁(422)	→	423
2₁(1198)	→	1199
2₁(170)	→	171
2₁(231)	→	232
2₁(1660)	→	1661
2₁(37)	→	38
2₁(143)	→	144
2₁(298)	→	299
2₁(122)	→	123
2₁(58)	→	59
2₁(343)	→	344
2₁(1350)	→	1351
2₁(149)	→	150
2₁(1658)	→	1659
2₁(78)	→	79
2₁(108)	→	109
2₁(1686)	→	1687
2₁(424)	→	425
2₁(110)	→	111
2₁(1616)	→	1617
2₁(1688)	→	1689
2₁(134)	→	135
2₁(1253)	→	1254
2₁(1195)	→	1196
2₁(400)	→	401
2₁(102)	→	103
2₁(329)	→	330
2₁(976)	→	977
2₁(209)	→	210
2₁(397)	→	398
2₁(1027)	→	1028
4₀(7)	→	7
5₀(7)	→	7
1₁(732)	→	733
1₁(414)	→	415
1₁(1652)	→	1653
1₁(345)	→	346
1₁(279)	→	280
1₁(47)	→	48
1₁(373)	→	374
1₁(372)	→	373
1₁(23)	→	24
1₁(24)	→	25
1₁(1387)	→	1388
1₁(281)	→	282
1₁(109)	→	110
1₁(220)	→	221
1₁(153)	→	154
1₁(235)	→	236
1₁(85)	→	86
1₁(142)	→	143
1₁(971)	→	972
1₁(249)	→	250
1₁(21)	→	22
1₁(213)	→	214
1₁(1646)	→	1647
1₁(147)	→	148
1₁(280)	→	281
1₁(1672)	→	1673
1₁(1272)	→	1273
1₁(1102)	→	1103
1₁(252)	→	253
1₁(155)	→	156
1₁(299)	→	300
1₁(1457)	→	1458
1₁(240)	→	241
1₁(380)	→	381
1₁(1269)	→	1270
1₁(1389)	→	1390
1₁(303)	→	304
1₁(327)	→	328
1₁(1309)	→	1310
1₁(1668)	→	1669
1₁(19)	→	20
1₁(417)	→	418
1₁(51)	→	52
1₁(287)	→	288
1₁(1104)	→	1105
1₁(405)	→	406
1₁(259)	→	260
1₁(120)	→	121
1₁(291)	→	292
1₁(486)	→	487
1₁(1313)	→	1314
1₁(307)	→	308
4₃(1470)	→	1471
4₃(1557)	→	1558
4₃(1430)	→	1431
4₃(1548)	→	1549
4₃(1806)	→	1807
4₃(1471)	→	1472
4₃(1429)	→	1430
4₃(1798)	→	1799
4₃(1551)	→	1552
4₃(1807)	→	1808
4₃(1801)	→	1802
4₃(1556)	→	1557
0₁(1324)	→	1325
0₁(1347)	→	1348
0₁(1395)	→	1396
0₁(1237)	→	1238
0₁(285)	→	286
0₁(318)	→	319
0₁(305)	→	306
0₁(261)	→	262
0₁(211)	→	212
0₁(103)	→	104
0₁(1266)	→	1267
0₁(320)	→	321
0₁(215)	→	216
0₁(367)	→	368
0₁(183)	→	184
0₁(419)	→	420
0₁(1307)	→	1308
0₁(415)	→	416
0₁(55)	→	56
0₁(856)	→	857
0₁(45)	→	46
0₁(216)	→	217
0₁(1345)	→	1346
0₁(106)	→	107
0₁(406)	→	407
0₁(1271)	→	1272
0₁(1342)	→	1343
0₁(56)	→	57
0₁(28)	→	29
0₁(76)	→	77
0₁(1238)	→	1239
0₁(1340)	→	1341
0₁(68)	→	69
0₁(309)	→	310
0₁(1257)	→	1258
0₁(130)	→	131
0₁(256)	→	257
0₁(297)	→	298
0₁(146)	→	147
0₁(35)	→	36
0₁(325)	→	326
0₁(346)	→	347
0₁(148)	→	149
0₁(49)	→	50
0₁(396)	→	397
0₁(853)	→	854
0₁(323)	→	324
0₁(370)	→	371
0₁(71)	→	72
0₁(239)	→	240
0₁(377)	→	378
2₂(1515)	→	1516
2₂(1512)	→	1513
2₂(686)	→	687
2₂(527)	→	528
2₂(1504)	→	1505
2₂(431)	→	432
2₂(618)	→	619
2₂(700)	→	701
2₂(786)	→	787
2₂(1499)	→	1500
2₂(631)	→	632
2₂(725)	→	726
2₂(757)	→	758
2₂(554)	→	555
2₂(570)	→	571
2₂(646)	→	647
2₂(595)	→	596
2₂(648)	→	649
2₂(1447)	→	1448
2₂(674)	→	675
2₂(620)	→	621
2₂(723)	→	724
2₂(1541)	→	1542
2₂(1021)	→	1022
2₂(785)	→	786
2₂(669)	→	670
2₂(830)	→	831
2₂(1501)	→	1502
2₂(539)	→	540
2₂(634)	→	635
2₂(1017)	→	1018
2₂(684)	→	685
2₂(689)	→	690
2₂(559)	→	560
2₂(1740)	→	1741
2₂(1476)	→	1477
2₂(493)	→	494
2₂(504)	→	505
2₂(1510)	→	1511
2₂(1608)	→	1609
2₂(1481)	→	1482
2₂(1544)	→	1545
2₂(597)	→	598
2₂(829)	→	830
2₂(1478)	→	1479
2₂(541)	→	542
2₂(697)	→	698
2₂(567)	→	568
2₂(476)	→	477
2₂(1054)	→	1055
2₂(600)	→	601
2₂(565)	→	566
2₂(1539)	→	1540
2₂(695)	→	696
2₂(728)	→	729
2₂(963)	→	964
2₂(556)	→	557
2₂(1055)	→	1056
2₂(1434)	→	1435
2₂(1015)	→	1016
2₂(623)	→	624
2₂(651)	→	652
2₂(831)	→	832
2₂(544)	→	545
2₂(671)	→	672
2₂(787)	→	788
2₂(629)	→	630
1₃(1463)	→	1464
1₃(1426)	→	1427
1₃(1465)	→	1466
1₃(1427)	→	1428
1₃(1424)	→	1425
1₃(1467)	→	1468
1₃(1422)	→	1423
1₃(1468)	→	1469
0₀(7)	→	7
4₂(652)	→	653
4₂(546)	→	547
4₂(438)	→	439
4₂(1729)	→	1730
4₂(1440)	→	1441
4₂(563)	→	564
4₂(636)	→	637
4₂(534)	→	535
4₂(1058)	→	1059
4₂(1537)	→	1538
4₂(593)	→	594
4₂(724)	→	725
4₂(1482)	→	1483
4₂(780)	→	781
4₂(729)	→	730
4₂(702)	→	703
4₂(1516)	→	1517
4₂(571)	→	572
4₂(625)	→	626
4₂(533)	→	534
4₂(1057)	→	1058
4₂(721)	→	722
4₂(1508)	→	1509
4₂(1505)	→	1506
4₂(1441)	→	1442
4₂(1454)	→	1455
4₂(545)	→	546
4₂(1506)	→	1507
4₂(602)	→	603
4₂(825)	→	826
4₂(624)	→	625
4₂(1602)	→	1603
4₂(693)	→	694
4₂(670)	→	671
4₂(572)	→	573
4₂(1474)	→	1475
4₂(552)	→	553
4₂(511)	→	512
4₂(437)	→	438
4₂(1517)	→	1518
4₂(1737)	→	1738
4₂(667)	→	668
4₂(1721)	→	1722
4₂(1607)	→	1608
4₂(644)	→	645
4₂(685)	→	686
4₂(781)	→	782
4₂(690)	→	691
4₂(540)	→	541
4₂(482)	→	483
4₂(1540)	→	1541
4₂(596)	→	597
4₂(1709)	→	1710
4₂(701)	→	702
4₂(1495)	→	1496
4₂(635)	→	636
4₂(566)	→	567
4₂(1012)	→	1013
4₂(824)	→	825
4₂(1511)	→	1512
4₂(500)	→	501
4₂(1545)	→	1546
4₂(1525)	→	1526
4₂(675)	→	676
4₂(510)	→	511
4₂(1546)	→	1547
4₂(555)	→	556
4₂(676)	→	677
4₂(537)	→	538
4₂(647)	→	648
4₂(616)	→	617
4₂(1500)	→	1501
4₂(499)	→	500
4₂(483)	→	484
4₂(1019)	→	1020
4₂(1732)	→	1733
4₂(561)	→	562
4₂(682)	→	683
4₂(619)	→	620
4₂(560)	→	561
4₂(630)	→	631
4₂(627)	→	628
4₂(696)	→	697
4₂(730)	→	731
4₂(691)	→	692
4₂(1519)	→	1520
4₂(1734)	→	1735
4₂(1717)	→	1718
4₂(1453)	→	1454
4₂(1497)	→	1498
4₂(601)	→	602
4₂(1598)	→	1599
4₂(1477)	→	1478
4₂(1727)	→	1728
4₂(653)	→	654

The automaton is closed under rewriting as it is compatible.