Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/5076)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 2. This is shown by the following automaton.

final states:

{7}

transitions:

1389	→	1378
1405	→	31
1405	→	582
1405	→	75
1405	→	368
1405	→	1566
1405	→	1583
1197	→	968
314	→	259
588	→	995
588	→	1012
588	→	1130
1693	→	355
793	→	209
329	→	778
221	→	1138
176	→	792
176	→	1357
587	→	1154
587	→	1388
102	→	999
32	→	771
29	→	7
29	→	235
29	→	263
29	→	74
29	→	290
29	→	1141
1608	→	31
1335	→	31
1703	→	530
589	→	327
589	→	280
589	→	234
589	→	104
589	→	30
589	→	19
589	→	45
589	→	218
589	→	7
589	→	106
589	→	219
1057	→	121
1106	→	210
81	→	28
81	→	828
750	→	106
356	→	1560
80	→	912
80	→	1377
103	→	7
103	→	366
103	→	309
103	→	73
103	→	65
103	→	178
103	→	31
103	→	310
103	→	391
103	→	301
103	→	118
103	→	128
103	→	105
103	→	302
103	→	288
103	→	311
103	→	348
103	→	197
103	→	66
103	→	254
103	→	46
103	→	327
103	→	280
103	→	106
103	→	219
103	→	998
103	→	374
103	→	1177
103	→	1577
103	→	1583
103	→	1567
1630	→	129
1142	→	1222
1142	→	1226
1142	→	1427
1288	→	1068
1163	→	355
1169	→	355
1169	→	1170
1169	→	1334
1313	→	1067
289	→	373
537	→	1336
1248	→	1008
1393	→	45
1046	→	1240
96	→	1056
1642	→	210
1606	→	54
1606	→	1629
326	→	102
326	→	749
326	→	751
1195	→	54
1195	→	1270
136	→	39
998	→	31
995	→	1590
149	→	7
149	→	366
149	→	309
149	→	73
149	→	65
149	→	178
149	→	31
149	→	310
149	→	391
149	→	301
149	→	118
149	→	128
149	→	105
149	→	302
149	→	998
149	→	1577
149	→	1583
211	→	1043
119	→	190
1575	→	66
1575	→	311
1575	→	1567
878	→	391
878	→	301
878	→	118
878	→	234
878	→	104
878	→	30
878	→	19
878	→	45
878	→	218
878	→	7
878	→	128
878	→	105
878	→	302
1327	→	19
1589	→	530
1098	→	19
1141	→	290
1395	→	45
226	→	38
1577	→	1566
39	→	659
39	→	961
39	→	1113
57	→	784
772	→	102
1628	→	129
1033	→	20
1011	→	56
1011	→	1099
1011	→	1162
980	→	1318
1226	→	1517
1074	→	1328
564	→	66
219	→	327
219	→	1140
219	→	1176
147	→	1081
1000	→	1396
1524	→	1067
1076	→	31
1076	→	171
1076	→	1583
1454	→	581
1454	→	1548
1055	→	209
1055	→	56
1055	→	234
1055	→	104
1055	→	30
1055	→	19
1055	→	45
1055	→	218
1055	→	7
1055	→	170
1055	→	20
1055	→	1067
1055	→	1078
1027	→	20
1681	→	1378
185	→	155
997	→	1576
361	→	53
1664	→	209
1183	→	54
1183	→	1256
1139	→	283
55	→	7
55	→	301
55	→	118
55	→	32
55	→	128
55	→	105
55	→	391
55	→	302
55	→	209
55	→	56
55	→	170
55	→	20
55	→	31
55	→	75
55	→	368
55	→	582
55	→	1566
55	→	1583
255	→	786
813	→	1034
813	→	1192
325	→	1045
325	→	1142
243	→	39
1636	→	1067
1082	→	1067
889	→	872
889	→	1097
749	→	1032
749	→	1182
20	→	56
20	→	170
20	→	209
20	→	234
20	→	104
20	→	30
20	→	19
20	→	45
20	→	218
20	→	7
20	→	1067
20	→	1078
837	→	129
837	→	234
837	→	104
837	→	30
837	→	19
837	→	45
837	→	218
837	→	7
837	→	235
397	→	20
1159	→	331
31	→	65
31	→	73
31	→	178
31	→	309
1034	→	1304
40	→	7
40	→	301
40	→	118
40	→	328
40	→	128
40	→	105
40	→	235
40	→	288
40	→	254
40	→	46
40	→	129
40	→	327
40	→	280
40	→	106
40	→	219
40	→	244
40	→	47
40	→	290
40	→	1141
1443	→	1566
1078	→	1067
1026	→	1310
1591	→	530
287	→	148
877	→	976
877	→	980
877	→	1024
1009	→	771
1009	→	32
922	→	1146
1687	→	1378
977	→	968
127	→	7
127	→	209
127	→	56
127	→	170
127	→	20
127	→	288
127	→	303
127	→	254
127	→	46
127	→	1067
127	→	1078
1267	→	1257
1223	→	1212
1387	→	771
1387	→	32
60	→	24
1319	→	1067
1208	→	412
1607	→	1702
73	→	997
73	→	1014
1366	→	1008
1329	→	19
1161	→	349
261	→	1128
1137	→	281
993	→	1584
235	→	581
235	→	861
235	→	888
1428	→	54
1428	→	1509
296	→	148
816	→	810
269	→	135
1503	→	1635
58	→	815
349	→	1152
994	→	31
177	→	101
21	→	95
21	→	141
21	→	355
21	→	1022
21	→	1196
72	→	27
1170	→	1355
1528	→	142
779	→	154
1084	→	172
1311	→	1067
839	→	247
1075	→	1287
1075	→	1371
302	→	391
1193	→	54
1193	→	1268
1032	→	1306
921	→	1198
1042	→	20
1356	→	209
1356	→	1525
54	→	869
308	→	112
22	→	234
22	→	104
22	→	30
22	→	19
22	→	45
22	→	218
22	→	7
22	→	1566
22	→	1583
1041	→	1312
105	→	118
105	→	128
105	→	301
105	→	7
105	→	32
1450	→	1643
1450	→	1678
1450	→	1686
1585	→	1566
1131	→	236
249	→	71
1181	→	54
1181	→	1266
1168	→	1523
1146	→	1211
1146	→	1224
1146	→	1421
538	→	993
538	→	1010
538	→	1132
538	→	1320
204	→	102
1337	→	19
143	→	1083
923	→	209
923	→	56
923	→	234
923	→	104
923	→	30
923	→	19
923	→	45
923	→	218
923	→	7
923	→	170
923	→	20
814	→	288
814	→	7
814	→	254
814	→	46
787	→	199
979	→	21
1679	→	209
528	→	56
528	→	794
528	→	914
28	→	410
28	→	527
1504	→	20
843	→	135
557	→	1289
419	→	1041
419	→	1124
419	→	1194
1404	→	1558
1451	→	1607
1451	→	1613
1451	→	1657
1035	→	20
1108	→	210
1015	→	56
1015	→	1107
1015	→	1168
1587	→	1568
66	→	197
66	→	348
106	→	280
106	→	234
106	→	104
106	→	30
106	→	19
106	→	45
106	→	218
106	→	7
379	→	53
1452	→	1176
1452	→	327
1452	→	280
1452	→	1077
1452	→	218
1452	→	45
1452	→	19
1452	→	30
1452	→	104
1452	→	234
1452	→	7
1452	→	106
1452	→	1140
1452	→	219
1155	→	209
862	→	264
913	→	209
1224	→	1519
1063	→	129
795	→	210
1334	→	1588
981	→	20
1125	→	1114
1143	→	28
1143	→	1394
1221	→	366
1221	→	31
1221	→	998
1221	→	310
1221	→	1577
1177	→	374
335	→	126
1013	→	56
1013	→	1105
1013	→	1164
1526	→	21
1559	→	54
1559	→	1627
1044	→	108
7	→	19
7	→	30
7	→	45
7	→	104
7	→	218
7	→	234
757	→	203
217	→	54
217	→	563
1080	→	1067
113	→	54
126	→	1079
30	→	1582
962	→	54
962	→	1062
216	→	529
216	→	982
1614	→	56
1614	→	1641
1614	→	1692
1307	→	1067
46	→	254
46	→	288
46	→	1134
46	→	1148
46	→	1160
1305	→	1067
1321	→	1068
1133	→	235
1510	→	129
1100	→	210
310	→	366
531	→	1586
48	→	150
48	→	553
1372	→	21
1372	→	1453
1025	→	530
245	→	840
1512	→	129
47	→	244
1644	→	54
1149	→	304
836	→	1026
836	→	1180
1537	→	1176
1537	→	327
1537	→	1140
1537	→	219
1549	→	264
1583	→	1566
1439	→	97
1017	→	530
1129	→	1114
870	→	1136
148	→	396
148	→	967
148	→	1016
324	→	1209
1153	→	313
492	→	102
1054	→	1326
1422	→	54
1422	→	1511
142	→	978
1227	→	20
74	→	263
74	→	7
74	→	235
1264	→	1503
1264	→	1605
1271	→	129
1290	→	1067
1561	→	349
1165	→	355
1225	→	20
1444	→	1529
1210	→	1199
1520	→	1067
1171	→	102
19	→	1077
328	→	838
1518	→	1067
558	→	73
1065	→	131
372	→	203
1269	→	129
210	→	319
354	→	325
669	→	366
669	→	309
669	→	73
669	→	7
669	→	65
669	→	178
669	→	31
669	→	310
669	→	998
669	→	1577
669	→	1583
785	→	181
785	→	1064
396	→	1066
1265	→	290
1265	→	888
1265	→	581
1265	→	1077
1265	→	218
1265	→	45
1265	→	19
1265	→	30
1265	→	104
1265	→	234
1265	→	7
1265	→	861
1265	→	235
1265	→	1141
1371	→	1429
1371	→	1442
1371	→	1527
1658	→	54
1023	→	530
539	→	263
539	→	74
539	→	367
539	→	290
539	→	1141
992	→	871
975	→	537
1123	→	288
1123	→	254
1123	→	46
996	→	31
262	→	39
395	→	183
191	→	488
1147	→	28
1147	→	1392
661	→	807
1262	→	1663
1262	→	1680
156	→	102
1135	→	239
1135	→	1158
196	→	112
420	→	301
420	→	118
420	→	7
420	→	328
420	→	128
420	→	105
2₁(1692)	→	1693
2₁(1328)	→	1329
2₁(126)	→	127
2₁(36)	→	37
2₁(527)	→	528
2₁(912)	→	913
2₁(190)	→	191
2₁(27)	→	28
2₁(141)	→	142
2₁(919)	→	920
2₁(1164)	→	1165
2₁(1336)	→	1337
2₁(124)	→	125
2₁(195)	→	196
2₁(329)	→	330
2₁(1663)	→	1664
2₁(659)	→	660
2₁(238)	→	239
2₁(280)	→	281
2₁(79)	→	80
2₁(586)	→	587
2₁(1168)	→	1169
2₁(1355)	→	1356
2₁(585)	→	586
2₁(242)	→	243
2₁(319)	→	320
2₁(771)	→	772
2₁(219)	→	220
2₁(980)	→	981
2₁(835)	→	836
2₁(1136)	→	1137
2₁(369)	→	370
2₁(1014)	→	1015
2₁(292)	→	293
2₁(1010)	→	1011
2₁(78)	→	79
2₁(67)	→	68
2₁(25)	→	26
2₁(1012)	→	1013
2₁(378)	→	379
2₁(1224)	→	1225
2₁(1678)	→	1679
2₁(751)	→	752
2₁(118)	→	119
2₁(183)	→	184
2₁(144)	→	145
2₁(172)	→	173
2₁(1326)	→	1327
2₁(213)	→	214
2₁(203)	→	204
2₁(1613)	→	1614
2₁(1041)	→	1042
2₁(305)	→	306
2₁(112)	→	113
2₁(266)	→	267
2₁(1226)	→	1227
2₁(281)	→	282
2₁(1162)	→	1163
2₁(978)	→	979
2₁(792)	→	793
2₁(1260)	→	1261
2₁(660)	→	661
2₁(268)	→	269
2₁(416)	→	417
2₁(225)	→	226
2₁(873)	→	874
2₁(47)	→	48
2₁(1026)	→	1027
2₁(374)	→	375
2₁(1154)	→	1155
2₁(20)	→	21
2₁(191)	→	192
2₁(1527)	→	1528
2₁(19)	→	20
2₁(1134)	→	1135
2₁(201)	→	202
2₁(368)	→	369
2₁(178)	→	179
2₁(132)	→	133
2₁(811)	→	812
2₁(1032)	→	1033
2₁(584)	→	585
2₁(284)	→	285
2₁(182)	→	183
2₁(264)	→	265
2₁(1034)	→	1035
2₁(1525)	→	1526
2₁(359)	→	360
2₁(146)	→	147
2₁(147)	→	148
2₁(1503)	→	1504
2₁(220)	→	221
2₁(914)	→	915
2₁(557)	→	558
2₁(48)	→	49
2₁(396)	→	397
2₁(352)	→	353
2₁(77)	→	78
2₁(831)	→	832
0₂(1045)	→	1046
0₂(1119)	→	1120
0₂(1446)	→	1447
0₂(1117)	→	1118
0₂(1382)	→	1383
0₂(1199)	→	1200
0₂(1000)	→	1001
0₂(1121)	→	1122
0₂(1401)	→	1402
0₂(1008)	→	1009
0₂(1404)	→	1405
0₂(1573)	→	1574
0₂(1207)	→	1208
0₂(1364)	→	1365
0₂(1385)	→	1386
0₂(531)	→	532
0₂(1070)	→	1071
2₂(1212)	→	1213
2₂(1067)	→	1068
2₂(1289)	→	1290
2₂(973)	→	974
2₂(1523)	→	1524
2₂(1304)	→	1305
2₂(1534)	→	1535
2₂(1287)	→	1288
2₂(1120)	→	1121
2₂(1306)	→	1307
2₂(537)	→	538
2₂(1519)	→	1520
2₂(1320)	→	1321
2₂(1052)	→	1053
2₂(1517)	→	1518
2₂(1430)	→	1431
2₂(1115)	→	1116
2₂(976)	→	977
2₂(1247)	→	1248
2₂(1071)	→	1072
2₂(1388)	→	1389
2₂(1222)	→	1223
2₂(1686)	→	1687
2₂(1077)	→	1078
2₂(968)	→	969
2₂(1318)	→	1319
2₂(1357)	→	1358
2₂(1429)	→	1430
2₂(1200)	→	1201
2₂(1079)	→	1080
2₂(1635)	→	1636
2₂(990)	→	991
2₂(1114)	→	1115
2₂(1081)	→	1082
2₂(1571)	→	1572
2₂(988)	→	989
2₂(1001)	→	1002
2₂(1310)	→	1311
2₂(983)	→	984
2₂(1073)	→	1074
2₂(1074)	→	1075
2₂(1379)	→	1380
2₂(1201)	→	1202
2₂(1532)	→	1533
2₂(1066)	→	1067
2₂(1448)	→	1449
2₂(1196)	→	1197
2₂(1046)	→	1047
2₂(1437)	→	1438
2₂(1398)	→	1399
2₂(967)	→	968
2₂(1680)	→	1681
2₂(1002)	→	1003
2₂(1402)	→	1403
2₂(1449)	→	1450
2₂(532)	→	533
2₂(1447)	→	1448
2₂(1362)	→	1363
2₂(1054)	→	1055
2₂(1068)	→	1069
2₂(982)	→	983
2₂(1377)	→	1378
2₂(1211)	→	1212
2₂(1312)	→	1313
2₂(1435)	→	1436
2₂(1530)	→	1531
3₂(1399)	→	1400
3₂(1569)	→	1570
3₂(538)	→	539
3₂(1244)	→	1245
3₂(534)	→	535
3₂(991)	→	992
3₂(985)	→	986
3₂(1450)	→	1451
3₂(989)	→	990
3₂(970)	→	971
3₂(1363)	→	1364
3₂(1436)	→	1437
3₂(1451)	→	1452
3₂(533)	→	534
3₂(1214)	→	1215
3₂(1432)	→	1433
3₂(974)	→	975
3₂(1443)	→	1444
3₂(1438)	→	1439
3₂(1445)	→	1446
3₂(1116)	→	1117
3₂(1535)	→	1536
3₂(1383)	→	1384
4₁(794)	→	795
4₁(282)	→	283
4₁(419)	→	420
4₁(70)	→	71
4₁(813)	→	814
4₁(1138)	→	1139
4₁(1105)	→	1106
4₁(334)	→	335
4₁(491)	→	492
4₁(1107)	→	1108
4₁(663)	→	664
4₁(874)	→	875
4₁(211)	→	212
4₁(1142)	→	1143
4₁(129)	→	130
4₁(778)	→	779
4₁(832)	→	833
4₁(175)	→	176
4₁(353)	→	354
4₁(752)	→	753
4₁(285)	→	286
4₁(1099)	→	1100
4₁(332)	→	333
4₁(1257)	→	1258
4₁(555)	→	556
4₁(1083)	→	1084
4₁(661)	→	662
4₁(749)	→	750
4₁(244)	→	245
4₁(1146)	→	1147
4₁(153)	→	154
4₁(52)	→	53
4₁(119)	→	120
4₁(223)	→	224
4₁(393)	→	394
4₁(809)	→	810
4₁(869)	→	870
4₁(1264)	→	1265
4₁(39)	→	40
4₁(1641)	→	1642
4₁(665)	→	666
4₁(304)	→	305
4₁(294)	→	295
4₁(256)	→	257
4₁(95)	→	96
4₁(239)	→	240
4₁(105)	→	106
4₁(261)	→	262
4₁(171)	→	172
4₁(218)	→	219
4₁(283)	→	284
4₁(209)	→	210
4₁(784)	→	785
4₁(99)	→	100
4₁(59)	→	60
4₁(180)	→	181
4₁(313)	→	314
4₁(320)	→	321
4₁(199)	→	200
4₁(875)	→	876
4₁(97)	→	98
4₁(150)	→	151
4₁(293)	→	294
4₁(111)	→	112
4₁(815)	→	816
4₁(836)	→	837
4₁(666)	→	667
4₁(376)	→	377
4₁(100)	→	101
4₁(288)	→	289
1₀(7)	→	7
0₀(7)	→	7
5₂(1586)	→	1587
5₂(984)	→	985
5₂(1022)	→	1023
5₂(1048)	→	1049
5₂(1431)	→	1432
5₂(971)	→	972
5₂(1444)	→	1445
5₂(1531)	→	1532
5₂(1702)	→	1703
5₂(969)	→	970
5₂(1533)	→	1534
5₂(529)	→	530
5₂(1584)	→	1585
5₂(1024)	→	1025
5₂(1069)	→	1070
5₂(1051)	→	1052
5₂(1590)	→	1591
5₂(1245)	→	1246
5₂(986)	→	987
5₂(1570)	→	1571
5₂(1203)	→	1204
5₂(1442)	→	1443
5₂(1016)	→	1017
5₂(1588)	→	1589
5₂(1433)	→	1434
5₂(1381)	→	1382
5₂(1576)	→	1577
5₂(1075)	→	1076
5₂(1582)	→	1583
5₂(1004)	→	1005
5₂(1397)	→	1398
5₂(1567)	→	1568
5₂(1365)	→	1366
5₂(1242)	→	1243
2₀(7)	→	7
1₁(125)	→	126
1₁(1261)	→	1262
1₁(108)	→	109
1₁(876)	→	877
1₁(101)	→	102
1₁(106)	→	107
1₁(556)	→	557
1₁(841)	→	842
1₁(490)	→	491
1₁(58)	→	59
1₁(667)	→	668
1₁(488)	→	489
1₁(122)	→	123
1₁(915)	→	916
1₁(98)	→	99
1₁(349)	→	350
1₁(237)	→	238
1₁(263)	→	264
1₁(257)	→	258
1₁(53)	→	54
1₁(414)	→	415
1₁(830)	→	831
1₁(152)	→	153
1₁(333)	→	334
1₁(355)	→	356
1₁(295)	→	296
1₁(921)	→	922
1₁(49)	→	50
1₁(840)	→	841
1₁(145)	→	146
1₁(755)	→	756
1₁(102)	→	103
1₁(133)	→	134
1₁(413)	→	414
1₁(197)	→	198
1₁(65)	→	66
1₁(664)	→	665
1₁(34)	→	35
1₁(302)	→	303
1₁(310)	→	311
1₁(754)	→	755
1₁(392)	→	393
1₁(121)	→	122
1₁(254)	→	255
1₁(247)	→	248
1₁(210)	→	211
1₁(24)	→	25
1₁(45)	→	46
1₁(668)	→	669
1₁(51)	→	52
1₁(842)	→	843
1₁(33)	→	34
1₁(212)	→	213
1₁(328)	→	329
1₁(563)	→	564
1₁(259)	→	260
1₁(861)	→	862
1₁(1548)	→	1549
1₁(71)	→	72
1₁(258)	→	259
1₁(371)	→	372
1₁(324)	→	325
5₁(267)	→	268
5₁(995)	→	996
5₁(131)	→	132
5₁(348)	→	349
5₁(123)	→	124
5₁(1371)	→	1372
5₁(877)	→	878
5₁(331)	→	332
5₁(410)	→	411
5₁(265)	→	266
5₁(321)	→	322
5₁(753)	→	754
5₁(155)	→	156
5₁(200)	→	201
5₁(756)	→	757
5₁(21)	→	22
5₁(311)	→	312
5₁(120)	→	121
5₁(1097)	→	1098
5₁(1043)	→	1044
5₁(32)	→	33
5₁(351)	→	352
5₁(920)	→	921
5₁(581)	→	582
5₁(1334)	→	1335
5₁(360)	→	361
5₁(23)	→	24
5₁(194)	→	195
5₁(50)	→	51
5₁(489)	→	490
5₁(1259)	→	1260
5₁(833)	→	834
5₁(74)	→	75
5₁(373)	→	374
5₁(216)	→	217
5₁(148)	→	149
5₁(307)	→	308
5₁(240)	→	241
5₁(1560)	→	1561
5₁(993)	→	994
5₁(357)	→	358
5₁(1607)	→	1608
5₁(142)	→	143
5₁(1056)	→	1057
5₁(30)	→	31
5₁(107)	→	108
5₁(170)	→	171
5₁(367)	→	368
5₁(1160)	→	1161
5₁(917)	→	918
5₁(110)	→	111
5₁(1176)	→	1177
5₁(997)	→	998
5₁(309)	→	310
5₁(412)	→	413
4₀(7)	→	7
5₀(7)	→	7
3₁(1170)	→	1171
3₁(179)	→	180
3₁(918)	→	919
3₁(134)	→	135
3₁(214)	→	215
3₁(22)	→	23
3₁(1262)	→	1263
3₁(1511)	→	1512
3₁(375)	→	376
3₁(1256)	→	1257
3₁(807)	→	808
3₁(128)	→	129
3₁(394)	→	395
3₁(290)	→	291
3₁(69)	→	70
3₁(154)	→	155
3₁(109)	→	110
3₁(1643)	→	1644
3₁(1629)	→	1630
3₁(221)	→	222
3₁(587)	→	588
3₁(234)	→	235
3₁(248)	→	249
3₁(1657)	→	1658
3₁(582)	→	583
3₁(75)	→	76
3₁(554)	→	555
3₁(662)	→	663
3₁(366)	→	367
3₁(871)	→	872
3₁(193)	→	194
3₁(350)	→	351
3₁(1263)	→	1264
3₁(1509)	→	1510
3₁(37)	→	38
3₁(181)	→	182
3₁(35)	→	36
3₁(73)	→	74
3₁(1062)	→	1063
3₁(135)	→	136
3₁(1140)	→	1141
3₁(68)	→	69
3₁(1268)	→	1269
3₁(358)	→	359
3₁(391)	→	392
3₁(323)	→	324
3₁(56)	→	57
3₁(588)	→	589
3₁(1132)	→	1133
3₁(303)	→	304
3₁(1266)	→	1267
3₁(176)	→	177
3₁(28)	→	29
3₁(1270)	→	1271
3₁(198)	→	199
3₁(888)	→	889
3₁(417)	→	418
3₁(370)	→	371
3₁(80)	→	81
3₁(1627)	→	1628
3₁(553)	→	554
3₁(1453)	→	1454
3₁(870)	→	871
3₁(289)	→	290
3₁(786)	→	787
3₁(1158)	→	1159
3₁(96)	→	97
3₁(26)	→	27
3₁(330)	→	331
3₁(260)	→	261
3₁(174)	→	175
3₁(1148)	→	1149
3₁(415)	→	416
3₁(192)	→	193
0₁(235)	→	236
0₁(1152)	→	1153
0₁(327)	→	328
0₁(418)	→	419
0₁(583)	→	584
0₁(1421)	→	1422
0₁(291)	→	292
0₁(215)	→	216
0₁(246)	→	247
0₁(1605)	→	1606
0₁(1130)	→	1131
0₁(1194)	→	1195
0₁(255)	→	256
0₁(1192)	→	1193
0₁(31)	→	32
0₁(411)	→	412
0₁(236)	→	237
0₁(306)	→	307
0₁(834)	→	835
0₁(1064)	→	1065
0₁(66)	→	67
0₁(222)	→	223
0₁(922)	→	923
0₁(961)	→	962
0₁(322)	→	323
0₁(1392)	→	1393
0₁(872)	→	873
0₁(829)	→	830
0₁(57)	→	58
0₁(1180)	→	1181
0₁(356)	→	357
0₁(1558)	→	1559
0₁(838)	→	839
0₁(173)	→	174
0₁(224)	→	225
0₁(76)	→	77
0₁(1427)	→	1428
0₁(828)	→	829
0₁(810)	→	811
0₁(38)	→	39
0₁(46)	→	47
0₁(312)	→	313
0₁(286)	→	287
0₁(241)	→	242
0₁(151)	→	152
0₁(130)	→	131
0₁(104)	→	105
0₁(1258)	→	1259
0₁(325)	→	326
0₁(143)	→	144
0₁(916)	→	917
0₁(202)	→	203
0₁(301)	→	302
0₁(245)	→	246
0₁(54)	→	55
0₁(184)	→	185
0₁(1394)	→	1395
0₁(812)	→	813
0₁(1182)	→	1183
0₁(808)	→	809
0₁(377)	→	378
4₂(1378)	→	1379
4₂(1536)	→	1537
4₂(1360)	→	1361
4₂(1572)	→	1573
4₂(1218)	→	1219
4₂(1400)	→	1401
4₂(1118)	→	1119
4₂(1358)	→	1359
4₂(1128)	→	1129
4₂(1217)	→	1218
4₂(1047)	→	1048
4₂(1122)	→	1123
4₂(1205)	→	1206
4₂(1380)	→	1381
4₂(1006)	→	1007
4₂(1215)	→	1216
4₂(1246)	→	1247
4₂(1213)	→	1214
4₂(1113)	→	1114
4₂(1124)	→	1125
4₂(535)	→	536
4₂(1240)	→	1241
4₂(1396)	→	1397
3₀(7)	→	7
1₂(1241)	→	1242
1₂(1529)	→	1530
1₂(1072)	→	1073
1₂(1384)	→	1385
1₂(1005)	→	1006
1₂(1216)	→	1217
1₂(1209)	→	1210
1₂(1220)	→	1221
1₂(530)	→	531
1₂(987)	→	988
1₂(1202)	→	1203
1₂(1243)	→	1244
1₂(1204)	→	1205
1₂(1003)	→	1004
1₂(1574)	→	1575
1₂(1219)	→	1220
1₂(972)	→	973
1₂(1359)	→	1360
1₂(999)	→	1000
1₂(1568)	→	1569
1₂(1053)	→	1054
1₂(1206)	→	1207
1₂(1007)	→	1008
1₂(1050)	→	1051
1₂(1361)	→	1362
1₂(1403)	→	1404
1₂(1049)	→	1050
1₂(1386)	→	1387
1₂(536)	→	537
1₂(1434)	→	1435
1₂(1198)	→	1199
1₂(1566)	→	1567

The automaton is closed under rewriting as it is compatible.