Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4282)

The rewrite relation of the following TRS is considered.

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

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

0(0(3(x1)))	→	3(3(2(3(1(3(1(3(3(3(x1))))))))))	(43)
4(1(0(0(x1))))	→	4(1(1(5(2(5(5(3(2(5(x1))))))))))	(44)
1(0(4(0(x1))))	→	1(3(2(2(3(2(2(2(3(5(x1))))))))))	(45)
3(0(0(4(x1))))	→	3(2(5(5(3(2(4(3(3(5(x1))))))))))	(46)
0(4(2(4(x1))))	→	4(3(0(3(1(2(0(5(1(1(x1))))))))))	(47)
4(0(0(5(x1))))	→	4(4(4(5(0(1(1(3(2(5(x1))))))))))	(48)
0(1(0(4(0(x1)))))	→	2(3(5(5(1(4(5(3(2(5(x1))))))))))	(49)
0(1(0(0(1(x1)))))	→	2(3(3(2(2(5(4(4(0(1(x1))))))))))	(50)
1(0(0(4(2(x1)))))	→	1(4(3(3(3(3(3(2(0(2(x1))))))))))	(51)
5(0(4(0(3(x1)))))	→	2(2(5(0(4(3(1(1(4(3(x1))))))))))	(52)
1(2(5(2(3(x1)))))	→	1(1(3(4(1(1(3(2(2(3(x1))))))))))	(53)
1(4(0(0(5(x1)))))	→	3(0(0(3(2(2(1(1(3(1(x1))))))))))	(54)
0(0(0(5(0(0(x1))))))	→	4(4(0(4(4(4(5(4(3(0(x1))))))))))	(55)
3(4(0(0(0(1(x1))))))	→	3(3(2(3(4(2(2(5(5(1(x1))))))))))	(56)
2(3(5(0(3(1(x1))))))	→	2(2(5(1(3(3(0(3(2(1(x1))))))))))	(57)
0(5(4(2(3(1(x1))))))	→	0(2(5(1(3(3(0(1(1(1(x1))))))))))	(58)
1(2(0(5(4(1(x1))))))	→	1(5(5(3(1(2(1(1(2(1(x1))))))))))	(59)
3(5(2(4(0(2(x1))))))	→	1(4(5(5(1(3(2(4(1(2(x1))))))))))	(60)
1(0(0(1(0(4(x1))))))	→	1(5(5(1(4(3(1(4(2(4(x1))))))))))	(61)
4(0(4(4(1(4(x1))))))	→	4(4(2(0(5(1(3(3(1(4(x1))))))))))	(62)
0(4(0(0(0(5(x1))))))	→	4(3(0(1(1(4(3(5(0(5(x1))))))))))	(63)
5(0(0(2(4(5(x1))))))	→	4(1(2(5(0(1(1(5(4(5(x1))))))))))	(64)
3(4(2(3(0(0(0(x1)))))))	→	3(2(1(0(4(5(5(2(2(5(x1))))))))))	(65)
0(5(0(4(2(0(0(x1)))))))	→	4(3(4(4(0(1(4(2(2(5(x1))))))))))	(66)
3(4(0(2(5(1(0(x1)))))))	→	3(4(3(0(2(3(1(1(1(0(x1))))))))))	(67)
5(0(0(3(3(4(0(x1)))))))	→	5(0(0(3(3(3(1(4(5(2(x1))))))))))	(68)
3(0(0(0(0(0(1(x1)))))))	→	1(0(1(5(2(1(1(5(2(5(x1))))))))))	(69)
1(4(5(0(0(0(1(x1)))))))	→	1(4(3(4(2(0(1(3(2(1(x1))))))))))	(70)
1(0(2(1(2(3(1(x1)))))))	→	1(3(5(1(1(3(1(2(4(1(x1))))))))))	(71)
4(4(1(0(2(0(2(x1)))))))	→	3(1(0(3(4(5(3(2(0(2(x1))))))))))	(72)
0(5(0(3(5(0(2(x1)))))))	→	0(4(4(1(1(2(1(5(5(2(x1))))))))))	(73)
1(0(5(2(4(1(2(x1)))))))	→	3(5(4(5(5(3(2(0(4(2(x1))))))))))	(74)
3(5(2(3(3(4(2(x1)))))))	→	5(4(4(2(2(3(2(4(4(2(x1))))))))))	(75)
2(3(4(0(3(5(2(x1)))))))	→	0(3(0(3(3(0(3(5(2(2(x1))))))))))	(76)
4(0(3(5(0(3(3(x1)))))))	→	4(1(3(5(5(0(1(4(3(3(x1))))))))))	(77)
2(4(5(4(1(4(3(x1)))))))	→	2(1(1(3(1(1(3(3(5(3(x1))))))))))	(78)
2(1(4(2(3(4(3(x1)))))))	→	0(3(1(3(5(1(1(1(5(3(x1))))))))))	(79)
1(2(0(4(5(2(4(x1)))))))	→	1(5(4(1(5(5(1(1(1(1(x1))))))))))	(80)
5(0(1(0(2(3(4(x1)))))))	→	4(3(0(1(0(3(3(1(3(4(x1))))))))))	(81)
3(4(3(2(3(3(4(x1)))))))	→	4(4(5(3(3(3(0(3(0(4(x1))))))))))	(82)
0(0(5(0(1(0(5(x1)))))))	→	0(0(3(4(3(1(1(0(0(5(x1))))))))))	(83)
1(0(4(1(0(4(5(x1)))))))	→	1(4(2(1(5(3(5(4(1(4(x1))))))))))	(84)

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:

1405	→	734
1405	→	159
1405	→	709
1405	→	6
1405	→	87
1405	→	732
1405	→	158
1198	→	357
854	→	1277
854	→	1299
854	→	1472
223	→	194
223	→	291
223	→	563
223	→	606
223	→	809
157	→	1832
157	→	1927
588	→	564
1380	→	657
221	→	194
221	→	312
221	→	572
221	→	616
221	→	828
221	→	4
221	→	750
221	→	457
221	→	1833
846	→	810
733	→	714
1940	→	1134
633	→	1040
633	→	1323
633	→	1428
315	→	292
1608	→	1599
89	→	262
1394	→	691
202	→	1088
202	→	1127
202	→	1144
263	→	1462
1463	→	806
338	→	292
87	→	159
87	→	711
87	→	734
87	→	1629
1089	→	1074
1089	→	1621
1624	→	1602
1072	→	1065
1072	→	1909
1475	→	812
1630	→	194
1630	→	620
1630	→	480
1630	→	4
1630	→	644
1630	→	335
1630	→	589
1630	→	843
1630	→	261
855	→	5
855	→	939
855	→	681
855	→	654
855	→	674
1007	→	9
880	→	1230
880	→	1700
1603	→	1848
10	→	892
10	→	975
1169	→	262
1169	→	1273
742	→	190
1261	→	500
1367	→	655
571	→	191
294	→	1509
1409	→	737
1473	→	810
96	→	5
96	→	939
96	→	681
96	→	848
96	→	654
96	→	664
96	→	293
96	→	1192
96	→	1445
96	→	1928
608	→	804
1209	→	167
1606	→	619
1606	→	882
1606	→	783
1606	→	758
1606	→	3
1606	→	355
1606	→	402
1606	→	625
655	→	1474
1386	→	686
136	→	87
136	→	689
136	→	713
995	→	766
167	→	1445
1740	→	2082
811	→	1333
1849	→	1280
956	→	633
956	→	1260
784	→	759
784	→	856
784	→	1567
1954	→	847
1954	→	604
1954	→	352
1954	→	620
1954	→	480
1954	→	194
1954	→	1319
1954	→	644
1954	→	335
1954	→	589
1954	→	843
1954	→	261
1792	→	194
1160	→	1134
466	→	4
466	→	847
466	→	604
466	→	352
466	→	618
466	→	457
466	→	194
466	→	957
466	→	682
466	→	314
466	→	587
466	→	830
466	→	241
466	→	750
466	→	1319
466	→	843
466	→	335
466	→	480
466	→	620
466	→	644
466	→	589
466	→	261
466	→	168
1670	→	1664
1584	→	895
1724	→	1713
625	→	607
676	→	654
676	→	1406
676	→	1517
18	→	1
18	→	499
18	→	554
18	→	1686
1118	→	1639
41	→	1723
3	→	84
3	→	112
3	→	260
3	→	399
3	→	508
3	→	679
955	→	1030
955	→	1042
1506	→	867
1411	→	753
499	→	749
1104	→	500
652	→	2
652	→	899
652	→	422
652	→	184
652	→	160
652	→	448
652	→	9
652	→	42
652	→	885
652	→	1568
1888	→	865
1289	→	161
617	→	607
500	→	1669
500	→	1675
907	→	614
298	→	288
9	→	422
9	→	448
9	→	899
9	→	1653
914	→	889
914	→	1266
1332	→	899
1332	→	422
1332	→	184
1332	→	661
1332	→	420
1332	→	114
1332	→	63
1332	→	220
1332	→	525
1332	→	2
1332	→	160
1332	→	448
1332	→	9
1332	→	885
1332	→	1568
5	→	65
5	→	135
5	→	240
5	→	354
5	→	527
5	→	673
1629	→	1879
95	→	1084
95	→	1116
95	→	1146
95	→	1317
642	→	167
1076	→	1593
1126	→	749
1126	→	1
1126	→	940
1126	→	499
1126	→	528
65	→	1725
1918	→	159
1918	→	1923
1454	→	1885
456	→	167
483	→	458
483	→	1387
483	→	1412
185	→	1589
241	→	194
241	→	314
241	→	457
241	→	587
241	→	618
241	→	830
891	→	3
891	→	882
891	→	783
891	→	779
891	→	449
891	→	355
891	→	421
891	→	619
891	→	758
891	→	402
891	→	625
765	→	1258
947	→	1082
947	→	1131
947	→	1159
381	→	355
381	→	1170
243	→	194
243	→	337
243	→	602
243	→	622
243	→	845
756	→	1597
1806	→	1134
674	→	654
889	→	964
90	→	284
1890	→	865
1668	→	66
1668	→	931
1833	→	457
938	→	721
1132	→	1117
1403	→	1889
1034	→	1172
1493	→	1939
1	→	41
1	→	157
1	→	193
1	→	378
1	→	553
1	→	653
1726	→	1713
1730	→	9
654	→	681
654	→	930
654	→	939
1884	→	87
690	→	949
1298	→	430
1837	→	465
695	→	200
1331	→	1883
1081	→	289
940	→	1505
1707	→	167
778	→	759
1318	→	635
1749	→	159
688	→	267
1722	→	1686
1052	→	848
1130	→	1117
590	→	564
44	→	9
1278	→	607
1515	→	1834
1515	→	1925
1029	→	465
402	→	355
402	→	758
1194	→	357
1790	→	194
748	→	201
634	→	1
634	→	690
634	→	552
634	→	712
634	→	710
634	→	950
634	→	554
423	→	1262
1676	→	41
261	→	194
261	→	335
261	→	480
261	→	589
261	→	620
261	→	843
573	→	564
735	→	714
881	→	2
881	→	899
881	→	422
881	→	184
881	→	160
881	→	448
881	→	9
881	→	885
881	→	1568
1070	→	190
816	→	166
920	→	641
1413	→	464
662	→	654
662	→	1397
1654	→	932
1622	→	1599
1709	→	965
994	→	1911
890	→	1006
890	→	1038
890	→	1208
890	→	1435
268	→	95
619	→	607
552	→	499
552	→	1195
552	→	653
552	→	378
552	→	157
552	→	41
552	→	193
552	→	553
552	→	1
138	→	87
138	→	1499
138	→	1501
1176	→	1819
844	→	810
1926	→	167
509	→	499
509	→	1197
526	→	499
526	→	1191
526	→	1393
526	→	1685
976	→	1385
976	→	1587
1322	→	167
1322	→	1887
1382	→	686
2071	→	865
6	→	8
6	→	137
6	→	242
6	→	380
6	→	551
6	→	675
554	→	499
554	→	1193
792	→	651
1240	→	847
1240	→	604
1240	→	352
1240	→	618
1240	→	457
1240	→	194
1240	→	957
1240	→	663
1240	→	401
1240	→	86
1240	→	43
1240	→	222
1240	→	498
1240	→	4
1240	→	682
1240	→	314
1240	→	587
1240	→	830
1240	→	241
1240	→	1319
1240	→	843
1240	→	335
1240	→	480
1240	→	750
1240	→	620
1240	→	644
1240	→	589
1240	→	261
1240	→	168
1032	→	1408
627	→	915
627	→	1410
627	→	1623
1667	→	1748
1667	→	1791
1667	→	1805
1882	→	87
220	→	1881
88	→	736
88	→	785
88	→	1168
88	→	679
88	→	399
88	→	112
88	→	84
88	→	260
88	→	508
88	→	3
88	→	449
88	→	779
88	→	421
982	→	499
982	→	1
982	→	554
1037	→	455
1763	→	159
1818	→	378
431	→	6
431	→	734
431	→	159
431	→	709
431	→	87
431	→	732
431	→	158
1041	→	1031
1041	→	1064
1041	→	1488
1701	→	167
288	→	1830
1205	→	734
1205	→	159
1205	→	709
1205	→	6
1205	→	87
1205	→	732
1205	→	158
292	→	1294
363	→	167
336	→	292
615	→	3
615	→	882
615	→	783
615	→	779
615	→	449
615	→	161
615	→	355
615	→	421
615	→	655
1566	→	886
900	→	908
1192	→	293
831	→	810
1242	→	1231
1500	→	857
1516	→	899
1516	→	422
1516	→	184
1516	→	661
1516	→	420
1516	→	114
1516	→	63
1516	→	220
1516	→	525
1516	→	2
1516	→	160
1516	→	448
1516	→	9
1516	→	885
1516	→	1568
808	→	361
2	→	63
2	→	114
2	→	220
2	→	420
2	→	525
2	→	661
313	→	292
863	→	633
863	→	1366
872	→	465
954	→	1008
4	→	43
4	→	86
4	→	222
4	→	401
4	→	498
4	→	663
528	→	499
1178	→	749
1178	→	292
1178	→	653
1178	→	378
1178	→	157
1178	→	41
1178	→	193
1178	→	553
1178	→	1
1178	→	353
1178	→	499
1018	→	1
1018	→	634
1018	→	1945
400	→	355
400	→	777
1594	→	903
1786	→	194
1404	→	1746
1404	→	1770
1404	→	1789
1404	→	1795
1404	→	1856
1892	→	8
1814	→	167
66	→	9
66	→	661
66	→	420
66	→	114
66	→	63
66	→	220
66	→	525
66	→	2
66	→	1713
66	→	1726
379	→	355
379	→	1226
379	→	779
379	→	449
379	→	3
379	→	421
481	→	458
862	→	1073
862	→	1094
913	→	1279
766	→	1241
766	→	1706
421	→	355
421	→	779
421	→	1168
1334	→	647
1773	→	1095
981	→	1959
1962	→	1945
1125	→	1764
1125	→	1785
1125	→	1797
623	→	607
1835	→	457
1145	→	1134
1586	→	900
1743	→	87
1143	→	866
1143	→	1505
1143	→	940
12	→	1381
720	→	1507
1436	→	1429
85	→	9
1604	→	1708
1604	→	1836
1771	→	1095
1455	→	42
697	→	690
1878	→	758
663	→	1762
663	→	1787
663	→	1803
1605	→	1729
1605	→	1742
1605	→	1815
1605	→	1877
621	→	607
757	→	191
757	→	1659
1085	→	1074
290	→	1
290	→	749
290	→	292
290	→	353
290	→	499
710	→	690
1686	→	950
1236	→	1731
724	→	714
1765	→	159
1765	→	1919
113	→	87
113	→	696
113	→	723
1207	→	425
42	→	9
42	→	661
42	→	420
42	→	114
42	→	63
42	→	220
42	→	525
42	→	2
42	→	500
42	→	1713
42	→	1724
64	→	9
1816	→	167
362	→	1585
1196	→	357
1396	→	693
1494	→	721
1259	→	500
1910	→	902
948	→	2
948	→	66
948	→	931
158	→	87
158	→	709
158	→	732
158	→	6
1745	→	87
1831	→	1820
1083	→	1074
115	→	87
115	→	1264
763	→	985
1128	→	1117
1886	→	87
17	→	1961
160	→	184
160	→	1395
160	→	1565
1272	→	1080
1894	→	8
651	→	1456
712	→	690
1502	→	858
1017	→	1727
1788	→	194
168	→	4
168	→	352
168	→	604
168	→	847
168	→	194
168	→	750
168	→	620
168	→	480
168	→	644
168	→	335
168	→	589
168	→	843
168	→	261
168	→	618
168	→	457
168	→	957
168	→	682
168	→	314
168	→	587
168	→	830
168	→	241
168	→	1833
424	→	1581
664	→	654
664	→	848
664	→	5
462	→	1019
1508	→	865
1407	→	1398
1928	→	167
974	→	509
974	→	356
1087	→	1074
1087	→	1607
203	→	1
203	→	749
203	→	866
203	→	940
203	→	499
203	→	528
203	→	554
203	→	710
203	→	552
203	→	712
1796	→	1134
1457	→	1446
865	→	873
865	→	1379
722	→	6
722	→	734
722	→	159
722	→	709
722	→	87
722	→	732
722	→	158
829	→	810
353	→	292
1434	→	954
1227	→	451
848	→	810
1798	→	1134
358	→	849
1225	→	451
1028	→	1891
1741	→	1239
1804	→	1134
195	→	626
195	→	1199
1171	→	262
1320	→	637
1016	→	1893
1518	→	1509
1829	→	1319
1829	→	644
1829	→	847
1829	→	604
1829	→	352
1829	→	620
1829	→	480
1829	→	194
1829	→	335
1829	→	589
1829	→	843
1829	→	261
660	→	640
680	→	654
1388	→	11
1568	→	885
1876	→	758
507	→	202
194	→	352
194	→	482
194	→	604
194	→	624
194	→	847
1912	→	86
603	→	564
1265	→	565
605	→	564
551	→	1744
551	→	1875
1857	→	167
1857	→	2070
767	→	6
767	→	734
767	→	159
767	→	709
767	→	87
767	→	732
767	→	158
1924	→	194
682	→	957
682	→	1206
682	→	1583
737	→	743
1920	→	194
721	→	1086
721	→	1129
721	→	1133
721	→	1321
721	→	1772
1263	→	502
1274	→	609
1588	→	454
2083	→	8
1747	→	159
1590	→	903
644	→	1319
1880	→	87
1300	→	167
1147	→	1134
191	→	1712
192	→	2
192	→	42
192	→	66
192	→	931
192	→	1726
780	→	759
1640	→	659
607	→	635
1039	→	1031
1039	→	1071
1960	→	1945
355	→	643
355	→	783
355	→	864
355	→	882
883	→	1224
963	→	362
1728	→	8
1728	→	1813
1728	→	1817
1728	→	1917
898	→	94
1582	→	895
5₁(871)	→	872
5₁(1080)	→	1081
5₁(501)	→	502
5₁(1515)	→	1516
5₁(911)	→	912
5₁(1328)	→	1329
5₁(1406)	→	1407
5₁(137)	→	138
5₁(1038)	→	1039
5₁(1264)	→	1265
5₁(1174)	→	1175
5₁(766)	→	767
5₁(1623)	→	1624
5₁(896)	→	897
5₁(563)	→	564
5₁(738)	→	739
5₁(958)	→	959
5₁(1885)	→	1886
5₁(1488)	→	1489
5₁(883)	→	884
5₁(265)	→	266
5₁(895)	→	896
5₁(602)	→	603
5₁(777)	→	778
5₁(815)	→	816
5₁(1879)	→	1880
5₁(1883)	→	1884
5₁(286)	→	287
5₁(587)	→	588
5₁(195)	→	196
5₁(1445)	→	1446
5₁(1202)	→	1203
5₁(1381)	→	1382
5₁(785)	→	786
5₁(1447)	→	1448
5₁(1597)	→	1598
5₁(1744)	→	1745
5₁(779)	→	780
5₁(1030)	→	1031
5₁(1742)	→	1743
5₁(1499)	→	1500
5₁(114)	→	115
5₁(960)	→	961
5₁(1033)	→	1034
5₁(157)	→	158
5₁(856)	→	857
5₁(1084)	→	1085
5₁(1917)	→	1918
5₁(1451)	→	1452
5₁(1036)	→	1037
5₁(649)	→	650
5₁(783)	→	784
5₁(945)	→	946
5₁(916)	→	917
5₁(86)	→	87
5₁(1385)	→	1386
5₁(1429)	→	1430
5₁(1393)	→	1394
5₁(604)	→	605
5₁(188)	→	189
5₁(690)	→	691
5₁(1262)	→	1263
5₁(1040)	→	1041
5₁(589)	→	590
5₁(1401)	→	1402
5₁(1073)	→	1074
5₁(112)	→	113
5₁(869)	→	870
5₁(1764)	→	1765
5₁(849)	→	850
5₁(1456)	→	1457
5₁(90)	→	91
5₁(1762)	→	1763
5₁(758)	→	759
5₁(92)	→	93
5₁(1665)	→	1666
5₁(880)	→	881
5₁(1601)	→	1602
5₁(564)	→	565
5₁(1329)	→	1330
5₁(718)	→	719
5₁(1118)	→	1119
5₁(868)	→	869
5₁(640)	→	641
5₁(135)	→	136
5₁(89)	→	90
5₁(1175)	→	1176
5₁(1748)	→	1749
5₁(1585)	→	1586
5₁(1297)	→	1298
5₁(1086)	→	1087
5₁(1079)	→	1080
5₁(737)	→	738
5₁(917)	→	918
5₁(428)	→	429
5₁(789)	→	790
5₁(1082)	→	1083
5₁(189)	→	190
5₁(294)	→	295
5₁(648)	→	649
5₁(1088)	→	1089
5₁(612)	→	613
5₁(572)	→	573
5₁(899)	→	900
5₁(685)	→	686
5₁(1034)	→	1035
5₁(641)	→	642
5₁(631)	→	632
5₁(287)	→	288
5₁(1881)	→	1882
5₁(1397)	→	1398
5₁(714)	→	715
5₁(1746)	→	1747
0₂(1136)	→	1137
0₂(1140)	→	1141
0₂(1282)	→	1283
2₂(971)	→	972
2₂(1288)	→	1289
2₂(1287)	→	1288
2₂(1137)	→	1138
2₂(1043)	→	1044
2₂(1102)	→	1103
2₂(1026)	→	1027
2₂(1280)	→	1281
2₂(1098)	→	1099
2₂(1738)	→	1739
2₂(992)	→	993
2₂(1047)	→	1048
2₂(1821)	→	1822
2₂(1719)	→	1720
2₂(1945)	→	1946
2₂(1946)	→	1947
2₂(1015)	→	1016
2₂(1820)	→	1821
5₂(1772)	→	1773
5₂(1135)	→	1136
5₂(1770)	→	1771
5₂(1100)	→	1101
5₂(1286)	→	1287
5₂(1045)	→	1046
5₂(1048)	→	1049
5₂(1094)	→	1095
5₂(1046)	→	1047
5₂(1042)	→	1043
5₂(1101)	→	1102
0₁(941)	→	942
0₁(754)	→	755
0₁(463)	→	464
0₁(1238)	→	1239
0₁(1201)	→	1202
0₁(696)	→	697
0₁(791)	→	792
0₁(551)	→	552
0₁(936)	→	937
0₁(427)	→	428
0₁(525)	→	526
0₁(689)	→	690
0₁(633)	→	634
0₁(1400)	→	1401
0₁(314)	→	315
0₁(291)	→	292
0₁(885)	→	886
0₁(805)	→	806
0₁(337)	→	338
0₁(352)	→	353
0₁(1565)	→	1566
0₁(1605)	→	1606
0₁(1119)	→	1120
0₁(939)	→	940
0₁(1685)	→	1686
0₁(312)	→	313
0₁(1659)	→	1660
0₁(888)	→	889
0₁(686)	→	687
0₁(1661)	→	1662
0₁(505)	→	506
0₁(745)	→	746
0₁(1675)	→	1676
0₁(264)	→	265
0₁(765)	→	766
0₁(865)	→	866
0₁(464)	→	465
0₁(1123)	→	1124
0₁(949)	→	950
0₁(1268)	→	1269
0₁(508)	→	509
0₁(890)	→	891
0₁(1273)	→	1274
0₁(553)	→	554
0₁(1462)	→	1463
0₁(709)	→	710
0₁(196)	→	197
0₁(717)	→	718
0₁(1581)	→	1582
0₁(1453)	→	1454
0₁(740)	→	741
0₁(764)	→	765
0₁(955)	→	956
0₁(608)	→	609
0₁(527)	→	528
0₁(627)	→	628
0₁(894)	→	895
0₁(498)	→	499
0₁(200)	→	201
0₁(355)	→	356
0₁(852)	→	853
0₁(1583)	→	1584
0₁(335)	→	336
0₁(934)	→	935
0₁(711)	→	712
0₁(1237)	→	1238
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
4₂(1825)	→	1826
4₂(1051)	→	1052
4₂(1142)	→	1143
4₂(1097)	→	1098
4₂(1950)	→	1951
1₀(1)	→	4
1₀(6)	→	4
1₀(3)	→	4
1₀(5)	→	4
1₀(2)	→	4
1₀(4)	→	4
1₁(1791)	→	1792
1₁(893)	→	894
1₁(1449)	→	1450
1₁(1233)	→	1234
1₁(1431)	→	1432
1₁(423)	→	424
1₁(1491)	→	1492
1₁(694)	→	695
1₁(626)	→	627
1₁(1319)	→	1320
1₁(1501)	→	1502
1₁(1230)	→	1231
1₁(636)	→	637
1₁(643)	→	644
1₁(1452)	→	1453
1₁(611)	→	612
1₁(906)	→	907
1₁(1832)	→	1833
1₁(915)	→	916
1₁(961)	→	962
1₁(1454)	→	1455
1₁(811)	→	812
1₁(263)	→	264
1₁(1599)	→	1600
1₁(716)	→	717
1₁(1653)	→	1654
1₁(1299)	→	1300
1₁(222)	→	223
1₁(1127)	→	1128
1₁(94)	→	95
1₁(859)	→	860
1₁(647)	→	648
1₁(741)	→	742
1₁(11)	→	12
1₁(260)	→	261
1₁(1206)	→	1207
1₁(857)	→	858
1₁(1241)	→	1242
1₁(242)	→	243
1₁(744)	→	745
1₁(1448)	→	1449
1₁(860)	→	861
1₁(1331)	→	1332
1₁(1379)	→	1380
1₁(198)	→	199
1₁(913)	→	914
1₁(458)	→	459
1₁(975)	→	976
1₁(13)	→	14
1₁(1232)	→	1233
1₁(659)	→	660
1₁(1116)	→	1117
1₁(1489)	→	1490
1₁(93)	→	94
1₁(1789)	→	1790
1₁(977)	→	978
1₁(220)	→	221
1₁(1323)	→	1324
1₁(1129)	→	1130
1₁(285)	→	286
1₁(1474)	→	1475
1₁(903)	→	904
1₁(1598)	→	1599
1₁(1919)	→	1920
1₁(651)	→	652
1₁(167)	→	168
1₁(681)	→	682
1₁(451)	→	452
1₁(1121)	→	1122
1₁(790)	→	791
1₁(452)	→	453
1₁(630)	→	631
1₁(194)	→	195
1₁(853)	→	854
1₁(951)	→	952
1₁(193)	→	194
1₁(1589)	→	1590
1₁(760)	→	761
1₁(814)	→	815
1₁(1639)	→	1640
1₁(1621)	→	1622
1₁(918)	→	919
1₁(1117)	→	1118
1₁(240)	→	241
1₁(1327)	→	1328
1₁(902)	→	903
1₁(813)	→	814
1₁(908)	→	909
1₁(1603)	→	1604
1₁(909)	→	910
1₁(1923)	→	1924
1₁(1600)	→	1601
1₁(910)	→	911
1₁(1398)	→	1399
1₁(1629)	→	1630
1₁(638)	→	639
1₁(1607)	→	1608
1₁(1593)	→	1594
1₁(905)	→	906
1₁(656)	→	657
1₁(935)	→	936
1₁(1787)	→	1788
1₁(750)	→	751
1₁(787)	→	788
1₁(1492)	→	1493
1₁(262)	→	263
1₁(1271)	→	1272
1₁(1587)	→	1588
1₁(455)	→	456
1₁(786)	→	787
1₁(1296)	→	1297
1₁(1399)	→	1400
1₁(931)	→	932
1₁(1834)	→	1835
1₁(693)	→	694
1₁(950)	→	951
1₁(424)	→	425
1₁(684)	→	685
1₁(751)	→	752
1₁(635)	→	636
1₁(1131)	→	1132
1₁(715)	→	716
1₁(1785)	→	1786
1₁(459)	→	460
1₁(720)	→	721
1₁(804)	→	805
1₁(749)	→	750
1₁(1173)	→	1174
1₁(1403)	→	1404
4₁(267)	→	268
4₁(502)	→	503
4₁(807)	→	808
4₁(1706)	→	1707
4₁(284)	→	285
4₁(673)	→	674
4₁(743)	→	744
4₁(692)	→	693
4₁(919)	→	920
4₁(1395)	→	1396
4₁(1887)	→	1888
4₁(1813)	→	1814
4₁(843)	→	844
4₁(828)	→	829
4₁(293)	→	294
4₁(1330)	→	1331
4₁(506)	→	507
4₁(746)	→	747
4₁(266)	→	267
4₁(2070)	→	2071
4₁(185)	→	186
4₁(957)	→	958
4₁(1667)	→	1668
4₁(756)	→	757
4₁(732)	→	733
4₁(864)	→	865
4₁(1815)	→	1816
4₁(809)	→	810
4₁(862)	→	863
4₁(95)	→	96
4₁(947)	→	948
4₁(1925)	→	1926
4₁(870)	→	871
4₁(644)	→	645
4₁(202)	→	203
4₁(1404)	→	1405
4₁(661)	→	662
4₁(1208)	→	1209
4₁(655)	→	656
4₁(1513)	→	1514
4₁(879)	→	880
4₁(503)	→	504
4₁(1700)	→	1701
4₁(734)	→	735
4₁(1666)	→	1667
4₁(847)	→	848
4₁(1889)	→	1890
4₁(504)	→	505
4₁(679)	→	680
4₁(713)	→	714
4₁(759)	→	760
4₁(830)	→	831
4₁(453)	→	454
4₁(422)	→	423
4₁(1514)	→	1515
4₁(1125)	→	1126
4₁(861)	→	862
4₁(873)	→	874
4₁(723)	→	724
4₁(850)	→	851
4₁(650)	→	651
4₁(721)	→	722
4₁(845)	→	846
4₁(1507)	→	1508
4₁(1324)	→	1325
4₁(426)	→	427
4₁(362)	→	363
4₁(1430)	→	1431
4₁(1472)	→	1473
4₁(1191)	→	1192
4₁(739)	→	740
4₁(658)	→	659
4₁(878)	→	879
4₁(892)	→	893
4₁(292)	→	293
4₁(1076)	→	1077
4₁(953)	→	954
4₁(946)	→	947
4₁(1517)	→	1518
4₁(500)	→	501
4₁(567)	→	568
4₁(747)	→	748
4₁(663)	→	664
4₁(1927)	→	1928
4₁(675)	→	676
4₁(653)	→	654
4₁(1200)	→	1201
4₁(1493)	→	1494
4₁(1172)	→	1173
3₀(3)	→	2
3₀(5)	→	2
3₀(2)	→	2
3₀(4)	→	2
3₀(1)	→	2
3₀(6)	→	2
2₀(2)	→	3
2₀(4)	→	3
2₀(3)	→	3
2₀(6)	→	3
2₀(1)	→	3
2₀(5)	→	3
3₁(1170)	→	1171
3₁(187)	→	188
3₁(940)	→	941
3₁(1727)	→	1728
3₁(1122)	→	1123
3₁(199)	→	200
3₁(17)	→	18
3₁(1669)	→	1670
3₁(887)	→	888
3₁(912)	→	913
3₁(166)	→	167
3₁(1064)	→	1065
3₁(933)	→	934
3₁(568)	→	569
3₁(1236)	→	1237
3₁(610)	→	611
3₁(357)	→	358
3₁(9)	→	10
3₁(854)	→	855
3₁(65)	→	66
3₁(683)	→	684
3₁(159)	→	160
3₁(944)	→	945
3₁(607)	→	608
3₁(1660)	→	1661
3₁(63)	→	64
3₁(1909)	→	1910
3₁(691)	→	692
3₁(1239)	→	1240
3₁(761)	→	762
3₁(1071)	→	1072
3₁(1387)	→	1388
3₁(184)	→	185
3₁(1893)	→	1894
3₁(901)	→	902
3₁(952)	→	953
3₁(900)	→	901
3₁(88)	→	89
3₁(462)	→	463
3₁(937)	→	938
3₁(1006)	→	1007
3₁(41)	→	42
3₁(1433)	→	1434
3₁(1729)	→	1730
3₁(752)	→	753
3₁(1226)	→	1227
3₁(480)	→	481
3₁(425)	→	426
3₁(360)	→	361
3₁(1231)	→	1232
3₁(12)	→	13
3₁(454)	→	455
3₁(1176)	→	1177
3₁(851)	→	852
3₁(657)	→	658
3₁(930)	→	931
3₁(1267)	→	1268
3₁(1911)	→	1912
3₁(976)	→	977
3₁(8)	→	9
3₁(288)	→	289
3₁(954)	→	955
3₁(1032)	→	1033
3₁(1074)	→	1075
3₁(1510)	→	1511
3₁(361)	→	362
3₁(1168)	→	1169
3₁(84)	→	85
3₁(1567)	→	1568
3₁(499)	→	500
3₁(1224)	→	1225
3₁(297)	→	298
3₁(682)	→	683
3₁(1326)	→	1327
3₁(812)	→	813
3₁(943)	→	944
3₁(359)	→	360
3₁(942)	→	943
3₁(358)	→	359
3₁(1410)	→	1411
3₁(14)	→	15
3₁(904)	→	905
3₁(932)	→	933
3₁(1432)	→	1433
3₁(1891)	→	1892
3₁(482)	→	483
3₁(1663)	→	1664
3₁(191)	→	192
3₁(629)	→	630
3₁(763)	→	764
3₁(43)	→	44
3₁(1269)	→	1270
3₁(16)	→	17
3₁(867)	→	868
3₁(1604)	→	1605
3₁(570)	→	571
3₁(457)	→	458
3₁(884)	→	885
3₁(1068)	→	1069
3₁(609)	→	610
3₁(1294)	→	1295
3₁(1124)	→	1125
3₁(10)	→	11
3₁(450)	→	451
3₁(1270)	→	1271
3₁(1333)	→	1334
3₁(646)	→	647
3₁(980)	→	981
3₁(875)	→	876
3₁(1664)	→	1665
3₁(762)	→	763
3₁(1662)	→	1663
3₁(1199)	→	1200
3₁(1260)	→	1261
3₁(981)	→	982
3₁(163)	→	164
3₁(465)	→	466
3₁(2082)	→	2083
3₁(755)	→	756
3₁(889)	→	890
3₁(978)	→	979
3₁(886)	→	887
3₁(897)	→	898
3₁(1602)	→	1603
3₁(628)	→	629
3₁(1258)	→	1259
3₁(639)	→	640
3₁(1075)	→	1076
3₁(1295)	→	1296
3₁(959)	→	960
3₁(201)	→	202
3₁(1078)	→	1079
2₁(296)	→	297
2₁(645)	→	646
2₁(160)	→	161
2₁(165)	→	166
2₁(1877)	→	1878
2₁(1203)	→	1204
2₁(399)	→	400
2₁(1412)	→	1413
2₁(1235)	→	1236
2₁(687)	→	688
2₁(876)	→	877
2₁(190)	→	191
2₁(616)	→	617
2₁(1066)	→	1067
2₁(1035)	→	1036
2₁(1266)	→	1267
2₁(1817)	→	1818
2₁(736)	→	737
2₁(1512)	→	1513
2₁(448)	→	449
2₁(420)	→	421
2₁(1490)	→	1491
2₁(806)	→	807
2₁(979)	→	980
2₁(882)	→	883
2₁(1366)	→	1367
2₁(1428)	→	1429
2₁(1325)	→	1326
2₁(1408)	→	1409
2₁(1402)	→	1403
2₁(753)	→	754
2₁(788)	→	789
2₁(622)	→	623
2₁(460)	→	461
2₁(877)	→	878
2₁(295)	→	296
2₁(613)	→	614
2₁(858)	→	859
2₁(566)	→	567
2₁(401)	→	402
2₁(289)	→	290
2₁(1193)	→	1194
2₁(620)	→	621
2₁(186)	→	187
2₁(356)	→	357
2₁(354)	→	355
2₁(161)	→	162
2₁(618)	→	619
2₁(378)	→	379
2₁(1450)	→	1451
2₁(429)	→	430
2₁(1856)	→	1857
2₁(614)	→	615
2₁(1197)	→	1198
2₁(1836)	→	1837
2₁(866)	→	867
2₁(1067)	→	1068
2₁(1120)	→	1121
2₁(632)	→	633
2₁(91)	→	92
2₁(164)	→	165
2₁(606)	→	607
2₁(1509)	→	1510
2₁(1234)	→	1235
2₁(380)	→	381
2₁(1277)	→	1278
2₁(430)	→	431
2₁(1204)	→	1205
2₁(810)	→	811
2₁(624)	→	625
2₁(1446)	→	1447
2₁(1195)	→	1196
2₁(1511)	→	1512
2₁(461)	→	462
2₁(565)	→	566
2₁(1505)	→	1506
2₁(1077)	→	1078
2₁(1321)	→	1322
2₁(15)	→	16
2₁(637)	→	638
2₁(1031)	→	1032
2₁(197)	→	198
2₁(1069)	→	1070
2₁(1317)	→	1318
2₁(87)	→	88
2₁(1177)	→	1178
2₁(1435)	→	1436
2₁(569)	→	570
2₁(719)	→	720
2₁(654)	→	655
2₁(962)	→	963
2₁(874)	→	875
2₁(1065)	→	1066
2₁(162)	→	163
2₁(1875)	→	1876
2₁(449)	→	450
3₂(1716)	→	1717
3₂(1014)	→	1015
3₂(1720)	→	1721
3₂(989)	→	990
3₂(964)	→	965
3₂(1735)	→	1736
3₂(1284)	→	1285
3₂(1732)	→	1733
3₂(1739)	→	1740
3₂(1044)	→	1045
3₂(991)	→	992
3₂(1139)	→	1140
3₂(1281)	→	1282
3₂(1020)	→	1021
3₂(1713)	→	1714
3₂(993)	→	994
3₂(1010)	→	1011
3₂(968)	→	969
3₂(1959)	→	1960
3₂(1016)	→	1017
3₂(1718)	→	1719
3₂(1819)	→	1820
3₂(1095)	→	1096
3₂(994)	→	995
3₂(965)	→	966
3₂(1027)	→	1028
3₂(1721)	→	1722
3₂(1021)	→	1022
3₂(1947)	→	1948
3₂(1708)	→	1709
3₂(1822)	→	1823
3₂(987)	→	988
3₂(972)	→	973
3₂(1733)	→	1734
3₂(1830)	→	1831
3₂(1961)	→	1962
3₂(1017)	→	1018
3₂(1712)	→	1713
3₂(1025)	→	1026
3₂(1103)	→	1104
3₂(1028)	→	1029
3₂(1826)	→	1827
3₂(1740)	→	1741
3₂(1023)	→	1024
3₂(1731)	→	1732
3₂(1012)	→	1013
3₂(973)	→	974
3₂(1096)	→	1097
3₂(986)	→	987
3₂(1009)	→	1010
3₂(1737)	→	1738
3₂(970)	→	971
3₂(1008)	→	1009
3₂(1099)	→	1100
3₂(1725)	→	1726
3₂(1141)	→	1142
3₂(985)	→	986
3₂(966)	→	967
3₂(1723)	→	1724
3₂(1951)	→	1952
3₂(1714)	→	1715
3₂(1283)	→	1284
3₂(1019)	→	1020
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
1₂(1022)	→	1023
1₂(1939)	→	1940
1₂(1013)	→	1014
1₂(1949)	→	1950
1₂(1159)	→	1160
1₂(1952)	→	1953
1₂(1823)	→	1824
1₂(1824)	→	1825
1₂(1803)	→	1804
1₂(1953)	→	1954
1₂(1144)	→	1145
1₂(1138)	→	1139
1₂(1285)	→	1286
1₂(969)	→	970
1₂(967)	→	968
1₂(1134)	→	1135
1₂(1011)	→	1012
1₂(988)	→	989
1₂(1827)	→	1828
1₂(1797)	→	1798
1₂(1715)	→	1716
1₂(1795)	→	1796
1₂(1948)	→	1949
1₂(990)	→	991
1₂(1848)	→	1849
1₂(1050)	→	1051
1₂(1133)	→	1134
1₂(1146)	→	1147
1₂(1049)	→	1050
1₂(1805)	→	1806
1₂(1736)	→	1737
1₂(1734)	→	1735
1₂(1717)	→	1718
1₂(1024)	→	1025
1₂(1279)	→	1280
1₂(1828)	→	1829

The automaton is closed under rewriting as it is compatible.