Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3786)

The rewrite relation of the following TRS is considered.

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

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

4(4(4(3(x1))))	→	2(3(3(2(5(3(3(0(1(5(x1))))))))))	(36)
3(1(3(5(x1))))	→	1(1(1(5(5(5(1(2(5(5(x1))))))))))	(37)
0(5(0(4(0(x1)))))	→	3(3(4(0(4(2(2(2(4(0(x1))))))))))	(38)
4(1(5(3(0(0(x1))))))	→	0(3(3(5(2(5(1(1(4(0(x1))))))))))	(39)
0(5(4(0(5(0(x1))))))	→	0(1(0(0(2(0(3(2(0(0(x1))))))))))	(40)
4(4(3(0(0(1(x1))))))	→	3(3(0(0(3(3(1(2(2(0(x1))))))))))	(41)
3(0(2(4(5(3(x1))))))	→	3(3(1(5(1(2(1(0(2(3(x1))))))))))	(42)
0(4(4(0(4(4(x1))))))	→	0(1(5(1(5(4(0(0(3(4(x1))))))))))	(43)
4(5(1(0(4(5(x1))))))	→	1(3(3(0(1(1(2(3(4(5(x1))))))))))	(44)
0(5(0(5(4(5(x1))))))	→	0(2(4(0(1(1(2(3(3(3(x1))))))))))	(45)
4(4(5(0(3(0(0(x1)))))))	→	2(4(0(2(1(3(3(1(5(5(x1))))))))))	(46)
3(4(5(1(3(0(0(x1)))))))	→	3(0(3(3(5(2(0(5(1(2(x1))))))))))	(47)
4(4(5(0(3(1(0(x1)))))))	→	5(3(0(5(4(3(3(3(1(0(x1))))))))))	(48)
4(4(2(2(0(4(0(x1)))))))	→	4(4(2(3(3(2(5(5(2(4(x1))))))))))	(49)
1(3(1(4(0(5(0(x1)))))))	→	0(0(3(5(4(3(2(1(0(0(x1))))))))))	(50)
4(5(3(4(3(5(0(x1)))))))	→	3(3(5(3(3(1(5(1(3(0(x1))))))))))	(51)
2(3(2(3(5(5(0(x1)))))))	→	1(4(3(5(5(4(3(5(5(0(x1))))))))))	(52)
0(4(4(1(4(3(1(x1)))))))	→	0(2(4(0(0(3(3(4(0(2(x1))))))))))	(53)
4(4(1(2(4(4(1(x1)))))))	→	0(1(3(0(5(0(1(1(5(3(x1))))))))))	(54)
0(1(4(5(1(1(2(x1)))))))	→	0(3(3(5(1(2(1(5(5(1(x1))))))))))	(55)
5(3(1(2(3(5(2(x1)))))))	→	1(1(5(5(4(3(4(3(3(5(x1))))))))))	(56)
4(4(5(1(0(1(3(x1)))))))	→	5(0(2(3(3(3(3(4(0(3(x1))))))))))	(57)
4(4(2(1(3(2(3(x1)))))))	→	5(4(0(3(1(5(2(5(2(3(x1))))))))))	(58)
4(4(2(3(4(4(3(x1)))))))	→	2(2(0(2(4(4(2(5(5(3(x1))))))))))	(59)
5(4(5(2(4(2(4(x1)))))))	→	5(3(1(4(3(4(5(1(5(0(x1))))))))))	(60)
2(3(5(3(2(3(4(x1)))))))	→	2(5(1(1(0(2(5(1(5(4(x1))))))))))	(61)
4(5(4(5(0(4(4(x1)))))))	→	4(5(1(2(3(3(4(2(0(2(x1))))))))))	(62)
2(1(4(2(4(5(4(x1)))))))	→	2(2(3(1(3(3(3(5(3(4(x1))))))))))	(63)
5(4(5(1(1(0(5(x1)))))))	→	1(5(4(1(4(0(3(1(1(5(x1))))))))))	(64)
4(5(4(2(3(0(5(x1)))))))	→	0(2(5(4(2(2(5(5(3(5(x1))))))))))	(65)
4(1(5(4(5(0(5(x1)))))))	→	2(5(5(1(5(0(0(0(1(2(x1))))))))))	(66)
5(0(4(4(4(3(5(x1)))))))	→	1(1(1(5(1(3(5(3(3(2(x1))))))))))	(67)
4(1(4(1(0(4(5(x1)))))))	→	5(3(0(0(1(4(0(2(3(3(x1))))))))))	(68)
1(0(5(2(1(4(5(x1)))))))	→	1(0(0(3(0(4(3(4(3(3(x1))))))))))	(69)
4(5(4(3(1(4(5(x1)))))))	→	4(0(5(5(5(5(2(4(2(3(x1))))))))))	(70)

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:

1182	→	575
1198	→	587
239	→	1
239	→	686
239	→	365
239	→	408
239	→	526
239	→	424
239	→	426
239	→	461
239	→	1569
366	→	704
366	→	986
1268	→	641
1602	→	575
364	→	1635
364	→	1647
494	→	1310
1652	→	729
457	→	426
534	→	975
534	→	1300
534	→	1338
964	→	1380
964	→	1394
633	→	4
633	→	665
633	→	65
633	→	588
633	→	603
633	→	673
633	→	456
633	→	117
633	→	624
633	→	67
633	→	566
633	→	1495
633	→	1470
1608	→	587
89	→	1298
89	→	1356
745	→	737
1513	→	265
1680	→	777
1333	→	95
1156	→	569
533	→	1326
1648	→	585
794	→	1617
794	→	1623
1624	→	624
1630	→	565
855	→	847
880	→	686
880	→	365
880	→	614
880	→	423
880	→	159
880	→	40
880	→	323
880	→	496
880	→	1
880	→	408
880	→	526
880	→	1569
1007	→	139
874	→	1350
10	→	712
1166	→	575
274	→	1
274	→	686
274	→	526
274	→	365
274	→	424
274	→	455
274	→	461
273	→	798
273	→	1471
1379	→	728
537	→	527
1638	→	565
487	→	463
1546	→	497
1688	→	1453
1284	→	649
743	→	631
1393	→	673
1393	→	636
1393	→	139
1393	→	456
1393	→	9
1393	→	620
1393	→	364
1393	→	192
1393	→	42
1393	→	325
1393	→	508
1393	→	4
1393	→	117
1393	→	624
1393	→	67
1393	→	566
1393	→	1453
1393	→	1495
1393	→	1470
1046	→	462
886	→	873
96	→	2
96	→	638
96	→	486
96	→	602
96	→	297
1642	→	585
933	→	686
933	→	526
933	→	1
933	→	365
933	→	424
1544	→	139
1606	→	575
326	→	297
326	→	462
326	→	600
882	→	872
882	→	1083
472	→	463
391	→	365
391	→	536
511	→	497
511	→	575
511	→	754
595	→	238
784	→	534
276	→	266
461	→	426
1575	→	527
1172	→	575
18	→	1
18	→	686
18	→	526
18	→	365
18	→	424
18	→	408
18	→	1569
547	→	881
547	→	1012
547	→	1029
365	→	538
365	→	686
365	→	1
978	→	368
1395	→	1385
41	→	9
41	→	634
41	→	813
1577	→	526
3	→	85
3	→	214
3	→	362
3	→	388
3	→	514
3	→	618
939	→	924
1003	→	462
1003	→	1448
1628	→	565
1634	→	565
213	→	160
213	→	5
213	→	193
213	→	1636
1011	→	139
617	→	605
617	→	1045
980	→	1651
1495	→	9
405	→	1629
405	→	1641
406	→	365
406	→	885
1678	→	737
646	→	524
646	→	904
298	→	647
298	→	777
298	→	979
9	→	139
9	→	460
9	→	636
1332	→	1621
5	→	66
5	→	194
5	→	345
5	→	405
5	→	510
5	→	604
1200	→	605
584	→	576
95	→	938
95	→	1179
95	→	1193
515	→	497
515	→	583
515	→	756
1190	→	587
1276	→	650
65	→	9
65	→	115
65	→	454
65	→	4
65	→	687
65	→	634
65	→	41
65	→	1453
65	→	1493
65	→	1466
1567	→	497
241	→	540
1618	→	605
1646	→	585
1636	→	565
1082	→	1071
1095	→	605
1095	→	616
1095	→	407
1095	→	212
1095	→	8
1095	→	296
1095	→	512
1095	→	6
1095	→	623
1095	→	551
1095	→	1125
892	→	873
193	→	160
495	→	17
1493	→	9
1	→	40
1	→	159
1	→	323
1	→	423
1	→	496
1	→	614
1078	→	534
1040	→	686
1040	→	526
1040	→	1
1040	→	365
1040	→	424
1009	→	139
654	→	524
305	→	785
305	→	1467
1299	→	668
1656	→	497
695	→	3
695	→	777
695	→	507
695	→	647
695	→	298
695	→	758
695	→	513
695	→	1656
695	→	1644
695	→	1646
695	→	1561
1022	→	234
645	→	1586
755	→	737
1509	→	231
1509	→	1574
601	→	588
969	→	1597
1626	→	640
524	→	973
524	→	1004
524	→	1675
1154	→	568
1713	→	17
1478	→	1453
505	→	305
548	→	6
548	→	605
548	→	623
548	→	551
548	→	1125
390	→	1631
390	→	1643
987	→	979
1345	→	705
884	→	873
1213	→	665
1213	→	65
1213	→	620
1213	→	364
1213	→	192
1213	→	42
1213	→	325
1213	→	508
1213	→	4
1213	→	588
1213	→	603
1515	→	265
761	→	737
970	→	168
1616	→	587
1194	→	587
423	→	1637
423	→	1649
323	→	1465
323	→	1492
1676	→	1658
573	→	944
573	→	1181
573	→	1189
735	→	17
1598	→	575
297	→	486
297	→	602
297	→	638
297	→	1124
86	→	9
86	→	137
86	→	458
1030	→	1019
556	→	272
1005	→	462
1005	→	1115
1005	→	1344
1005	→	1450
783	→	1070
1622	→	605
1212	→	1514
1212	→	1601
1212	→	1609
1709	→	624
161	→	231
161	→	1267
248	→	1010
248	→	1027
248	→	1081
924	→	1273
1499	→	9
619	→	605
702	→	1000
138	→	88
407	→	1633
407	→	1645
509	→	497
509	→	736
346	→	297
346	→	473
346	→	587
346	→	622
346	→	390
346	→	170
346	→	64
346	→	343
346	→	506
346	→	2
1339	→	1327
976	→	366
389	→	365
1084	→	1072
1311	→	1301
597	→	588
1610	→	587
171	→	160
639	→	977
6	→	8
6	→	212
6	→	296
6	→	407
6	→	512
6	→	616
116	→	88
1667	→	673
1667	→	566
345	→	1469
345	→	1494
823	→	814
799	→	786
1351	→	714
455	→	426
1282	→	648
498	→	728
249	→	5
249	→	565
249	→	516
249	→	240
249	→	160
249	→	193
249	→	213
249	→	1638
249	→	1634
363	→	297
363	→	475
363	→	596
613	→	248
615	→	605
615	→	1043
433	→	936
433	→	1171
433	→	1197
776	→	6
776	→	605
776	→	517
67	→	9
67	→	117
67	→	456
67	→	624
1180	→	575
525	→	1
525	→	686
525	→	526
525	→	365
525	→	424
525	→	408
525	→	1569
1596	→	455
1596	→	365
1596	→	461
853	→	565
853	→	516
853	→	240
853	→	5
853	→	160
853	→	193
853	→	1636
1188	→	587
2	→	64
2	→	170
2	→	343
2	→	390
2	→	506
2	→	622
814	→	1275
937	→	924
937	→	1265
1540	→	139
797	→	786
4	→	42
4	→	192
4	→	325
4	→	364
4	→	508
4	→	620
941	→	924
528	→	1283
118	→	88
344	→	297
344	→	471
463	→	762
463	→	768
1392	→	1516
1392	→	1603
1392	→	1611
1174	→	575
1650	→	585
212	→	1541
212	→	1560
212	→	1568
470	→	248
1501	→	9
1538	→	139
1451	→	777
1001	→	462
1001	→	1444
580	→	467
1108	→	542
820	→	1512
820	→	1605
820	→	1607
1217	→	624
1505	→	9
1461	→	1704
1461	→	1708
1470	→	1453
913	→	907
795	→	686
795	→	526
795	→	1
795	→	365
795	→	424
1094	→	1508
1094	→	1535
1094	→	1545
535	→	1
535	→	686
535	→	526
535	→	365
535	→	424
535	→	426
535	→	461
972	→	966
1692	→	297
306	→	2
306	→	346
306	→	550
306	→	324
306	→	366
1125	→	551
623	→	605
1536	→	139
1600	→	575
985	→	426
985	→	686
985	→	1
985	→	538
985	→	365
985	→	461
1705	→	605
497	→	585
497	→	760
497	→	846
169	→	5
169	→	565
169	→	516
169	→	240
169	→	160
169	→	193
169	→	1636
759	→	737
1604	→	575
140	→	88
140	→	488
140	→	1153
672	→	17
1517	→	265
1013	→	139
1559	→	497
1044	→	462
1632	→	565
694	→	1199
694	→	1203
621	→	605
757	→	737
295	→	266
295	→	1281
1202	→	605
635	→	625
635	→	1155
1686	→	777
719	→	632
64	→	1520
64	→	1655
681	→	4
681	→	636
681	→	139
681	→	9
681	→	687
681	→	634
681	→	41
681	→	1453
681	→	1493
681	→	1466
1307	→	433
1122	→	1477
1122	→	1504
637	→	625
637	→	720
1196	→	587
434	→	1
434	→	426
434	→	686
434	→	538
434	→	365
434	→	461
586	→	576
586	→	696
586	→	971
566	→	673
909	→	773
905	→	1087
821	→	638
821	→	486
821	→	622
821	→	390
821	→	170
821	→	64
821	→	343
821	→	506
821	→	2
821	→	602
821	→	297
17	→	1201
17	→	1216
1644	→	585
160	→	240
160	→	294
160	→	516
160	→	549
160	→	565
945	→	924
727	→	238
1569	→	526
1583	→	526
168	→	796
168	→	1463
1361	→	426
1361	→	686
1361	→	1
1361	→	538
1361	→	365
1361	→	461
424	→	365
424	→	526
424	→	883
424	→	1
1464	→	1453
1476	→	1453
464	→	1035
703	→	534
324	→	297
324	→	598
324	→	2
324	→	427
517	→	1107
215	→	160
215	→	275
974	→	585
974	→	1378
974	→	1384
1266	→	640
1360	→	1537
1360	→	1547
1360	→	1576
1093	→	1543
1093	→	1566
388	→	1627
388	→	1639
1445	→	777
1561	→	497
1472	→	1453
711	→	694
775	→	942
775	→	1165
775	→	1195
932	→	1475
932	→	1500
1028	→	1019
574	→	3
574	→	777
574	→	507
574	→	647
574	→	298
574	→	1656
574	→	1644
474	→	463
943	→	924
195	→	160
195	→	265
852	→	1452
852	→	1498
935	→	924
546	→	1006
546	→	1018
43	→	9
43	→	87
43	→	425
43	→	822
594	→	923
266	→	912
372	→	247
680	→	963
680	→	1002
507	→	497
507	→	744
476	→	463
1449	→	777
603	→	588
603	→	665
767	→	522
767	→	871
632	→	940
632	→	1173
632	→	1187
1612	→	587
1521	→	462
1521	→	1679
984	→	1510
984	→	1599
984	→	1615
539	→	527
539	→	854
1511	→	265
1511	→	1625
1468	→	1453
1274	→	640
1123	→	455
1123	→	365
1123	→	614
1123	→	423
1123	→	159
1123	→	40
1123	→	323
1123	→	496
1123	→	1
1123	→	461
599	→	588
1640	→	585
1381	→	728
1460	→	1712
1595	→	1687
1595	→	1689
1595	→	1691
1039	→	1518
1039	→	1533
1039	→	1657
238	→	1008
238	→	1023
238	→	1085
1466	→	1453
1462	→	686
1462	→	883
1462	→	365
1462	→	526
1462	→	424
408	→	365
408	→	891
1024	→	1019
1542	→	139
459	→	426
247	→	934
1086	→	1071
879	→	1539
879	→	1558
879	→	1582
1548	→	497
1534	→	462
1534	→	1685
1690	→	9
513	→	497
513	→	758
1519	→	298
1519	→	1677
2₁(529)	→	530
2₁(1328)	→	1329
2₁(694)	→	695
2₁(1599)	→	1600
2₁(1645)	→	1646
2₁(905)	→	906
2₁(700)	→	701
2₁(644)	→	645
2₁(234)	→	235
2₁(17)	→	18
2₁(1332)	→	1333
2₁(1165)	→	1166
2₁(265)	→	266
2₁(538)	→	539
2₁(88)	→	89
2₁(778)	→	779
2₁(1074)	→	1075
2₁(689)	→	690
2₁(963)	→	964
2₁(532)	→	533
2₁(526)	→	527
2₁(1545)	→	1546
2₁(671)	→	672
2₁(1566)	→	1567
2₁(1356)	→	1357
2₁(710)	→	711
2₁(1173)	→	1174
2₁(1359)	→	1360
2₁(1560)	→	1561
2₁(1023)	→	1024
2₁(1444)	→	1445
2₁(1597)	→	1598
2₁(847)	→	848
2₁(666)	→	667
2₁(696)	→	697
2₁(506)	→	507
2₁(908)	→	909
2₁(791)	→	792
2₁(846)	→	847
2₁(822)	→	823
2₁(966)	→	967
2₁(1655)	→	1656
2₁(1639)	→	1640
2₁(1685)	→	1686
2₁(854)	→	855
2₁(875)	→	876
2₁(275)	→	276
2₁(1679)	→	1680
2₁(510)	→	511
2₁(1448)	→	1449
2₁(1107)	→	1108
2₁(1643)	→	1644
2₁(496)	→	497
2₁(1326)	→	1327
2₁(1018)	→	1019
2₁(1649)	→	1650
2₁(762)	→	763
2₁(1450)	→	1451
2₁(163)	→	164
2₁(1558)	→	1559
2₁(1171)	→	1172
2₁(508)	→	509
2₁(427)	→	428
2₁(986)	→	987
2₁(266)	→	267
2₁(1071)	→	1072
2₁(1641)	→	1642
2₁(512)	→	513
2₁(1283)	→	1284
2₁(469)	→	470
2₁(1574)	→	1575
2₁(297)	→	298
2₁(541)	→	542
2₁(1601)	→	1602
2₁(1603)	→	1604
2₁(1605)	→	1606
2₁(1338)	→	1339
2₁(536)	→	537
2₁(608)	→	609
2₁(241)	→	242
2₁(464)	→	465
2₁(723)	→	724
2₁(14)	→	15
2₁(813)	→	814
2₁(794)	→	795
2₁(925)	→	926
2₁(1547)	→	1548
2₁(514)	→	515
2₁(1647)	→	1648
2₁(726)	→	727
2₁(294)	→	295
2₁(1518)	→	1519
2₁(648)	→	649
2₁(300)	→	301
2₁(722)	→	723
2₁(1027)	→	1028
2₁(669)	→	670
2₁(1088)	→	1089
2₁(1077)	→	1078
2₁(1179)	→	1180
2₁(244)	→	245
2₁(500)	→	501
2₁(924)	→	925
2₁(1083)	→	1084
2₁(973)	→	974
2₁(162)	→	163
2₁(1181)	→	1182
2₁(1029)	→	1030
2₁(492)	→	493
2₁(161)	→	162
5₂(1477)	→	1478
5₂(1469)	→	1470
5₂(1465)	→	1466
5₂(1452)	→	1453
5₂(1471)	→	1472
5₂(1593)	→	1594
5₂(1475)	→	1476
5₂(1589)	→	1590
5₂(1467)	→	1468
5₂(1660)	→	1661
5₂(1663)	→	1664
5₂(1687)	→	1688
5₂(1457)	→	1458
5₂(1463)	→	1464
1₂(1662)	→	1663
1₂(1588)	→	1589
1₂(1666)	→	1667
1₂(1590)	→	1591
1₂(1665)	→	1666
1₂(1664)	→	1665
1₂(1453)	→	1454
1₁(616)	→	617
1₁(429)	→	430
1₁(618)	→	619
1₁(247)	→	248
1₁(716)	→	717
1₁(926)	→	927
1₁(428)	→	429
1₁(1124)	→	1125
1₁(93)	→	94
1₁(540)	→	541
1₁(433)	→	434
1₁(1392)	→	1393
1₁(465)	→	466
1₁(303)	→	304
1₁(650)	→	651
1₁(1117)	→	1118
1₁(491)	→	492
1₁(818)	→	819
1₁(1201)	→	1202
1₁(267)	→	268
1₁(9)	→	10
1₁(814)	→	815
1₁(1380)	→	1381
1₁(1211)	→	1212
1₁(594)	→	595
1₁(708)	→	709
1₁(820)	→	821
1₁(589)	→	590
1₁(819)	→	820
1₁(775)	→	776
1₁(979)	→	980
1₁(1388)	→	1389
1₁(1704)	→	1705
1₁(712)	→	713
1₁(967)	→	968
1₁(1391)	→	1392
1₁(622)	→	623
1₁(691)	→	692
1₁(885)	→	886
1₁(1087)	→	1088
1₁(620)	→	621
1₁(1617)	→	1618
1₁(607)	→	608
1₁(604)	→	605
1₁(370)	→	371
1₁(687)	→	688
1₁(965)	→	966
1₁(673)	→	674
1₁(232)	→	233
1₁(552)	→	553
1₁(1212)	→	1213
1₁(497)	→	498
1₁(94)	→	95
1₁(765)	→	766
1₁(1621)	→	1622
1₁(883)	→	884
1₁(872)	→	873
1₁(1019)	→	1020
1₁(1390)	→	1391
1₁(891)	→	892
1₁(89)	→	90
1₁(614)	→	615
1₁(678)	→	679
1₁(488)	→	489
1₁(732)	→	733
1₁(550)	→	551
1₁(873)	→	874
1₁(742)	→	743
1₁(95)	→	96
1₁(632)	→	633
1₁(466)	→	467
1₁(969)	→	970
1₁(631)	→	632
1₁(740)	→	741
1₁(701)	→	702
1₁(573)	→	574
1₁(588)	→	589
1₁(980)	→	981
1₁(1302)	→	1303
1₁(786)	→	787
1₁(299)	→	300
1₁(971)	→	972
1₁(1115)	→	1116
1₁(516)	→	517
1₁(1199)	→	1200
1₁(231)	→	232
1₁(609)	→	610
1₁(301)	→	302
1₁(984)	→	985
1₁(1378)	→	1379
1₁(692)	→	693
0₀(3)	→	5
0₀(6)	→	5
0₀(5)	→	5
0₀(4)	→	5
0₀(2)	→	5
0₀(1)	→	5
1₀(2)	→	6
1₀(6)	→	6
1₀(4)	→	6
1₀(1)	→	6
1₀(3)	→	6
1₀(5)	→	6
0₂(1586)	→	1587
0₂(1454)	→	1455
5₀(1)	→	4
5₀(6)	→	4
5₀(3)	→	4
5₀(5)	→	4
5₀(2)	→	4
5₀(4)	→	4
4₁(677)	→	678
4₁(1035)	→	1036
4₁(423)	→	424
4₁(626)	→	627
4₁(364)	→	365
4₁(160)	→	161
4₁(533)	→	534
4₁(1155)	→	1156
4₁(717)	→	718
4₁(881)	→	882
4₁(667)	→	668
4₁(164)	→	165
4₁(1329)	→	1330
4₁(764)	→	765
4₁(628)	→	629
4₁(871)	→	872
4₁(697)	→	698
4₁(368)	→	369
4₁(850)	→	851
4₁(407)	→	408
4₁(1206)	→	1207
4₁(1306)	→	1307
4₁(770)	→	771
4₁(1081)	→	1082
4₁(458)	→	459
4₁(1208)	→	1209
4₁(572)	→	573
4₁(543)	→	544
4₁(494)	→	495
4₁(576)	→	577
4₁(390)	→	391
4₁(1265)	→	1266
4₁(534)	→	535
4₁(1576)	→	1577
4₁(166)	→	167
4₁(653)	→	654
4₁(1070)	→	1071
4₁(468)	→	469
4₁(848)	→	849
4₁(1090)	→	1091
4₁(568)	→	569
4₁(777)	→	778
4₁(1508)	→	1509
4₁(454)	→	455
4₁(724)	→	725
4₁(1625)	→	1626
4₁(1298)	→	1299
4₁(1357)	→	1358
4₁(425)	→	426
4₁(668)	→	669
4₁(405)	→	406
4₁(1304)	→	1305
4₁(1568)	→	1569
4₁(460)	→	461
4₁(1085)	→	1086
4₁(520)	→	521
4₁(715)	→	716
4₁(639)	→	640
4₁(768)	→	769
4₁(1582)	→	1583
4₁(388)	→	389
4₁(1273)	→	1274
4₁(456)	→	457
4₁(675)	→	676
0₁(1631)	→	1632
0₁(1300)	→	1301
0₁(1310)	→	1311
0₁(936)	→	937
0₁(934)	→	935
0₁(1629)	→	1630
0₁(1093)	→	1094
0₁(923)	→	924
0₁(366)	→	367
0₁(467)	→	468
0₁(730)	→	731
0₁(1510)	→	1511
0₁(690)	→	691
0₁(1094)	→	1095
0₁(849)	→	850
0₁(592)	→	593
0₁(1627)	→	1628
0₁(575)	→	576
0₁(579)	→	580
0₁(929)	→	930
0₁(728)	→	729
0₁(771)	→	772
0₁(493)	→	494
0₁(930)	→	931
0₁(1512)	→	1513
0₁(270)	→	271
0₁(238)	→	239
0₁(1633)	→	1634
0₁(670)	→	671
0₁(766)	→	767
0₁(243)	→	244
0₁(1635)	→	1636
0₁(942)	→	943
0₁(194)	→	195
0₁(879)	→	880
0₁(214)	→	215
0₁(590)	→	591
0₁(964)	→	965
0₁(1037)	→	1038
0₁(165)	→	166
0₁(1651)	→	1652
0₁(645)	→	646
0₁(547)	→	548
0₁(212)	→	213
0₁(907)	→	908
0₁(499)	→	500
0₁(192)	→	193
0₁(504)	→	505
0₁(938)	→	939
0₁(583)	→	584
0₁(522)	→	523
0₁(240)	→	241
0₁(245)	→	246
0₁(1516)	→	1517
0₁(783)	→	784
0₁(944)	→	945
0₁(1514)	→	1515
0₁(940)	→	941
0₁(430)	→	431
0₁(774)	→	775
0₁(904)	→	905
0₁(170)	→	171
0₁(271)	→	272
0₁(1327)	→	1328
0₁(729)	→	730
0₁(298)	→	299
0₁(367)	→	368
0₁(1021)	→	1022
0₁(1637)	→	1638
0₁(977)	→	978
0₁(546)	→	547
0₁(1360)	→	1361
0₁(10)	→	11
0₁(652)	→	653
0₁(787)	→	788
0₁(585)	→	586
0₁(714)	→	715
0₁(638)	→	639
0₁(773)	→	774
0₁(159)	→	160
0₁(246)	→	247
0₁(248)	→	249
0₁(981)	→	982
0₁(763)	→	764
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₁(627)	→	628
3₁(1187)	→	1188
3₁(707)	→	708
3₁(1122)	→	1123
3₁(237)	→	238
3₁(463)	→	464
3₁(758)	→	759
3₁(431)	→	432
3₁(1330)	→	1331
3₁(912)	→	913
3₁(1205)	→	1206
3₁(530)	→	531
3₁(523)	→	524
3₁(928)	→	929
3₁(489)	→	490
3₁(1609)	→	1610
3₁(345)	→	346
3₁(365)	→	366
3₁(362)	→	363
3₁(640)	→	641
3₁(1394)	→	1395
3₁(1607)	→	1608
3₁(975)	→	976
3₁(272)	→	273
3₁(305)	→	306
3₁(15)	→	16
3₁(1615)	→	1616
3₁(1611)	→	1612
3₁(432)	→	433
3₁(1002)	→	1003
3₁(490)	→	491
3₁(1331)	→	1332
3₁(624)	→	625
3₁(1387)	→	1388
3₁(709)	→	710
3₁(475)	→	476
3₁(531)	→	532
3₁(1004)	→	1005
3₁(636)	→	637
3₁(471)	→	472
3₁(473)	→	474
3₁(462)	→	463
3₁(1520)	→	1521
3₁(1045)	→	1046
3₁(676)	→	677
3₁(12)	→	13
3₁(1350)	→	1351
3₁(878)	→	879
3₁(554)	→	555
3₁(851)	→	852
3₁(1153)	→	1154
3₁(167)	→	168
3₁(578)	→	579
3₁(1267)	→	1268
3₁(788)	→	789
3₁(982)	→	983
3₁(325)	→	326
3₁(549)	→	550
3₁(641)	→	642
3₁(1305)	→	1306
3₁(906)	→	907
3₁(502)	→	503
3₁(612)	→	613
3₁(168)	→	169
3₁(698)	→	699
3₁(1385)	→	1386
3₁(343)	→	344
3₁(1189)	→	1190
3₁(567)	→	568
3₁(1533)	→	1534
3₁(643)	→	644
3₁(242)	→	243
3₁(1118)	→	1119
3₁(1677)	→	1678
3₁(304)	→	305
3₁(744)	→	745
3₁(932)	→	933
3₁(518)	→	519
3₁(611)	→	612
3₁(1076)	→	1077
3₁(772)	→	773
3₁(705)	→	706
3₁(517)	→	518
3₁(1038)	→	1039
3₁(323)	→	324
3₁(426)	→	427
3₁(651)	→	652
3₁(1043)	→	1044
3₁(1193)	→	1194
3₁(927)	→	928
3₁(1197)	→	1198
3₁(1712)	→	1713
3₁(268)	→	269
3₁(1384)	→	1385
3₁(273)	→	274
3₁(983)	→	984
3₁(852)	→	853
3₁(756)	→	757
3₁(269)	→	270
3₁(296)	→	297
3₁(519)	→	520
3₁(545)	→	546
3₁(634)	→	635
3₁(16)	→	17
3₁(542)	→	543
3₁(11)	→	12
3₁(577)	→	578
3₁(1119)	→	1120
3₁(1092)	→	1093
3₁(593)	→	594
3₁(625)	→	626
3₁(1207)	→	1208
3₁(769)	→	770
3₁(760)	→	761
3₁(699)	→	700
3₁(754)	→	755
3₁(736)	→	737
3₁(1195)	→	1196
3₁(792)	→	793
3₁(877)	→	878
3₁(793)	→	794
3₁(553)	→	554
3₁(236)	→	237
3₁(737)	→	738
3₁(713)	→	714
3₁(571)	→	572
3₁(1204)	→	1205
3₁(706)	→	707
3₁(931)	→	932
3₁(789)	→	790
3₁(1121)	→	1122
3₁(642)	→	643
3₁(679)	→	680
3₁(1691)	→	1692
3₁(739)	→	740
3₁(1000)	→	1001
3₁(1089)	→	1090
3₁(486)	→	487
3₁(1075)	→	1076
3₁(503)	→	504
5₁(235)	→	236
5₁(1492)	→	1493
5₁(1494)	→	1495
5₁(570)	→	571
5₁(1203)	→	1204
5₁(64)	→	65
5₁(704)	→	705
5₁(1116)	→	1117
5₁(92)	→	93
5₁(815)	→	816
5₁(876)	→	877
5₁(596)	→	597
5₁(686)	→	687
5₁(40)	→	41
5₁(600)	→	601
5₁(551)	→	552
5₁(780)	→	781
5₁(498)	→	499
5₁(1209)	→	1210
5₁(665)	→	666
5₁(371)	→	372
5₁(798)	→	799
5₁(591)	→	592
5₁(115)	→	116
5₁(647)	→	648
5₁(779)	→	780
5₁(649)	→	650
5₁(796)	→	797
5₁(610)	→	611
5₁(781)	→	782
5₁(528)	→	529
5₁(524)	→	525
5₁(1073)	→	1074
5₁(718)	→	719
5₁(1301)	→	1302
5₁(137)	→	138
5₁(501)	→	502
5₁(66)	→	67
5₁(731)	→	732
5₁(1072)	→	1073
5₁(1344)	→	1345
5₁(1358)	→	1359
5₁(1091)	→	1092
5₁(1020)	→	1021
5₁(566)	→	567
5₁(738)	→	739
5₁(785)	→	786
5₁(521)	→	522
5₁(1389)	→	1390
5₁(13)	→	14
5₁(680)	→	681
5₁(629)	→	630
5₁(1275)	→	1276
5₁(1708)	→	1709
5₁(598)	→	599
5₁(968)	→	969
5₁(817)	→	818
5₁(1543)	→	1544
5₁(42)	→	43
5₁(90)	→	91
5₁(1281)	→	1282
5₁(688)	→	689
5₁(85)	→	86
5₁(602)	→	603
5₁(1541)	→	1542
5₁(733)	→	734
5₁(1039)	→	1040
5₁(1120)	→	1121
5₁(790)	→	791
5₁(91)	→	92
5₁(1210)	→	1211
5₁(606)	→	607
5₁(587)	→	588
5₁(527)	→	528
5₁(605)	→	606
5₁(139)	→	140
5₁(1498)	→	1499
5₁(233)	→	234
5₁(544)	→	545
5₁(1303)	→	1304
5₁(565)	→	566
5₁(674)	→	675
5₁(1689)	→	1690
5₁(702)	→	703
5₁(741)	→	742
5₁(816)	→	817
5₁(1623)	→	1624
5₁(1216)	→	1217
5₁(302)	→	303
5₁(1537)	→	1538
5₁(1012)	→	1013
5₁(734)	→	735
5₁(721)	→	722
5₁(1036)	→	1037
5₁(87)	→	88
5₁(369)	→	370
5₁(1008)	→	1009
5₁(1010)	→	1011
5₁(569)	→	570
5₁(117)	→	118
5₁(1504)	→	1505
5₁(555)	→	556
5₁(874)	→	875
5₁(1386)	→	1387
5₁(1535)	→	1536
5₁(782)	→	783
5₁(725)	→	726
5₁(693)	→	694
5₁(630)	→	631
5₁(1539)	→	1540
5₁(8)	→	9
5₁(1500)	→	1501
5₁(720)	→	721
5₁(1006)	→	1007
2₂(1657)	→	1658
2₂(1675)	→	1676
2₂(1461)	→	1462
2₂(1458)	→	1459
4₀(1)	→	1
4₀(6)	→	1
4₀(5)	→	1
4₀(2)	→	1
4₀(3)	→	1
4₀(4)	→	1
3₂(1661)	→	1662
3₂(1594)	→	1595
3₂(1591)	→	1592
3₂(1587)	→	1588
3₂(1592)	→	1593
3₂(1659)	→	1660
3₂(1459)	→	1460
3₂(1455)	→	1456
3₂(1658)	→	1659
3₂(1456)	→	1457
3₂(1595)	→	1596
3₂(1460)	→	1461

The automaton is closed under rewriting as it is compatible.