Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/85874)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

3(2(1(0(x1))))	→	2(4(0(x1)))	(31)
5(4(5(0(2(x1)))))	→	5(2(3(0(x1))))	(32)
1(3(2(3(2(1(x1))))))	→	2(0(2(4(2(x1)))))	(33)
2(2(1(2(5(3(x1))))))	→	5(5(5(2(x1))))	(34)
3(1(4(0(1(5(x1))))))	→	0(2(5(4(5(x1)))))	(35)
2(1(0(4(1(3(0(x1)))))))	→	5(1(2(3(0(0(0(x1)))))))	(36)
2(4(4(4(5(5(1(1(x1))))))))	→	5(0(2(3(1(1(0(1(x1))))))))	(37)
5(1(5(3(0(2(0(2(x1))))))))	→	0(1(0(5(0(1(5(2(x1))))))))	(38)
0(1(0(1(3(2(1(5(3(x1)))))))))	→	3(4(2(1(5(3(5(x1)))))))	(39)
5(1(5(1(5(3(5(0(1(1(x1))))))))))	→	3(3(1(1(2(2(0(2(0(5(1(x1)))))))))))	(40)
4(0(5(0(2(4(2(1(2(2(x1))))))))))	→	4(0(5(3(2(3(1(1(2(3(x1))))))))))	(41)
1(4(2(3(1(4(5(0(5(0(1(x1)))))))))))	→	5(0(3(5(4(3(4(5(3(x1)))))))))	(42)
5(3(0(1(5(1(2(2(1(1(1(0(x1))))))))))))	→	0(2(1(5(1(0(0(3(2(0(1(0(0(x1)))))))))))))	(43)
3(4(0(4(2(3(3(5(3(4(5(2(x1))))))))))))	→	5(2(4(0(4(5(0(1(3(2(3(5(x1))))))))))))	(44)
5(1(3(4(2(5(2(0(5(1(3(3(x1))))))))))))	→	0(0(0(0(1(0(5(1(2(4(4(0(0(5(x1))))))))))))))	(45)
3(5(3(3(4(4(3(2(5(0(2(2(5(1(x1))))))))))))))	→	0(4(4(5(4(3(2(1(3(0(1(2(5(2(x1))))))))))))))	(46)
3(2(3(3(2(4(5(3(2(0(3(3(2(3(x1))))))))))))))	→	0(0(1(0(4(2(5(3(5(5(3(5(5(x1)))))))))))))	(47)
0(2(0(0(3(5(5(1(1(5(2(3(4(3(x1))))))))))))))	→	2(4(2(1(5(4(4(0(0(3(1(0(1(4(x1))))))))))))))	(48)
3(1(0(1(5(3(1(2(5(2(3(0(1(0(2(x1)))))))))))))))	→	2(3(0(2(3(1(3(1(3(2(3(5(0(0(x1))))))))))))))	(49)
5(4(4(4(1(5(3(4(2(3(5(0(2(5(2(0(x1))))))))))))))))	→	5(2(2(5(4(1(3(2(3(1(4(4(5(4(4(2(x1))))))))))))))))	(50)
4(5(5(0(1(2(0(3(4(1(1(4(3(5(3(2(0(x1)))))))))))))))))	→	4(1(0(0(5(5(0(0(1(5(3(4(5(4(5(0(x1))))))))))))))))	(51)
3(1(4(1(5(3(0(3(2(1(1(1(1(2(2(4(4(x1)))))))))))))))))	→	3(3(3(5(0(0(3(1(1(2(3(3(0(2(5(4(x1))))))))))))))))	(52)
3(2(5(5(4(3(0(3(1(4(2(4(3(4(5(3(1(3(0(x1)))))))))))))))))))	→	0(2(2(4(2(1(3(3(5(5(4(4(3(3(4(2(3(0(x1))))))))))))))))))	(53)
0(5(3(1(2(3(3(5(0(1(2(4(1(4(0(1(0(3(3(x1)))))))))))))))))))	→	5(2(4(4(0(1(4(3(5(1(5(4(3(1(2(0(3(2(x1))))))))))))))))))	(54)
5(4(3(5(3(1(0(0(5(3(3(4(2(5(3(4(5(3(3(1(x1))))))))))))))))))))	→	5(3(0(5(1(1(1(0(5(0(1(2(5(3(3(5(1(3(4(0(3(x1)))))))))))))))))))))	(55)
5(0(3(4(3(5(2(4(2(5(4(4(0(1(0(5(1(5(0(2(x1))))))))))))))))))))	→	5(5(2(4(4(1(0(4(3(2(0(0(4(5(1(2(2(3(2(x1)))))))))))))))))))	(56)
3(4(5(0(1(5(0(0(3(4(2(3(3(5(1(5(2(4(0(3(x1))))))))))))))))))))	→	0(4(3(4(3(3(1(5(2(4(4(2(4(0(2(4(1(2(3(x1)))))))))))))))))))	(57)
5(1(5(5(5(5(5(4(5(3(4(1(3(1(5(0(1(0(2(3(x1))))))))))))))))))))	→	5(3(5(1(3(1(4(3(1(0(4(4(1(2(5(3(5(4(4(1(3(x1)))))))))))))))))))))	(58)
2(0(5(5(3(2(0(4(3(2(4(4(0(1(1(0(0(1(3(3(x1))))))))))))))))))))	→	2(5(4(2(1(2(3(3(4(2(0(5(5(4(2(2(5(x1)))))))))))))))))	(59)
5(4(4(4(5(1(3(1(1(0(5(3(1(1(5(5(1(5(5(0(3(x1)))))))))))))))))))))	→	0(2(2(4(1(2(1(0(4(0(3(2(3(3(4(1(3(4(2(5(x1))))))))))))))))))))	(60)

1.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:

854	→	738
854	→	809
854	→	490
854	→	459
854	→	691
854	→	602
854	→	384
854	→	95
854	→	48
854	→	263
854	→	469
854	→	1
854	→	709
854	→	801
854	→	474
854	→	713
1198	→	1181
1659	→	479
1206	→	1181
33	→	9
588	→	4
588	→	634
588	→	70
588	→	9
588	→	21
23	→	9
1151	→	343
1151	→	3
1151	→	576
650	→	1606
650	→	1620
1627	→	342
587	→	905
587	→	926
587	→	1120
587	→	1211
733	→	52
200	→	168
200	→	427
200	→	544
457	→	6
457	→	233
457	→	448
633	→	51
454	→	1441
1057	→	1048
1737	→	90
1418	→	1387
732	→	966
732	→	1078
1475	→	1446
229	→	903
229	→	946
229	→	1369
1603	→	50
1603	→	1724
10	→	911
10	→	920
10	→	1111
10	→	1205
1163	→	480
1163	→	832
1163	→	537
1163	→	227
1163	→	595
1163	→	386
1163	→	115
1163	→	34
1163	→	296
1163	→	458
1163	→	6
1163	→	264
1163	→	491
1163	→	1181
1163	→	1200
51	→	1199
1653	→	459
387	→	343
387	→	1504
487	→	3
487	→	343
487	→	576
1248	→	516
1248	→	1529
1546	→	1530
1546	→	1583
851	→	1598
851	→	1614
851	→	1644
851	→	1688
571	→	557
432	→	1359
1717	→	604
1250	→	517
1578	→	811
1479	→	51
1121	→	1112
1473	→	1446
96	→	90
1544	→	1530
1544	→	1581
1593	→	1790
530	→	517
1597	→	50
1597	→	1716
472	→	459
472	→	770
511	→	1180
1273	→	738
1273	→	474
1273	→	1
1273	→	691
1273	→	713
502	→	432
502	→	1046
502	→	1478
1625	→	167
461	→	755
299	→	227
299	→	443
299	→	535
299	→	570
299	→	830
299	→	1058
1584	→	835
491	→	480
927	→	916
705	→	1197
1098	→	1079
1098	→	1251
1098	→	1261
1098	→	1545
227	→	445
227	→	537
227	→	572
227	→	832
978	→	967
978	→	1417
3	→	32
3	→	117
3	→	232
3	→	419
3	→	477
3	→	589
1362	→	90
652	→	809
652	→	490
652	→	459
652	→	602
652	→	384
652	→	95
652	→	48
652	→	263
652	→	469
652	→	1
652	→	799
652	→	478
812	→	834
1254	→	517
460	→	1383
460	→	1474
1789	→	227
1613	→	916
1119	→	230
1258	→	199
347	→	901
347	→	932
919	→	637
1340	→	604
1424	→	1387
9	→	70
9	→	336
9	→	634
914	→	614
914	→	1335
5	→	22
5	→	89
5	→	226
5	→	342
5	→	475
5	→	593
1200	→	1181
1629	→	342
341	→	169
1190	→	1668
592	→	575
592	→	665
1071	→	342
1055	→	1047
456	→	983
456	→	1097
456	→	1317
1681	→	445
1252	→	517
947	→	942
90	→	199
90	→	712
446	→	435
446	→	503
713	→	691
713	→	738
1601	→	50
1601	→	1728
49	→	9
49	→	68
49	→	1152
1599	→	50
1599	→	1730
1162	→	1626
1162	→	1736
1162	→	1764
1403	→	517
1403	→	634
1403	→	70
1403	→	9
1403	→	574
1403	→	421
1403	→	138
1403	→	8
1403	→	265
1403	→	471
1403	→	4
1403	→	50
1403	→	35
1403	→	538
1403	→	942
1403	→	904
1403	→	947
1403	→	1613
1403	→	1607
1403	→	1603
1403	→	1621
1416	→	1386
1	→	48
1	→	95
1	→	263
1	→	384
1	→	469
1	→	602
1791	→	445
826	→	907
826	→	922
826	→	1122
826	→	1213
936	→	675
936	→	666
71	→	51
1687	→	445
833	→	812
1707	→	557
1318	→	1297
1753	→	1387
1052	→	1738
139	→	90
139	→	167
139	→	690
139	→	1496
1645	→	459
689	→	229
590	→	575
426	→	343
1283	→	557
1342	→	604
970	→	712
970	→	710
970	→	90
970	→	591
970	→	425
970	→	140
970	→	20
970	→	298
970	→	473
970	→	2
970	→	197
970	→	141
1607	→	50
1607	→	1714
1522	→	232
769	→	554
1161	→	1596
1161	→	1618
536	→	517
573	→	557
735	→	715
297	→	227
343	→	447
675	→	650
1348	→	604
1643	→	459
1729	→	604
233	→	227
233	→	441
233	→	529
233	→	568
233	→	828
233	→	1060
233	→	6
233	→	448
1669	→	445
91	→	621
91	→	1591
662	→	1247
662	→	1415
1370	→	638
170	→	2
170	→	712
170	→	710
170	→	90
170	→	197
170	→	141
170	→	708
170	→	171
170	→	118
349	→	169
385	→	343
1212	→	1181
1709	→	575
21	→	9
1723	→	604
1277	→	1262
912	→	614
912	→	1349
1214	→	1181
614	→	1284
141	→	90
141	→	197
141	→	710
1528	→	771
976	→	967
976	→	1423
172	→	168
1310	→	634
1310	→	70
1310	→	4
1310	→	9
1310	→	21
788	→	732
1358	→	90
1084	→	1622
1084	→	1634
1084	→	1708
648	→	467
810	→	771
6	→	34
6	→	115
6	→	296
6	→	386
6	→	458
6	→	595
1053	→	233
1053	→	6
1053	→	448
337	→	492
337	→	604
337	→	1042
1256	→	516
1256	→	1549
1336	→	604
116	→	90
116	→	1490
116	→	690
116	→	591
116	→	425
116	→	140
116	→	20
116	→	298
116	→	473
116	→	2
116	→	167
116	→	139
921	→	916
468	→	5
468	→	575
468	→	10
468	→	228
468	→	596
1051	→	1658
1456	→	703
345	→	1525
1763	→	51
52	→	676
52	→	1472
555	→	230
455	→	1255
455	→	1385
431	→	1142
1701	→	517
484	→	1577
1309	→	1604
1309	→	1608
1309	→	1650
1309	→	1680
1364	→	52
230	→	1054
230	→	1361
230	→	1443
433	→	6
433	→	233
433	→	448
433	→	480
433	→	264
433	→	491
433	→	1181
433	→	1200
615	→	10
615	→	1527
1637	→	434
264	→	227
264	→	675
264	→	229
264	→	595
264	→	386
264	→	115
264	→	34
264	→	296
264	→	458
264	→	6
264	→	1687
538	→	517
1192	→	809
1192	→	490
1192	→	714
1192	→	459
1192	→	602
1192	→	384
1192	→	95
1192	→	48
1192	→	263
1192	→	469
1192	→	1
1192	→	479
1192	→	807
1192	→	476
1192	→	1112
831	→	812
906	→	614
906	→	1339
923	→	916
569	→	557
853	→	1600
853	→	1616
853	→	1642
853	→	1686
53	→	6
53	→	832
53	→	537
53	→	637
53	→	675
53	→	229
53	→	445
53	→	572
53	→	227
53	→	266
53	→	635
53	→	233
53	→	1206
53	→	1687
53	→	1689
808	→	771
2	→	20
2	→	140
2	→	298
2	→	425
2	→	473
2	→	591
11	→	1
11	→	738
11	→	809
11	→	490
11	→	459
11	→	691
11	→	709
11	→	801
11	→	474
11	→	713
11	→	799
11	→	478
1679	→	445
4	→	8
4	→	138
4	→	265
4	→	421
4	→	471
4	→	574
528	→	432
118	→	90
118	→	171
118	→	708
344	→	1062
1635	→	434
1635	→	1700
1635	→	1706
1635	→	1770
1621	→	942
1594	→	1788
470	→	459
470	→	488
470	→	734
827	→	2
827	→	712
827	→	690
827	→	90
827	→	167
827	→	139
1779	→	1588
850	→	501
501	→	913
501	→	941
478	→	459
478	→	799
904	→	614
904	→	1333
1550	→	1530
440	→	4
440	→	634
440	→	70
440	→	344
440	→	9
440	→	33
754	→	52
802	→	771
1043	→	339
1059	→	1048
1715	→	604
1063	→	1050
1334	→	604
1094	→	1079
1094	→	1253
1094	→	1276
1094	→	1547
1773	→	811
93	→	909
93	→	915
93	→	1128
93	→	1203
1491	→	755
348	→	1480
800	→	771
1586	→	835
596	→	575
596	→	853
1771	→	812
1497	→	755
1526	→	772
1623	→	167
1623	→	1752
663	→	975
663	→	1093
663	→	1296
1605	→	50
1605	→	1722
1401	→	1678
69	→	51
1085	→	634
1085	→	70
1085	→	344
1085	→	574
1085	→	421
1085	→	138
1085	→	8
1085	→	265
1085	→	471
1085	→	4
1085	→	9
1085	→	33
444	→	435
1204	→	1181
1204	→	1363
1765	→	51
902	→	614
1442	→	714
1316	→	1297
709	→	691
1384	→	677
35	→	9
35	→	50
35	→	1164
1745	→	90
231	→	1
231	→	809
231	→	490
231	→	459
231	→	799
231	→	478
231	→	503
231	→	435
231	→	446
231	→	738
231	→	474
231	→	691
231	→	713
231	→	714
231	→	479
231	→	807
231	→	476
231	→	1653
231	→	1643
115	→	1602
115	→	1612
115	→	1652
115	→	1694
1739	→	90
707	→	4
707	→	517
707	→	634
707	→	70
707	→	9
707	→	50
707	→	35
707	→	538
707	→	942
707	→	904
707	→	947
707	→	1613
707	→	1607
707	→	1603
707	→	1621
908	→	614
908	→	1341
198	→	168
1725	→	604
1272	→	1744
945	→	229
945	→	675
945	→	1687
1609	→	916
651	→	1628
651	→	1746
651	→	1762
1148	→	1772
1129	→	1112
666	→	650
664	→	1
664	→	809
664	→	490
664	→	459
664	→	799
664	→	478
567	→	230
1422	→	1387
1360	→	90
1695	→	445
829	→	812
340	→	1257
1619	→	942
489	→	480
711	→	691
1165	→	1153
422	→	343
92	→	1070
92	→	1357
1285	→	556
1651	→	459
575	→	674
474	→	459
474	→	801
852	→	738
852	→	809
852	→	490
852	→	459
852	→	691
852	→	602
852	→	384
852	→	95
852	→	48
852	→	263
852	→	469
852	→	1
852	→	709
852	→	801
852	→	474
852	→	713
910	→	614
910	→	1347
1050	→	1778
594	→	575
266	→	227
266	→	434
266	→	516
266	→	556
266	→	811
266	→	1056
266	→	6
1481	→	51
476	→	459
476	→	479
476	→	714
476	→	807
603	→	575
603	→	649
603	→	851
603	→	5
603	→	10
1350	→	604
1689	→	445
1615	→	916
442	→	435
1521	→	1624
1521	→	1636
737	→	715
439	→	977
439	→	1095
439	→	1315
984	→	967
984	→	1421
1747	→	90
1590	→	738
1590	→	691
1590	→	713
1123	→	1112
94	→	3
94	→	802
94	→	385
94	→	810
430	→	1587
1061	→	1048
1617	→	916
1096	→	1079
1096	→	1249
1096	→	1282
1096	→	1543
1595	→	53
1542	→	1363
459	→	490
459	→	736
459	→	809
1548	→	1530
1548	→	1585
1731	→	604
513	→	1
513	→	809
513	→	490
513	→	714
513	→	459
513	→	479
513	→	807
513	→	476
513	→	1112
420	→	343
1582	→	835
1₁(693)	→	694
1₁(727)	→	728
1₁(521)	→	522
1₁(625)	→	626
1₁(384)	→	385
1₁(545)	→	546
1₁(799)	→	800
1₁(505)	→	506
1₁(1490)	→	1491
1₁(1047)	→	1048
1₁(749)	→	750
1₁(419)	→	420
1₁(1058)	→	1059
1₁(1540)	→	1541
1₁(344)	→	345
1₁(461)	→	462
1₁(1517)	→	1518
1₁(1389)	→	1390
1₁(1184)	→	1185
1₁(1164)	→	1165
1₁(777)	→	778
1₁(1081)	→	1082
1₁(656)	→	657
1₁(728)	→	729
1₁(498)	→	499
1₁(847)	→	848
1₁(1519)	→	1520
1₁(786)	→	787
1₁(421)	→	422
1₁(822)	→	823
1₁(1455)	→	1456
1₁(836)	→	837
1₁(807)	→	808
1₁(1299)	→	1300
1₁(1114)	→	1115
1₁(740)	→	741
1₁(1113)	→	1114
1₁(1152)	→	1153
1₁(801)	→	802
1₁(1270)	→	1271
1₁(342)	→	343
1₁(647)	→	648
1₁(610)	→	611
1₁(577)	→	578
1₁(1393)	→	1394
1₁(340)	→	341
1₁(1496)	→	1497
1₁(729)	→	730
1₁(431)	→	432
1₁(460)	→	461
1₁(425)	→	426
1₁(809)	→	810
1₁(524)	→	525
1₁(1056)	→	1057
1₁(427)	→	428
1₁(764)	→	765
1₁(1051)	→	1052
1₁(697)	→	698
1₁(1158)	→	1159
1₁(845)	→	846
1₁(1510)	→	1511
1₁(1446)	→	1447
1₁(548)	→	549
1₁(770)	→	771
1₁(640)	→	641
1₁(629)	→	630
1₁(717)	→	718
1₁(608)	→	609
1₁(1306)	→	1307
1₁(723)	→	724
1₁(1297)	→	1298
1₁(436)	→	437
1₁(453)	→	454
1₁(565)	→	566
1₁(1527)	→	1528
1₁(701)	→	702
1₁(784)	→	785
1₁(454)	→	455
1₁(781)	→	782
1₁(584)	→	585
1₁(386)	→	387
1₁(685)	→	686
1₁(500)	→	501
1₁(1160)	→	1161
1₁(655)	→	656
1₁(575)	→	576
1₁(1397)	→	1398
1₁(345)	→	346
1₁(1060)	→	1061
1₁(1514)	→	1515
1₁(492)	→	493
4₂(1588)	→	1589
2₂(917)	→	918
2₂(1593)	→	1594
2₂(1589)	→	1590
2₂(934)	→	935
2₂(943)	→	944
5₂(918)	→	919
5₂(944)	→	945
5₂(935)	→	936
5₂(1594)	→	1595
5₁(1186)	→	1187
5₁(429)	→	430
5₁(1276)	→	1277
5₁(1205)	→	1206
5₁(1634)	→	1635
5₁(1213)	→	1214
5₁(968)	→	969
5₁(644)	→	645
5₁(1392)	→	1393
5₁(1694)	→	1695
5₁(465)	→	466
5₁(1118)	→	1119
5₁(559)	→	560
5₁(1197)	→	1198
5₁(167)	→	168
5₁(639)	→	640
5₁(660)	→	661
5₁(263)	→	264
5₁(1706)	→	1707
5₁(296)	→	297
5₁(1143)	→	1144
5₁(1284)	→	1285
5₁(682)	→	683
5₁(696)	→	697
5₁(1282)	→	1283
5₁(814)	→	815
5₁(1211)	→	1212
5₁(1680)	→	1681
5₁(1080)	→	1081
5₁(706)	→	707
5₁(1070)	→	1071
5₁(483)	→	484
5₁(775)	→	776
5₁(558)	→	559
5₁(1508)	→	1509
5₁(1688)	→	1689
5₁(967)	→	968
5₁(1626)	→	1627
5₁(1678)	→	1679
5₁(1402)	→	1403
5₁(622)	→	623
5₁(721)	→	722
5₁(1150)	→	1151
5₁(1686)	→	1687
5₁(825)	→	826
5₁(604)	→	605
5₁(1095)	→	1096
5₁(169)	→	170
5₁(490)	→	491
5₁(1180)	→	1181
5₁(168)	→	169
5₁(1062)	→	1063
5₁(556)	→	557
5₁(232)	→	233
5₁(570)	→	571
5₁(228)	→	229
5₁(552)	→	553
5₁(643)	→	644
5₁(1636)	→	1637
5₁(52)	→	53
5₁(773)	→	774
5₁(787)	→	788
5₁(507)	→	508
5₁(447)	→	448
5₁(674)	→	675
5₁(730)	→	731
5₁(1247)	→	1248
5₁(1790)	→	1791
5₁(1049)	→	1050
5₁(1264)	→	1265
5₁(1054)	→	1055
5₁(197)	→	198
5₁(568)	→	569
5₁(1533)	→	1534
5₁(718)	→	719
5₁(1394)	→	1395
5₁(488)	→	489
5₁(1668)	→	1669
5₁(665)	→	666
5₁(583)	→	584
5₁(649)	→	650
5₁(435)	→	436
5₁(1266)	→	1267
5₁(1447)	→	1448
5₁(1046)	→	1047
5₁(1255)	→	1256
5₁(1097)	→	1098
5₁(1191)	→	1192
5₁(265)	→	266
5₁(298)	→	299
5₁(1261)	→	1262
5₁(479)	→	480
5₁(1520)	→	1521
5₁(698)	→	699
5₁(969)	→	970
5₁(631)	→	632
5₁(1263)	→	1264
5₁(636)	→	637
5₁(1305)	→	1306
5₁(171)	→	172
5₁(512)	→	513
5₁(1772)	→	1773
5₁(1532)	→	1533
5₁(499)	→	500
5₁(763)	→	764
5₁(1093)	→	1094
5₁(1628)	→	1629
5₁(226)	→	227
5₁(1078)	→	1079
5₁(199)	→	200
5₁(634)	→	635
5₁(486)	→	487
5₁(1199)	→	1200
5₁(681)	→	682
5₁(725)	→	726
5₁(1788)	→	1789
5₁(572)	→	573
5₁(1577)	→	1578
5₁(815)	→	816
5₁(1159)	→	1160
5₁(1506)	→	1507
5₁(1203)	→	1204
5₁(522)	→	523
5₁(753)	→	754
5₁(1147)	→	1148
5₁(561)	→	562
5₁(741)	→	742
4₀(3)	→	5
4₀(6)	→	5
4₀(5)	→	5
4₀(4)	→	5
4₀(2)	→	5
4₀(1)	→	5
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
0₀(1)	→	4
0₀(6)	→	4
0₀(3)	→	4
0₀(5)	→	4
0₀(2)	→	4
0₀(4)	→	4
0₁(432)	→	433
0₁(1449)	→	1450
0₁(1513)	→	1514
0₁(1730)	→	1731
0₁(1050)	→	1051
0₁(506)	→	507
0₁(8)	→	9
0₁(529)	→	530
0₁(1450)	→	1451
0₁(1387)	→	1388
0₁(1251)	→	1252
0₁(1052)	→	1053
0₁(1728)	→	1729
0₁(1153)	→	1154
0₁(336)	→	337
0₁(430)	→	431
0₁(734)	→	735
0₁(535)	→	536
0₁(714)	→	715
0₁(1454)	→	1455
0₁(613)	→	614
0₁(844)	→	845
0₁(230)	→	231
0₁(493)	→	494
0₁(1162)	→	1163
0₁(523)	→	524
0₁(564)	→	565
0₁(744)	→	745
0₁(1188)	→	1189
0₁(1349)	→	1350
0₁(913)	→	914
0₁(428)	→	429
0₁(1716)	→	1717
0₁(509)	→	510
0₁(1339)	→	1340
0₁(343)	→	344
0₁(659)	→	660
0₁(1269)	→	1270
0₁(576)	→	577
0₁(911)	→	912
0₁(22)	→	23
0₁(448)	→	449
0₁(92)	→	93
0₁(348)	→	349
0₁(20)	→	21
0₁(731)	→	732
0₁(658)	→	659
0₁(546)	→	547
0₁(903)	→	904
0₁(1598)	→	1599
0₁(651)	→	652
0₁(527)	→	528
0₁(736)	→	737
0₁(1048)	→	1049
0₁(516)	→	517
0₁(566)	→	567
0₁(450)	→	451
0₁(1714)	→	1715
0₁(48)	→	49
0₁(1335)	→	1336
0₁(907)	→	908
0₁(580)	→	581
0₁(646)	→	647
0₁(1722)	→	1723
0₁(724)	→	725
0₁(909)	→	910
0₁(34)	→	35
0₁(1724)	→	1725
0₁(1600)	→	1601
0₁(1604)	→	1605
0₁(1398)	→	1399
0₁(702)	→	703
0₁(1602)	→	1603
0₁(757)	→	758
0₁(32)	→	33
0₁(1249)	→	1250
0₁(905)	→	906
0₁(579)	→	580
0₁(1341)	→	1342
0₁(901)	→	902
0₁(1298)	→	1299
0₁(780)	→	781
0₁(726)	→	727
0₁(1347)	→	1348
0₁(1157)	→	1158
0₁(691)	→	692
0₁(1185)	→	1186
0₁(497)	→	498
0₁(526)	→	527
0₁(1271)	→	1272
0₁(642)	→	643
0₁(842)	→	843
0₁(517)	→	518
0₁(1534)	→	1535
0₁(496)	→	497
0₁(1301)	→	1302
0₁(1333)	→	1334
0₁(537)	→	538
0₁(748)	→	749
0₁(1253)	→	1254
0₁(1606)	→	1607
0₁(743)	→	744
0₁(1302)	→	1303
0₁(1149)	→	1150
0₁(466)	→	467
0₁(485)	→	486
0₁(1156)	→	1157
0₁(1272)	→	1273
0₁(1700)	→	1701
0₁(337)	→	338
0₁(641)	→	642
0₁(525)	→	526
0₁(645)	→	646
0₁(1596)	→	1597
0₁(816)	→	817
2₁(549)	→	550
2₁(1530)	→	1531
2₁(1541)	→	1542
2₁(138)	→	139
2₁(1509)	→	1510
2₁(632)	→	633
2₁(692)	→	693
2₁(1257)	→	1258
2₁(1738)	→	1739
2₁(606)	→	607
2₁(1309)	→	1310
2₁(562)	→	563
2₁(828)	→	829
2₁(437)	→	438
2₁(449)	→	450
2₁(93)	→	94
2₁(1401)	→	1402
2₁(229)	→	230
2₁(1736)	→	1737
2₁(851)	→	852
2₁(1388)	→	1389
2₁(1444)	→	1445
2₁(849)	→	850
2₁(1357)	→	1358
2₁(544)	→	545
2₁(1267)	→	1268
2₁(817)	→	818
2₁(705)	→	706
2₁(966)	→	967
2₁(756)	→	757
2₁(1539)	→	1540
2₁(1529)	→	1530
2₁(1359)	→	1360
2₁(459)	→	460
2₁(95)	→	96
2₁(1770)	→	1771
2₁(832)	→	833
2₁(1535)	→	1536
2₁(853)	→	854
2₁(762)	→	763
2₁(1415)	→	1416
2₁(463)	→	464
2₁(1082)	→	1083
2₁(1543)	→	1544
2₁(91)	→	92
2₁(983)	→	984
2₁(686)	→	687
2₁(627)	→	628
2₁(140)	→	141
2₁(776)	→	777
2₁(840)	→	841
2₁(1744)	→	1745
2₁(1182)	→	1183
2₁(811)	→	812
2₁(511)	→	512
2₁(823)	→	824
2₁(846)	→	847
2₁(1385)	→	1386
2₁(503)	→	504
2₁(745)	→	746
2₁(117)	→	118
2₁(722)	→	723
2₁(1547)	→	1548
2₁(1474)	→	1475
2₁(759)	→	760
2₁(1190)	→	1191
2₁(89)	→	90
2₁(830)	→	831
2₁(452)	→	453
2₁(1112)	→	1113
2₁(520)	→	521
2₁(612)	→	613
2₁(650)	→	651
2₁(587)	→	588
2₁(1161)	→	1162
2₁(1472)	→	1473
2₁(739)	→	740
2₁(1116)	→	1117
2₁(812)	→	813
2₁(738)	→	739
2₁(977)	→	978
2₁(494)	→	495
2₁(1545)	→	1546
2₁(1451)	→	1452
2₁(752)	→	753
2₁(1361)	→	1362
2₁(1624)	→	1625
2₁(10)	→	11
2₁(115)	→	116
2₁(654)	→	655
2₁(821)	→	822
2₁(826)	→	827
2₁(347)	→	348
2₁(585)	→	586
2₁(501)	→	502
2₁(975)	→	976
2₁(1445)	→	1446
2₁(1307)	→	1308
2₁(1622)	→	1623
2₁(688)	→	689
2₁(1154)	→	1155
2₁(339)	→	340
2₁(51)	→	52
2₁(451)	→	452
2₁(1746)	→	1747
2₁(1549)	→	1550
2₀(3)	→	2
2₀(5)	→	2
2₀(2)	→	2
2₀(4)	→	2
2₀(1)	→	2
2₀(6)	→	2
1₀(2)	→	3
1₀(4)	→	3
1₀(3)	→	3
1₀(6)	→	3
1₀(1)	→	3
1₀(5)	→	3
3₁(710)	→	711
3₁(732)	→	733
3₁(434)	→	435
3₁(1183)	→	1184
3₁(835)	→	836
3₁(1122)	→	1123
3₁(346)	→	347
3₁(456)	→	457
3₁(774)	→	775
3₁(694)	→	695
3₁(1652)	→	1653
3₁(458)	→	459
3₁(481)	→	482
3₁(1515)	→	1516
3₁(1650)	→	1651
3₁(338)	→	339
3₁(1538)	→	1539
3₁(1128)	→	1129
3₁(504)	→	505
3₁(1262)	→	1263
3₁(720)	→	721
3₁(652)	→	653
3₁(1441)	→	1442
3₁(708)	→	709
3₁(684)	→	685
3₁(716)	→	717
3₁(683)	→	684
3₁(1752)	→	1753
3₁(484)	→	485
3₁(1265)	→	1266
3₁(477)	→	478
3₁(469)	→	470
3₁(765)	→	766
3₁(607)	→	608
3₁(841)	→	842
3₁(677)	→	678
3₁(1443)	→	1444
3₁(1518)	→	1519
3₁(1478)	→	1479
3₁(475)	→	476
3₁(839)	→	840
3₁(471)	→	472
3₁(1300)	→	1301
3₁(473)	→	474
3₁(1079)	→	1080
3₁(443)	→	444
3₁(462)	→	463
3₁(1084)	→	1085
3₁(820)	→	821
3₁(1507)	→	1508
3₁(719)	→	720
3₁(1120)	→	1121
3₁(557)	→	558
3₁(657)	→	658
3₁(662)	→	663
3₁(653)	→	654
3₁(1762)	→	1763
3₁(578)	→	579
3₁(70)	→	71
3₁(1421)	→	1422
3₁(1521)	→	1522
3₁(1386)	→	1387
3₁(445)	→	446
3₁(1395)	→	1396
3₁(1042)	→	1043
3₁(1117)	→	1118
3₁(1390)	→	1391
3₁(1111)	→	1112
3₁(68)	→	69
3₁(1644)	→	1645
3₁(1181)	→	1182
3₁(1417)	→	1418
3₁(611)	→	612
3₁(663)	→	664
3₁(785)	→	786
3₁(1115)	→	1116
3₁(782)	→	783
3₁(439)	→	440
3₁(746)	→	747
3₁(766)	→	767
3₁(626)	→	627
3₁(560)	→	561
3₁(1145)	→	1146
3₁(605)	→	606
3₁(768)	→	769
3₁(819)	→	820
3₁(1452)	→	1453
3₁(1423)	→	1424
3₁(661)	→	662
3₁(678)	→	679
3₁(638)	→	639
3₁(609)	→	610
3₁(1642)	→	1643
3₁(464)	→	465
3₁(50)	→	51
3₁(690)	→	691
3₁(699)	→	700
3₁(1142)	→	1143
3₁(1658)	→	1659
3₁(455)	→	456
3₁(1764)	→	1765
3₁(614)	→	615
3₁(1155)	→	1156
3₁(550)	→	551
3₁(495)	→	496
3₁(838)	→	839
3₁(712)	→	713
3₁(547)	→	548
3₁(1480)	→	1481
3₁(441)	→	442
3₁(1537)	→	1538
3₁(628)	→	629
3₁(1148)	→	1149
4₁(1083)	→	1084
4₁(848)	→	849
4₁(818)	→	819
4₁(581)	→	582
4₁(704)	→	705
4₁(519)	→	520
4₁(687)	→	688
4₁(676)	→	677
4₁(778)	→	779
4₁(813)	→	814
4₁(1396)	→	1397
4₁(574)	→	575
4₁(1512)	→	1513
4₁(1304)	→	1305
4₁(551)	→	552
4₁(703)	→	704
4₁(591)	→	592
4₁(700)	→	701
4₁(779)	→	780
4₁(1369)	→	1370
4₁(510)	→	511
4₁(1583)	→	1584
4₁(1585)	→	1586
4₁(772)	→	773
4₁(1189)	→	1190
4₁(783)	→	784
4₁(834)	→	835
4₁(1315)	→	1316
4₁(1308)	→	1309
4₁(1268)	→	1269
4₁(750)	→	751
4₁(623)	→	624
4₁(1525)	→	1526
4₁(1399)	→	1400
4₁(227)	→	228
4₁(1536)	→	1537
4₁(1453)	→	1454
4₁(680)	→	681
4₁(1448)	→	1449
4₁(482)	→	483
4₁(1708)	→	1709
4₁(1516)	→	1517
4₁(518)	→	519
4₁(679)	→	680
4₁(480)	→	481
4₁(1146)	→	1147
4₁(90)	→	91
4₁(771)	→	772
4₁(755)	→	756
4₁(563)	→	564
4₁(635)	→	636
4₁(1383)	→	1384
4₁(843)	→	844
4₁(824)	→	825
4₁(602)	→	603
4₁(760)	→	761
4₁(747)	→	748
4₁(582)	→	583
4₁(624)	→	625
4₁(438)	→	439
4₁(695)	→	696
4₁(742)	→	743
4₁(767)	→	768
4₁(1511)	→	1512
4₁(1303)	→	1304
4₁(1400)	→	1401
4₁(715)	→	716
4₁(1505)	→	1506
4₁(751)	→	752
4₁(637)	→	638
4₁(758)	→	759
4₁(1581)	→	1582
4₁(1187)	→	1188
4₁(593)	→	594
4₁(761)	→	762
4₁(1363)	→	1364
4₁(554)	→	555
4₁(1317)	→	1318
4₁(586)	→	587
4₁(621)	→	622
4₁(1296)	→	1297
4₁(553)	→	554
4₁(508)	→	509
4₁(1504)	→	1505
4₁(837)	→	838
4₁(630)	→	631
4₁(1391)	→	1392
4₁(589)	→	590
4₁(9)	→	10
4₁(595)	→	596
4₁(1144)	→	1145
4₁(1531)	→	1532
4₁(467)	→	468
0₂(932)	→	933
0₂(920)	→	921
0₂(1618)	→	1619
0₂(926)	→	927
0₂(941)	→	942
0₂(1778)	→	1779
0₂(922)	→	923
0₂(1616)	→	1617
0₂(1614)	→	1615
0₂(1612)	→	1613
0₂(915)	→	916
0₂(1591)	→	1592
0₂(1587)	→	1588
0₂(1608)	→	1609
0₂(946)	→	947
0₂(1620)	→	1621
3₀(1)	→	1
3₀(6)	→	1
3₀(5)	→	1
3₀(2)	→	1
3₀(3)	→	1
3₀(4)	→	1
3₂(916)	→	917
3₂(1592)	→	1593
3₂(942)	→	943
3₂(933)	→	934

The automaton is closed under rewriting as it is compatible.