Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/5109)

The rewrite relation of the following TRS is considered.

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

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

1(0(0(0(x1))))	→	5(0(4(2(2(4(2(2(3(2(x1))))))))))	(52)
0(5(0(1(x1))))	→	1(1(2(2(4(4(4(2(2(1(x1))))))))))	(53)
4(1(0(3(0(x1)))))	→	4(1(5(5(0(4(2(4(2(2(x1))))))))))	(54)
0(1(0(4(0(x1)))))	→	5(3(3(1(1(1(1(5(0(2(x1))))))))))	(55)
1(0(0(5(0(x1)))))	→	5(1(3(4(4(1(1(1(5(0(x1))))))))))	(56)
2(5(4(3(0(0(x1))))))	→	1(1(2(4(1(4(2(4(3(2(x1))))))))))	(57)
5(2(5(3(0(0(x1))))))	→	5(3(2(5(2(2(1(1(4(2(x1))))))))))	(58)
0(1(5(4(0(0(x1))))))	→	1(1(4(2(1(3(4(4(1(3(x1))))))))))	(59)
4(1(5(4(0(0(x1))))))	→	4(5(0(2(4(1(4(2(4(3(x1))))))))))	(60)
3(5(5(4(1(0(x1))))))	→	4(2(3(0(5(4(4(4(2(2(x1))))))))))	(61)
5(2(0(0(3(0(x1))))))	→	5(2(5(2(4(2(3(0(4(2(x1))))))))))	(62)
2(2(0(0(4(0(x1))))))	→	2(2(0(3(2(3(0(4(2(2(x1))))))))))	(63)
2(0(1(3(4(0(x1))))))	→	2(5(3(0(1(1(4(2(2(2(x1))))))))))	(64)
4(3(0(0(5(0(x1))))))	→	4(2(2(5(4(1(0(2(4(2(x1))))))))))	(65)
1(4(3(0(5(0(x1))))))	→	1(3(1(3(4(1(2(3(4(2(x1))))))))))	(66)
2(0(0(0(5(1(x1))))))	→	4(2(2(5(1(5(5(1(1(1(x1))))))))))	(67)
1(4(0(5(5(1(x1))))))	→	1(2(3(3(4(2(4(4(1(1(x1))))))))))	(68)
4(5(4(0(1(2(x1))))))	→	4(3(3(2(0(1(2(4(2(2(x1))))))))))	(69)
0(5(0(0(1(4(x1))))))	→	1(5(1(1(4(4(1(5(1(4(x1))))))))))	(70)
2(2(3(0(5(4(x1))))))	→	2(4(2(2(5(2(4(2(2(4(x1))))))))))	(71)
5(4(0(0(0(5(x1))))))	→	5(3(4(4(1(1(4(5(0(5(x1))))))))))	(72)
0(0(5(3(0(5(x1))))))	→	5(5(1(1(5(1(3(2(2(5(x1))))))))))	(73)
0(5(0(4(0(5(x1))))))	→	0(2(4(4(2(4(4(4(5(0(x1))))))))))	(74)
4(4(5(4(0(5(x1))))))	→	2(4(1(4(4(4(2(5(1(2(x1))))))))))	(75)
0(5(5(3(1(5(x1))))))	→	1(4(4(4(5(1(2(3(2(5(x1))))))))))	(76)
2(1(0(5(2(5(x1))))))	→	4(2(5(1(0(4(2(4(2(5(x1))))))))))	(77)
5(0(4(3(0(0(0(x1)))))))	→	5(1(1(5(1(1(4(5(1(0(x1))))))))))	(78)
4(0(5(4(3(0(0(x1)))))))	→	3(5(3(5(4(5(1(1(2(3(x1))))))))))	(79)
3(5(0(3(0(1(0(x1)))))))	→	3(5(5(3(4(1(2(0(2(2(x1))))))))))	(80)
2(4(3(1(3(1(0(x1)))))))	→	4(5(1(1(1(1(2(4(4(5(x1))))))))))	(81)
5(0(3(0(5(2(0(x1)))))))	→	5(1(1(0(0(4(2(5(4(2(x1))))))))))	(82)
1(0(4(0(2(3(0(x1)))))))	→	1(3(1(4(2(4(0(0(2(3(x1))))))))))	(83)
3(0(0(2(5(3(0(x1)))))))	→	3(2(4(3(4(3(3(2(0(2(x1))))))))))	(84)
2(0(4(0(3(5(0(x1)))))))	→	4(1(2(3(1(5(0(1(2(2(x1))))))))))	(85)
0(5(2(2(3(5(0(x1)))))))	→	1(5(1(4(2(2(1(2(3(2(x1))))))))))	(86)
0(4(0(1(0(0(1(x1)))))))	→	5(4(5(1(2(2(3(1(4(1(x1))))))))))	(87)
2(1(1(4(0(0(1(x1)))))))	→	2(1(4(5(0(2(0(4(2(2(x1))))))))))	(88)
4(0(1(1(1(0(1(x1)))))))	→	2(0(3(3(0(4(1(1(4(1(x1))))))))))	(89)
5(0(5(4(1(0(1(x1)))))))	→	5(1(0(1(4(1(1(1(1(4(x1))))))))))	(90)
0(5(4(5(4(0(1(x1)))))))	→	1(1(3(5(2(0(2(1(2(2(x1))))))))))	(91)
3(3(1(4(5(3(1(x1)))))))	→	3(3(5(1(1(0(2(4(4(1(x1))))))))))	(92)
5(0(3(0(0(5(1(x1)))))))	→	5(1(5(5(0(5(1(4(1(1(x1))))))))))	(93)
1(0(3(3(1(5(2(x1)))))))	→	5(5(5(4(2(3(4(3(1(2(x1))))))))))	(94)
4(3(0(1(0(0(4(x1)))))))	→	0(2(5(5(1(3(3(2(3(4(x1))))))))))	(95)
4(0(0(0(0(0(5(x1)))))))	→	2(3(2(1(1(3(1(2(4(2(x1))))))))))	(96)
2(5(2(1(0(0(5(x1)))))))	→	2(5(4(5(1(2(2(0(2(5(x1))))))))))	(97)
4(0(1(3(0(0(5(x1)))))))	→	1(2(4(3(4(3(4(2(1(3(x1))))))))))	(98)
4(3(0(1(5(0(5(x1)))))))	→	5(1(4(2(2(2(1(4(5(5(x1))))))))))	(99)
4(3(4(0(0(1(5(x1)))))))	→	4(4(5(2(2(3(2(3(4(5(x1))))))))))	(100)
0(0(4(0(3(1(5(x1)))))))	→	5(3(2(2(5(4(1(4(1(5(x1))))))))))	(101)
2(4(0(1(0(2(5(x1)))))))	→	2(1(4(1(1(4(1(1(5(2(x1))))))))))	(102)

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	→	486
157	→	424
157	→	733
157	→	784
157	→	941
157	→	285
157	→	156
157	→	685
157	→	5
157	→	9
157	→	932
157	→	67
1400	→	821
871	→	943
871	→	1034
871	→	1307
322	→	296
793	→	1241
846	→	740
1525	→	1516
869	→	1536
200	→	17
200	→	1101
1573	→	602
1579	→	296
1703	→	296
1674	→	462
454	→	164
1529	→	920
750	→	486
1333	→	181
1762	→	853
791	→	486
860	→	17
87	→	478
87	→	797
87	→	1276
732	→	4
732	→	863
732	→	516
732	→	539
1697	→	517
1089	→	448
1624	→	1210
1072	→	425
286	→	396
286	→	447
286	→	455
286	→	759
286	→	1433
10	→	258
1166	→	521
1487	→	447
181	→	1561
181	→	1578
181	→	1657
487	→	5
487	→	941
487	→	285
487	→	156
487	→	9
487	→	65
487	→	695
487	→	88
487	→	939
487	→	42
487	→	44
487	→	366
487	→	578
1248	→	708
1546	→	1537
915	→	4
915	→	863
915	→	516
915	→	365
915	→	559
1736	→	293
1736	→	1761
294	→	3
294	→	924
294	→	757
294	→	942
294	→	667
294	→	906
294	→	601
294	→	753
294	→	646
294	→	755
294	→	193
294	→	648
294	→	603
294	→	164
294	→	1658
1560	→	9
578	→	1138
448	→	883
448	→	1255
96	→	2
96	→	714
96	→	602
96	→	192
96	→	257
96	→	216
303	→	94
608	→	292
1544	→	904
1593	→	192
1597	→	192
998	→	197
995	→	1596
995	→	1619
995	→	1708
811	→	422
706	→	95
1575	→	1564
668	→	699
668	→	707
668	→	890
1670	→	156
1172	→	605
1172	→	1524
1532	→	1594
1532	→	1617
1532	→	1704
610	→	601
610	→	751
585	→	422
1589	→	157
18	→	1
18	→	117
18	→	715
1141	→	157
1577	→	296
3	→	84
3	→	114
3	→	256
3	→	362
3	→	556
3	→	628
1506	→	1493
1246	→	9
988	→	1338
218	→	192
1254	→	712
1734	→	933
1033	→	782
1102	→	1136
1011	→	941
1011	→	285
1011	→	156
1011	→	668
1011	→	5
1011	→	9
1011	→	85
1114	→	1102
1531	→	864
838	→	94
626	→	1598
626	→	1623
626	→	1710
805	→	189
805	→	1167
1678	→	462
646	→	601
646	→	753
1359	→	800
1359	→	1456
9	→	156
9	→	181
9	→	285
9	→	697
9	→	941
9	→	668
9	→	85
914	→	1111
914	→	1183
914	→	1222
914	→	1503
5	→	66
5	→	134
5	→	235
5	→	342
5	→	540
5	→	600
931	→	188
341	→	296
341	→	626
341	→	295
341	→	136
341	→	8
341	→	191
341	→	558
341	→	6
341	→	363
95	→	1374
95	→	1421
698	→	686
698	→	861
1076	→	285
1076	→	1346
1076	→	1352
65	→	9
1055	→	397
1618	→	1210
1664	→	10
1139	→	492
973	→	714
973	→	602
973	→	647
973	→	340
973	→	116
973	→	64
973	→	233
973	→	538
973	→	2
973	→	192
973	→	257
756	→	743
696	→	686
696	→	853
889	→	693
674	→	1134
1110	→	941
1110	→	285
1110	→	156
1110	→	5
1110	→	9
1110	→	65
1662	→	784
193	→	676
495	→	462
495	→	1140
293	→	1187
293	→	1226
293	→	1507
713	→	485
942	→	933
1164	→	518
938	→	809
1601	→	1698
1601	→	1733
1599	→	192
1162	→	519
1	→	41
1	→	154
1	→	215
1	→	321
1	→	575
1	→	609
1726	→	293
1726	→	1747
1726	→	1753
1010	→	1563
1010	→	1669
1010	→	1673
1010	→	1679
1591	→	192
1656	→	164
165	→	4
165	→	839
165	→	863
165	→	516
165	→	576
165	→	798
165	→	926
165	→	365
165	→	559
165	→	916
165	→	743
165	→	754
165	→	758
165	→	557
1489	→	8
1331	→	285
1112	→	1102
601	→	667
601	→	757
601	→	906
601	→	924
940	→	933
1223	→	1210
524	→	95
524	→	1245
1317	→	44
1317	→	5
1317	→	366
1317	→	578
1319	→	1308
428	→	1332
390	→	969
1345	→	785
44	→	9
44	→	600
44	→	342
44	→	134
44	→	66
44	→	235
44	→	540
44	→	5
884	→	1142
1283	→	674
480	→	997
135	→	87
677	→	1171
796	→	522
1329	→	760
687	→	1161
423	→	5
423	→	784
423	→	424
423	→	941
423	→	285
423	→	156
423	→	685
423	→	9
423	→	932
423	→	67
423	→	733
423	→	157
423	→	65
423	→	695
423	→	88
423	→	939
423	→	42
423	→	44
423	→	578
423	→	669
423	→	1562
1676	→	462
1137	→	489
343	→	296
297	→	897
297	→	1173
1428	→	462
296	→	364
296	→	723
675	→	189
1414	→	462
1373	→	156
518	→	1441
1353	→	10
783	→	740
1709	→	296
161	→	1253
1170	→	484
1277	→	716
824	→	1330
1339	→	777
976	→	1038
976	→	1056
257	→	192
1699	→	447
1610	→	840
1610	→	1435
1610	→	577
1610	→	4
1610	→	744
1610	→	863
1610	→	516
1610	→	1436
648	→	601
648	→	755
6	→	8
6	→	136
6	→	191
6	→	295
6	→	558
6	→	626
1256	→	160
627	→	601
627	→	742
627	→	942
627	→	3
627	→	164
627	→	1658
741	→	6
741	→	723
741	→	296
741	→	363
741	→	341
741	→	1711
799	→	819
1186	→	1176
1351	→	793
1037	→	296
431	→	422
1701	→	296
1585	→	164
1585	→	1696
363	→	296
764	→	720
1168	→	578
67	→	9
67	→	685
67	→	932
67	→	1589
1242	→	703
923	→	164
717	→	1488
951	→	1580
1188	→	1176
1672	→	156
117	→	87
2	→	64
2	→	116
2	→	233
2	→	340
2	→	538
2	→	647
1060	→	683
872	→	4
872	→	863
872	→	516
872	→	365
872	→	559
11	→	792
979	→	674
1347	→	784
4	→	43
4	→	86
4	→	217
4	→	323
4	→	515
4	→	645
265	→	1380
265	→	1427
265	→	1574
265	→	1694
463	→	1
463	→	826
463	→	797
463	→	478
463	→	87
463	→	517
463	→	117
463	→	715
1504	→	1493
1174	→	672
1650	→	1572
827	→	1399
1711	→	296
1501	→	1586
1501	→	1675
557	→	516
479	→	488
479	→	1115
1035	→	296
904	→	1148
904	→	1419
754	→	743
754	→	1522
1587	→	157
1535	→	17
1748	→	158
16	→	1075
862	→	854
516	→	577
516	→	863
516	→	1435
1045	→	723
1045	→	296
1045	→	626
1045	→	295
1045	→	136
1045	→	8
1045	→	191
1045	→	558
1045	→	6
1045	→	363
972	→	1671
972	→	1677
925	→	1001
684	→	2
684	→	714
684	→	602
684	→	192
684	→	257
1705	→	296
1143	→	511
559	→	516
1436	→	840
85	→	9
1533	→	714
1533	→	2
1533	→	192
1533	→	234
514	→	164
1219	→	863
1219	→	744
1219	→	645
1219	→	323
1219	→	86
1219	→	43
1219	→	217
1219	→	515
1219	→	4
1219	→	577
1219	→	516
1219	→	840
1219	→	1436
236	→	192
944	→	974
944	→	987
944	→	1027
1091	→	456
694	→	4
694	→	863
694	→	744
694	→	577
694	→	516
694	→	539
694	→	840
694	→	1436
1184	→	1176
234	→	192
758	→	743
758	→	916
417	→	806
724	→	770
724	→	1458
182	→	776
182	→	602
182	→	647
182	→	340
182	→	116
182	→	64
182	→	233
182	→	538
182	→	2
182	→	257
1420	→	462
42	→	9
42	→	695
42	→	939
1581	→	285
1581	→	1661
1581	→	1663
137	→	87
137	→	1163
1442	→	850
216	→	192
957	→	944
189	→	1185
189	→	1224
189	→	1505
752	→	743
1756	→	853
825	→	693
158	→	388
158	→	416
115	→	87
952	→	1590
952	→	1600
952	→	1700
905	→	4
905	→	863
905	→	516
905	→	539
17	→	1175
17	→	1209
17	→	1492
1116	→	1104
946	→	1350
1149	→	157
683	→	956
683	→	1036
683	→	1318
945	→	1003
190	→	2
190	→	714
190	→	192
190	→	216
190	→	234
190	→	218
896	→	430
718	→	1515
1583	→	478
1583	→	1584
926	→	1165
1523	→	1515
1502	→	863
1502	→	516
1502	→	645
1502	→	323
1502	→	86
1502	→	43
1502	→	217
1502	→	515
1502	→	4
1502	→	539
1464	→	1559
1464	→	1576
1464	→	1655
159	→	509
159	→	1169
462	→	1372
462	→	1413
1508	→	1493
832	→	721
324	→	296
517	→	826
517	→	1358
517	→	1534
1457	→	855
866	→	1528
1422	→	462
1422	→	1530
1695	→	1680
722	→	293
722	→	1113
523	→	1641
523	→	1727
1434	→	840
629	→	601
1227	→	1210
489	→	847
670	→	1532
1620	→	1210
953	→	117
953	→	1
953	→	715
775	→	460
1002	→	195
1028	→	1054
1028	→	1088
1028	→	1090
1028	→	1328
1225	→	1210
1444	→	853
541	→	516
1210	→	1486
1210	→	1547
1210	→	1588
1520	→	1582
1520	→	1592
1520	→	1611
1520	→	1702
852	→	721
1375	→	156
266	→	5
266	→	941
266	→	285
266	→	156
266	→	668
266	→	9
266	→	85
372	→	164
1562	→	9
785	→	833
1689	→	603
403	→	293
403	→	1247
403	→	1443
1658	→	164
576	→	516
1612	→	1210
1521	→	863
1521	→	516
1521	→	4
1521	→	365
1521	→	559
798	→	839
798	→	863
798	→	516
798	→	645
798	→	323
798	→	86
798	→	43
798	→	217
798	→	515
798	→	4
798	→	576
539	→	516
975	→	1071
975	→	1278
975	→	1344
1488	→	1735
155	→	87
996	→	714
996	→	2
996	→	192
996	→	216
1465	→	863
1465	→	516
1465	→	4
1465	→	365
1465	→	559
395	→	6
395	→	723
395	→	296
395	→	363
192	→	714
1754	→	853
430	→	1545
1381	→	156
1595	→	192
1135	→	488
1462	→	1725
1548	→	1538
1728	→	293
1728	→	1755
5₁(941)	→	942
5₁(1328)	→	1329
5₁(293)	→	294
5₁(600)	→	601
5₁(1602)	→	1603
5₁(390)	→	391
5₁(738)	→	739
5₁(371)	→	372
5₁(17)	→	18
5₁(1488)	→	1489
5₁(674)	→	675
5₁(483)	→	484
5₁(928)	→	929
5₁(749)	→	750
5₁(1176)	→	1177
5₁(1520)	→	1521
5₁(480)	→	481
5₁(1733)	→	1734
5₁(602)	→	603
5₁(671)	→	672
5₁(851)	→	852
5₁(192)	→	193
5₁(921)	→	922
5₁(1173)	→	1174
5₁(728)	→	729
5₁(1163)	→	1164
5₁(290)	→	291
5₁(848)	→	849
5₁(1106)	→	1107
5₁(702)	→	703
5₁(859)	→	860
5₁(523)	→	524
5₁(451)	→	452
5₁(786)	→	787
5₁(1461)	→	1462
5₁(836)	→	837
5₁(1655)	→	1656
5₁(401)	→	402
5₁(730)	→	731
5₁(517)	→	518
5₁(1103)	→	1104
5₁(645)	→	646
5₁(647)	→	648
5₁(759)	→	760
5₁(1104)	→	1105
5₁(808)	→	809
5₁(1115)	→	1116
5₁(850)	→	851
5₁(1211)	→	1212
5₁(995)	→	996
5₁(609)	→	610
5₁(430)	→	431
5₁(712)	→	713
5₁(581)	→	582
5₁(1040)	→	1041
5₁(1657)	→	1658
5₁(1276)	→	1277
5₁(939)	→	940
5₁(626)	→	627
5₁(844)	→	845
5₁(869)	→	870
5₁(894)	→	895
5₁(686)	→	687
5₁(858)	→	859
5₁(1241)	→	1242
5₁(868)	→	869
5₁(1315)	→	1316
5₁(906)	→	907
5₁(719)	→	720
5₁(628)	→	629
5₁(1547)	→	1548
5₁(715)	→	716
5₁(481)	→	482
5₁(952)	→	953
5₁(1169)	→	1170
5₁(189)	→	190
5₁(726)	→	727
5₁(1032)	→	1033
5₁(182)	→	183
5₁(1307)	→	1308
5₁(1318)	→	1319
5₁(1532)	→	1533
5₁(739)	→	740
5₁(803)	→	804
5₁(162)	→	163
5₁(932)	→	933
5₁(988)	→	989
5₁(914)	→	915
5₁(1537)	→	1538
5₁(1462)	→	1463
5₁(161)	→	162
0₂(1686)	→	1687
1₂(1574)	→	1575
1₂(1680)	→	1681
1₂(1571)	→	1572
1₂(1687)	→	1688
1₂(1682)	→	1683
1₂(1572)	→	1573
1₂(1681)	→	1682
1₂(1683)	→	1684
1₂(1563)	→	1564
1₂(1645)	→	1646
1₂(1685)	→	1686
3₂(1643)	→	1644
0₁(235)	→	236
0₁(1598)	→	1599
0₁(428)	→	429
0₁(807)	→	808
0₁(396)	→	397
0₁(160)	→	161
0₁(420)	→	421
0₁(1142)	→	1143
0₁(391)	→	392
0₁(841)	→	842
0₁(978)	→	979
0₁(831)	→	832
0₁(1187)	→	1188
0₁(770)	→	771
0₁(217)	→	218
0₁(601)	→	602
0₁(821)	→	822
0₁(849)	→	850
0₁(951)	→	952
0₁(215)	→	216
0₁(191)	→	192
0₁(370)	→	371
0₁(1041)	→	1042
0₁(710)	→	711
0₁(733)	→	734
0₁(834)	→	835
0₁(1441)	→	1442
0₁(771)	→	772
0₁(1592)	→	1593
0₁(1175)	→	1176
0₁(1054)	→	1055
0₁(1183)	→	1184
0₁(890)	→	891
0₁(785)	→	786
0₁(448)	→	449
0₁(256)	→	257
0₁(1278)	→	1279
0₁(1590)	→	1591
0₁(1056)	→	1057
0₁(1464)	→	1465
0₁(763)	→	764
0₁(1596)	→	1597
0₁(233)	→	234
0₁(510)	→	511
0₁(871)	→	872
0₁(824)	→	825
0₁(762)	→	763
0₁(683)	→	684
0₁(1185)	→	1186
0₁(987)	→	988
0₁(1594)	→	1595
0₁(416)	→	417
0₁(181)	→	182
0₁(16)	→	17
2₀(3)	→	5
2₀(6)	→	5
2₀(5)	→	5
2₀(4)	→	5
2₀(2)	→	5
2₀(1)	→	5
3₀(2)	→	6
3₀(6)	→	6
3₀(4)	→	6
3₀(1)	→	6
3₀(3)	→	6
3₀(5)	→	6
4₂(1566)	→	1567
4₂(1647)	→	1648
4₂(1568)	→	1569
4₂(1684)	→	1685
4₂(1649)	→	1650
4₂(1694)	→	1695
4₂(1679)	→	1680
4₂(1567)	→	1568
4₂(1648)	→	1649
4₀(1)	→	4
4₀(6)	→	4
4₀(3)	→	4
4₀(5)	→	4
4₀(2)	→	4
4₀(4)	→	4
2₁(87)	→	88
2₁(1516)	→	1517
2₁(301)	→	302
2₁(892)	→	893
2₁(1528)	→	1529
2₁(970)	→	971
2₁(794)	→	795
2₁(1030)	→	1031
2₁(1735)	→	1736
2₁(1209)	→	1210
2₁(856)	→	857
2₁(946)	→	947
2₁(8)	→	9
2₁(1058)	→	1059
2₁(490)	→	491
2₁(1279)	→	1280
2₁(919)	→	920
2₁(948)	→	949
2₁(1222)	→	1223
2₁(582)	→	583
2₁(870)	→	871
2₁(800)	→	801
2₁(667)	→	668
2₁(1180)	→	1181
2₁(734)	→	735
2₁(974)	→	975
2₁(88)	→	89
2₁(1332)	→	1333
2₁(930)	→	931
2₁(864)	→	865
2₁(263)	→	264
2₁(833)	→	834
2₁(1494)	→	1495
2₁(687)	→	688
2₁(369)	→	370
2₁(11)	→	12
2₁(682)	→	683
2₁(400)	→	401
2₁(66)	→	67
2₁(578)	→	579
2₁(744)	→	745
2₁(1515)	→	1516
2₁(511)	→	512
2₁(1536)	→	1537
2₁(365)	→	366
2₁(789)	→	790
2₁(1108)	→	1109
2₁(84)	→	85
2₁(1623)	→	1624
2₁(1167)	→	1168
2₁(700)	→	701
2₁(43)	→	44
2₁(782)	→	783
2₁(13)	→	14
2₁(393)	→	394
2₁(402)	→	403
2₁(1545)	→	1546
2₁(494)	→	495
2₁(1310)	→	1311
2₁(93)	→	94
2₁(1380)	→	1381
2₁(911)	→	912
2₁(288)	→	289
2₁(793)	→	794
2₁(583)	→	584
2₁(708)	→	709
2₁(10)	→	11
2₁(41)	→	42
2₁(917)	→	918
2₁(1609)	→	1610
2₁(92)	→	93
2₁(447)	→	448
2₁(903)	→	904
2₁(1463)	→	1464
2₁(452)	→	453
2₁(1617)	→	1618
2₁(1586)	→	1587
2₁(156)	→	157
2₁(897)	→	898
2₁(1226)	→	1227
2₁(453)	→	454
2₁(1245)	→	1246
2₁(840)	→	841
2₁(1148)	→	1149
2₁(956)	→	957
2₁(760)	→	761
2₁(1338)	→	1339
2₁(14)	→	15
2₁(289)	→	290
2₁(887)	→	888
2₁(1140)	→	1141
2₁(1346)	→	1347
2₁(806)	→	807
2₁(577)	→	578
2₁(580)	→	581
2₁(835)	→	836
2₁(1517)	→	1518
2₁(1603)	→	1604
2₁(158)	→	159
2₁(909)	→	910
2₁(943)	→	944
2₁(1600)	→	1601
2₁(910)	→	911
2₁(891)	→	892
2₁(1669)	→	1670
2₁(484)	→	485
2₁(969)	→	970
2₁(1671)	→	1672
2₁(1224)	→	1225
2₁(1559)	→	1560
2₁(945)	→	946
2₁(1031)	→	1032
2₁(1212)	→	1213
2₁(776)	→	777
2₁(1218)	→	1219
2₁(929)	→	930
2₁(1561)	→	1562
2₁(1075)	→	1076
2₁(422)	→	423
2₁(949)	→	950
2₁(1043)	→	1044
2₁(668)	→	669
2₁(64)	→	65
2₁(1588)	→	1589
2₁(1727)	→	1728
2₁(1725)	→	1726
2₁(1008)	→	1009
2₁(1372)	→	1373
2₁(773)	→	774
2₁(1330)	→	1331
2₁(920)	→	921
2₁(418)	→	419
2₁(1374)	→	1375
2₁(1500)	→	1501
2₁(259)	→	260
2₁(291)	→	292
2₁(693)	→	694
2₁(1088)	→	1089
2₁(1107)	→	1108
2₁(1004)	→	1005
2₁(424)	→	425
2₁(1611)	→	1612
2₁(1071)	→	1072
2₁(485)	→	486
2₁(398)	→	399
2₁(1619)	→	1620
2₁(1580)	→	1581
2₁(1524)	→	1525
2₁(421)	→	422
2₁(456)	→	457
2₁(679)	→	680
2₁(1661)	→	1662
2₁(801)	→	802
2₁(723)	→	724
2₁(976)	→	977
1₁(184)	→	185
1₁(1541)	→	1542
1₁(798)	→	799
1₁(673)	→	674
1₁(695)	→	696
1₁(1460)	→	1461
1₁(936)	→	937
1₁(934)	→	935
1₁(720)	→	721
1₁(1601)	→	1602
1₁(908)	→	909
1₁(843)	→	844
1₁(261)	→	262
1₁(828)	→	829
1₁(1753)	→	1754
1₁(449)	→	450
1₁(1519)	→	1520
1₁(748)	→	749
1₁(509)	→	510
1₁(717)	→	718
1₁(460)	→	461
1₁(746)	→	747
1₁(827)	→	828
1₁(924)	→	925
1₁(427)	→	428
1₁(265)	→	266
1₁(185)	→	186
1₁(462)	→	463
1₁(1216)	→	1217
1₁(1344)	→	1345
1₁(893)	→	894
1₁(1280)	→	1281
1₁(193)	→	194
1₁(1539)	→	1540
1₁(1314)	→	1315
1₁(819)	→	820
1₁(883)	→	884
1₁(1542)	→	1543
1₁(972)	→	973
1₁(701)	→	702
1₁(802)	→	803
1₁(672)	→	673
1₁(735)	→	736
1₁(1105)	→	1106
1₁(95)	→	96
1₁(94)	→	95
1₁(1312)	→	1313
1₁(792)	→	793
1₁(842)	→	843
1₁(691)	→	692
1₁(670)	→	671
1₁(1113)	→	1114
1₁(1171)	→	1172
1₁(518)	→	519
1₁(933)	→	934
1₁(114)	→	115
1₁(1006)	→	1007
1₁(183)	→	184
1₁(194)	→	195
1₁(1101)	→	1102
1₁(199)	→	200
1₁(186)	→	187
1₁(990)	→	991
1₁(1313)	→	1314
1₁(745)	→	746
1₁(790)	→	791
1₁(989)	→	990
1₁(724)	→	725
1₁(847)	→	848
1₁(685)	→	686
1₁(1538)	→	1539
1₁(810)	→	811
1₁(1582)	→	1583
1₁(522)	→	523
1₁(867)	→	868
1₁(1311)	→	1312
1₁(711)	→	712
1₁(300)	→	301
1₁(1010)	→	1011
1₁(926)	→	927
1₁(830)	→	831
1₁(1755)	→	1756
1₁(784)	→	785
1₁(163)	→	164
1₁(725)	→	726
1₁(718)	→	719
1₁(1111)	→	1112
1₁(1607)	→	1608
1₁(521)	→	522
1₁(886)	→	887
1₁(721)	→	722
1₁(479)	→	480
1₁(904)	→	905
1₁(426)	→	427
1₁(1161)	→	1162
1₁(937)	→	938
1₁(605)	→	606
1₁(286)	→	287
1₁(604)	→	605
1₁(971)	→	972
1₁(1029)	→	1030
1₁(367)	→	368
1₁(992)	→	993
1₁(287)	→	288
1₁(296)	→	297
1₁(116)	→	117
1₁(264)	→	265
1₁(1350)	→	1351
1₁(1522)	→	1523
1₁(1210)	→	1211
1₁(1028)	→	1029
1₁(134)	→	135
1₁(1253)	→	1254
1₁(1696)	→	1697
1₁(826)	→	827
1₁(136)	→	137
1₁(787)	→	788
1₁(714)	→	715
1₁(1001)	→	1002
1₁(1102)	→	1103
1₁(913)	→	914
1₁(747)	→	748
1₁(991)	→	992
1₁(697)	→	698
1₁(482)	→	483
1₁(478)	→	479
1₁(1501)	→	1502
1₁(1009)	→	1010
1₁(86)	→	87
1₁(1493)	→	1494
1₁(154)	→	155
1₁(457)	→	458
1₁(516)	→	517
1₁(195)	→	196
1₁(1761)	→	1762
1₁(1134)	→	1135
1₁(885)	→	886
1₁(1443)	→	1444
0₀(3)	→	2
0₀(5)	→	2
0₀(2)	→	2
0₀(4)	→	2
0₀(1)	→	2
0₀(6)	→	2
5₀(2)	→	3
5₀(4)	→	3
5₀(3)	→	3
5₀(6)	→	3
5₀(1)	→	3
5₀(5)	→	3
3₁(916)	→	917
3₁(187)	→	188
3₁(861)	→	862
3₁(918)	→	919
3₁(1459)	→	1460
3₁(1498)	→	1499
3₁(461)	→	462
3₁(993)	→	994
3₁(823)	→	824
3₁(9)	→	10
3₁(731)	→	732
3₁(513)	→	514
3₁(492)	→	493
3₁(362)	→	363
3₁(855)	→	856
3₁(944)	→	945
3₁(512)	→	513
3₁(899)	→	900
3₁(292)	→	293
3₁(1036)	→	1037
3₁(865)	→	866
3₁(729)	→	730
3₁(845)	→	846
3₁(901)	→	902
3₁(1530)	→	1531
3₁(799)	→	800
3₁(321)	→	322
3₁(1507)	→	1508
3₁(493)	→	494
3₁(392)	→	393
3₁(837)	→	838
3₁(863)	→	864
3₁(1282)	→	1283
3₁(788)	→	789
3₁(429)	→	430
3₁(1496)	→	1497
3₁(1576)	→	1577
3₁(1700)	→	1701
3₁(1042)	→	1043
3₁(188)	→	189
3₁(740)	→	741
3₁(822)	→	823
3₁(459)	→	460
3₁(1710)	→	1711
3₁(295)	→	296
3₁(866)	→	867
3₁(778)	→	779
3₁(1057)	→	1058
3₁(299)	→	300
3₁(1663)	→	1664
3₁(323)	→	324
3₁(780)	→	781
3₁(1708)	→	1709
3₁(1090)	→	1091
3₁(1059)	→	1060
3₁(884)	→	885
3₁(1352)	→	1353
3₁(1704)	→	1705
3₁(1034)	→	1035
3₁(340)	→	341
3₁(1492)	→	1493
3₁(994)	→	995
3₁(198)	→	199
3₁(888)	→	889
3₁(699)	→	700
3₁(417)	→	418
3₁(455)	→	456
3₁(777)	→	778
3₁(1578)	→	1579
3₁(737)	→	738
3₁(1702)	→	1703
3₁(1503)	→	1504
3₁(1458)	→	1459
3₁(342)	→	343
3₁(419)	→	420
3₁(1358)	→	1359
3₁(1505)	→	1506
3₁(397)	→	398
3₁(669)	→	670
3₁(853)	→	854
4₁(1165)	→	1166
4₁(774)	→	775
4₁(925)	→	926
4₁(366)	→	367
4₁(709)	→	710
4₁(1255)	→	1256
4₁(285)	→	286
4₁(399)	→	400
4₁(704)	→	705
4₁(820)	→	821
4₁(677)	→	678
4₁(519)	→	520
4₁(1214)	→	1215
4₁(1675)	→	1676
4₁(1316)	→	1317
4₁(795)	→	796
4₁(1038)	→	1039
4₁(538)	→	539
4₁(1421)	→	1422
4₁(676)	→	677
4₁(898)	→	899
4₁(488)	→	489
4₁(857)	→	858
4₁(736)	→	737
4₁(689)	→	690
4₁(1413)	→	1414
4₁(1109)	→	1110
4₁(1215)	→	1216
4₁(1605)	→	1606
4₁(703)	→	704
4₁(89)	→	90
4₁(912)	→	913
4₁(450)	→	451
4₁(1419)	→	1420
4₁(368)	→	369
4₁(779)	→	780
4₁(388)	→	389
4₁(1247)	→	1248
4₁(486)	→	487
4₁(1027)	→	1028
4₁(159)	→	160
4₁(950)	→	951
4₁(1003)	→	1004
4₁(781)	→	782
4₁(1534)	→	1535
4₁(743)	→	744
4₁(772)	→	773
4₁(1495)	→	1496
4₁(947)	→	948
4₁(12)	→	13
4₁(1007)	→	1008
4₁(1497)	→	1498
4₁(1518)	→	1519
4₁(1181)	→	1182
4₁(716)	→	717
4₁(854)	→	855
4₁(1308)	→	1309
4₁(753)	→	754
4₁(1606)	→	1607
4₁(1456)	→	1457
4₁(1005)	→	1006
4₁(922)	→	923
4₁(603)	→	604
4₁(1217)	→	1218
4₁(1584)	→	1585
4₁(196)	→	197
4₁(364)	→	365
4₁(1399)	→	1400
4₁(607)	→	608
4₁(902)	→	903
4₁(680)	→	681
4₁(900)	→	901
4₁(575)	→	576
4₁(829)	→	830
4₁(895)	→	896
4₁(1044)	→	1045
4₁(157)	→	158
4₁(1213)	→	1214
4₁(705)	→	706
4₁(1543)	→	1544
4₁(458)	→	459
4₁(579)	→	580
4₁(90)	→	91
4₁(678)	→	679
4₁(489)	→	490
4₁(1281)	→	1282
4₁(688)	→	689
4₁(1309)	→	1310
4₁(755)	→	756
4₁(804)	→	805
4₁(258)	→	259
4₁(425)	→	426
4₁(977)	→	978
4₁(1427)	→	1428
4₁(1039)	→	1040
4₁(1608)	→	1609
4₁(1747)	→	1748
4₁(262)	→	263
4₁(1677)	→	1678
4₁(91)	→	92
4₁(1138)	→	1139
4₁(164)	→	165
4₁(606)	→	607
4₁(997)	→	998
4₁(1499)	→	1500
4₁(757)	→	758
4₁(975)	→	976
4₁(1179)	→	1180
4₁(1698)	→	1699
4₁(742)	→	743
4₁(1433)	→	1434
4₁(707)	→	708
4₁(520)	→	521
4₁(1178)	→	1179
4₁(389)	→	390
4₁(515)	→	516
4₁(491)	→	492
4₁(394)	→	395
4₁(1604)	→	1605
4₁(681)	→	682
4₁(935)	→	936
4₁(751)	→	752
4₁(692)	→	693
4₁(297)	→	298
4₁(15)	→	16
4₁(558)	→	559
4₁(1136)	→	1137
4₁(797)	→	798
4₁(809)	→	810
4₁(197)	→	198
4₁(761)	→	762
4₁(302)	→	303
4₁(298)	→	299
4₁(1177)	→	1178
4₁(1435)	→	1436
4₁(556)	→	557
4₁(727)	→	728
4₁(540)	→	541
4₁(1540)	→	1541
4₁(584)	→	585
4₁(927)	→	928
4₁(1673)	→	1674
4₁(907)	→	908
4₁(260)	→	261
4₁(690)	→	691
4₁(839)	→	840
4₁(1486)	→	1487
2₂(1644)	→	1645
2₂(1570)	→	1571
2₂(1569)	→	1570
2₂(1642)	→	1643
2₂(1564)	→	1565
2₂(1565)	→	1566
1₀(1)	→	1
1₀(6)	→	1
1₀(5)	→	1
1₀(2)	→	1
1₀(3)	→	1
1₀(4)	→	1
5₂(1646)	→	1647
5₂(1641)	→	1642
5₂(1688)	→	1689

The automaton is closed under rewriting as it is compatible.