Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3533)

The rewrite relation of the following TRS is considered.

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

{6, 5, 4, 3, 2, 1}

transitions:

1374	→	728
1206	→	637
1400	→	1590
1400	→	1592
1400	→	1600
1380	→	733
329	→	1472
329	→	1578
376	→	2
376	→	624
376	→	298
376	→	627
376	→	349
376	→	9
376	→	301
376	→	66
376	→	602
457	→	4
457	→	510
457	→	661
534	→	915
534	→	1056
534	→	1227
633	→	1211
731	→	234
1573	→	694
1437	→	399
1579	→	694
685	→	1060
685	→	1335
685	→	1402
89	→	448
89	→	626
89	→	723
1459	→	500
745	→	1385
745	→	1428
1513	→	660
1057	→	500
1441	→	448
1529	→	667
1529	→	1554
750	→	740
1463	→	526
1463	→	1480
87	→	9
87	→	347
87	→	618
98	→	2
98	→	87
98	→	596
98	→	627
98	→	1210
1072	→	1061
1475	→	526
1475	→	1492
855	→	840
10	→	1203
1169	→	588
97	→	826
97	→	881
1557	→	9
537	→	527
537	→	739
487	→	459
487	→	1209
571	→	545
1431	→	300
1479	→	545
578	→	306
1473	→	526
1473	→	1490
641	→	633
96	→	1263
1435	→	399
438	→	1438
438	→	1506
438	→	1586
608	→	406
882	→	870
1593	→	89
1386	→	163
543	→	527
543	→	1153
706	→	695
502	→	574
659	→	97
122	→	89
122	→	6
122	→	142
299	→	251
299	→	490
466	→	789
668	→	998
668	→	1373
878	→	870
585	→	1174
585	→	1217
625	→	610
676	→	1
676	→	399
676	→	439
18	→	1
18	→	399
18	→	439
227	→	163
227	→	367
227	→	703
227	→	499
227	→	398
227	→	88
227	→	65
227	→	193
227	→	458
227	→	5
1118	→	500
226	→	1416
226	→	1496
815	→	1379
41	→	9
41	→	250
120	→	89
3	→	86
3	→	119
3	→	206
3	→	418
3	→	484
3	→	509
1483	→	545
939	→	1168
653	→	687
600	→	592
1003	→	1446
1003	→	1516
1003	→	1558
1565	→	694
500	→	542
500	→	572
500	→	667
500	→	677
617	→	375
460	→	635
460	→	715
460	→	980
1531	→	667
1531	→	1546
838	→	15
1495	→	545
1062	→	1140
1226	→	660
1074	→	1061
1258	→	1234
1258	→	1301
347	→	1470
347	→	1572
1359	→	510
1359	→	4
1359	→	661
1340	→	694
1467	→	526
1467	→	1484
9	→	298
9	→	349
9	→	624
1332	→	652
5	→	65
5	→	88
5	→	193
5	→	398
5	→	458
5	→	499
209	→	163
209	→	694
1126	→	500
65	→	1476
65	→	1584
1124	→	500
1055	→	500
456	→	1071
456	→	1339
483	→	459
947	→	435
947	→	1
947	→	90
1220	→	660
973	→	962
674	→	1377
616	→	1117
1344	→	709
397	→	368
446	→	1290
467	→	762
467	→	1054
467	→	1225
495	→	1052
713	→	1233
938	→	1193
1601	→	500
1403	→	1392
1493	→	545
1	→	40
1	→	121
1	→	226
1	→	420
1	→	480
1	→	515
1471	→	526
1471	→	1488
1443	→	448
1591	→	250
1298	→	1450
1299	→	1391
1299	→	1460
1299	→	1560
1489	→	545
977	→	962
1112	→	545
527	→	1500
1004	→	677
1004	→	572
1004	→	544
1004	→	500
1004	→	579
1004	→	517
1004	→	432
1004	→	139
1004	→	42
1004	→	162
1004	→	486
1004	→	4
1004	→	449
1004	→	526
1004	→	523
1509	→	660
1154	→	581
770	→	1389
770	→	1430
1228	→	660
1317	→	1292
1507	→	609
987	→	510
987	→	4
987	→	661
1342	→	694
1376	→	667
1515	→	660
1208	→	636
970	→	1462
970	→	1562
1194	→	602
1547	→	678
748	→	740
634	→	97
769	→	1536
261	→	251
573	→	545
330	→	301
1070	→	707
1070	→	459
1070	→	595
1070	→	509
1070	→	418
1070	→	119
1070	→	86
1070	→	206
1070	→	484
1070	→	3
1070	→	400
1070	→	481
1070	→	1511
235	→	5
235	→	705
235	→	440
235	→	703
235	→	163
235	→	367
235	→	227
235	→	207
675	→	937
675	→	1195
675	→	1349
1348	→	711
1503	→	399
309	→	6
309	→	723
309	→	448
309	→	89
309	→	142
309	→	708
309	→	120
91	→	893
518	→	500
518	→	538
518	→	568
170	→	856
349	→	1464
349	→	1564
1212	→	544
161	→	89
161	→	1345
916	→	903
1499	→	500
619	→	610
702	→	685
552	→	308
912	→	624
912	→	298
912	→	2
912	→	627
912	→	349
912	→	9
441	→	587
441	→	1375
407	→	974
407	→	1255
407	→	1331
1453	→	500
207	→	163
894	→	370
172	→	1
172	→	399
172	→	419
172	→	435
172	→	90
918	→	903
788	→	764
911	→	1440
911	→	1530
911	→	1556
1358	→	1448
1358	→	1528
121	→	1436
121	→	1458
121	→	1510
1382	→	790
171	→	961
171	→	1257
1477	→	526
1477	→	1494
6	→	8
6	→	141
6	→	208
6	→	434
6	→	482
6	→	522
1053	→	500
773	→	764
1256	→	1234
1256	→	1314
1336	→	694
1539	→	677
1571	→	694
468	→	4
468	→	510
468	→	661
986	→	1383
986	→	1454
986	→	1512
1417	→	250
823	→	399
823	→	515
823	→	420
823	→	121
823	→	40
823	→	226
823	→	480
823	→	1
823	→	419
799	→	596
1302	→	1292
308	→	917
308	→	1058
308	→	1219
1585	→	694
498	→	4
498	→	677
498	→	572
498	→	544
498	→	500
498	→	579
498	→	449
498	→	526
498	→	523
498	→	566
498	→	536
498	→	516
498	→	510
498	→	661
498	→	1497
498	→	1459
283	→	251
433	→	399
433	→	774
1146	→	300
485	→	459
1192	→	601
350	→	301
1346	→	709
525	→	500
525	→	540
525	→	570
569	→	545
301	→	624
301	→	298
301	→	327
301	→	9
301	→	524
301	→	438
301	→	160
301	→	63
301	→	191
301	→	488
301	→	2
301	→	260
301	→	620
301	→	64
301	→	350
301	→	609
301	→	1507
2	→	63
2	→	160
2	→	191
2	→	438
2	→	488
2	→	524
1175	→	399
11	→	228
11	→	1333
686	→	1
686	→	399
686	→	439
686	→	678
686	→	433
4	→	42
4	→	139
4	→	162
4	→	432
4	→	486
4	→	517
528	→	836
449	→	579
876	→	16
400	→	595
1069	→	1434
1069	→	1456
1069	→	1514
827	→	814
258	→	854
258	→	1123
1501	→	581
1425	→	250
419	→	399
419	→	772
1451	→	448
904	→	1176
1001	→	1452
300	→	1466
300	→	1570
593	→	1191
281	→	251
508	→	234
1587	→	459
66	→	9
66	→	282
66	→	329
66	→	622
66	→	2
1535	→	667
1535	→	1542
1390	→	163
1505	→	602
1059	→	500
704	→	695
1461	→	526
1461	→	1478
481	→	459
971	→	510
971	→	4
971	→	661
421	→	399
1334	→	689
516	→	500
516	→	536
516	→	566
535	→	3
535	→	707
535	→	459
535	→	595
535	→	400
535	→	481
535	→	1511
1491	→	545
348	→	301
623	→	610
1555	→	678
738	→	730
985	→	1381
1145	→	1502
1145	→	1508
684	→	976
497	→	972
497	→	1240
497	→	1329
1177	→	596
1533	→	667
1533	→	1540
708	→	1347
596	→	1205
140	→	89
140	→	1343
1315	→	1292
1378	→	163
1455	→	500
1517	→	667
1517	→	1548
1497	→	500
944	→	1538
746	→	399
746	→	515
746	→	420
746	→	121
746	→	40
746	→	226
746	→	480
746	→	1
746	→	439
1543	→	678
1559	→	9
1006	→	667
621	→	610
1401	→	1005
1401	→	601
1401	→	396
1401	→	367
1401	→	5
1401	→	163
1401	→	703
1401	→	227
1202	→	507
234	→	839
234	→	1125
1563	→	694
1204	→	629
1239	→	640
1581	→	694
64	→	9
64	→	260
64	→	327
64	→	620
1384	→	90
1384	→	1432
1541	→	678
825	→	814
763	→	903
1447	→	448
586	→	375
1429	→	300
821	→	1424
771	→	87
771	→	524
771	→	438
771	→	160
771	→	63
771	→	191
771	→	488
771	→	2
771	→	596
17	→	824
17	→	877
946	→	1442
946	→	1532
945	→	1422
510	→	500
714	→	496
1537	→	667
1549	→	678
164	→	732
1433	→	400
1439	→	440
1439	→	1504
666	→	15
567	→	545
693	→	675
1419	→	250
1457	→	500
722	→	497
523	→	500
523	→	526
523	→	544
142	→	89
1445	→	448
489	→	459
489	→	1207
1264	→	1234
259	→	6
259	→	723
259	→	448
259	→	89
259	→	161
848	→	1418
848	→	1498
1561	→	694
378	→	368
775	→	764
375	→	1073
375	→	1341
541	→	527
541	→	749
1210	→	636
328	→	301
43	→	9
43	→	280
43	→	300
43	→	609
594	→	375
1218	→	660
1481	→	545
1241	→	1234
1241	→	1316
822	→	1444
822	→	1534
1449	→	448
194	→	163
1152	→	581
1423	→	250
447	→	170
163	→	396
163	→	440
163	→	601
163	→	705
163	→	1005
439	→	399
439	→	515
439	→	420
439	→	121
439	→	40
439	→	226
439	→	480
439	→	1
539	→	527
539	→	747
539	→	1151
1330	→	652
1511	→	660
975	→	962
1485	→	545
1465	→	526
1465	→	1482
1300	→	399
1300	→	515
1300	→	420
1300	→	121
1300	→	40
1300	→	226
1300	→	480
1300	→	1
1300	→	439
192	→	163
192	→	377
1061	→	1111
849	→	723
849	→	448
849	→	6
849	→	89
849	→	161
327	→	1474
327	→	1580
408	→	2
408	→	624
408	→	298
408	→	627
408	→	349
408	→	9
408	→	250
408	→	41
408	→	1417
459	→	660
459	→	707
857	→	840
545	→	652
435	→	399
435	→	787
307	→	813
307	→	869
1₁(529)	→	530
1₁(434)	→	435
1₁(905)	→	906
1₁(1502)	→	1503
1₁(675)	→	676
1₁(1174)	→	1175
1₁(732)	→	733
1₁(438)	→	439
1₁(1540)	→	1541
1₁(1316)	→	1317
1₁(461)	→	462
1₁(532)	→	533
1₁(587)	→	588
1₁(1379)	→	1380
1₁(1434)	→	1435
1₁(398)	→	399
1₁(872)	→	873
1₁(630)	→	631
1₁(1168)	→	1169
1₁(401)	→	402
1₁(740)	→	741
1₁(980)	→	981
1₁(369)	→	370
1₁(915)	→	916
1₁(690)	→	691
1₁(1064)	→	1065
1₁(762)	→	763
1₁(677)	→	678
1₁(593)	→	594
1₁(632)	→	633
1₁(1383)	→	1384
1₁(432)	→	433
1₁(418)	→	419
1₁(12)	→	13
1₁(367)	→	368
1₁(420)	→	421
1₁(89)	→	90
1₁(1291)	→	1292
1₁(893)	→	894
1₁(377)	→	378
1₁(917)	→	918
1₁(1436)	→	1437
1₁(1542)	→	1543
1₁(302)	→	303
1₁(1546)	→	1547
1₁(1548)	→	1549
1₁(1554)	→	1555
1₁(1301)	→	1302
1₁(655)	→	656
1₁(1314)	→	1315
1₁(1067)	→	1068
1₁(396)	→	397
1₁(550)	→	551
1₂(790)	→	791
4₂(797)	→	798
4₂(1396)	→	1397
4₂(793)	→	794
2₂(1399)	→	1400
2₂(798)	→	799
2₂(796)	→	797
2₂(1392)	→	1393
2₂(1397)	→	1398
2₂(794)	→	795
2₂(1398)	→	1399
4₁(1358)	→	1359
4₁(618)	→	619
4₁(371)	→	372
4₁(1298)	→	1299
4₁(1238)	→	1239
4₁(1225)	→	1226
4₁(1198)	→	1199
4₁(407)	→	408
4₁(842)	→	843
4₁(1586)	→	1587
4₁(399)	→	400
4₁(696)	→	697
4₁(1354)	→	1355
4₁(708)	→	709
4₁(662)	→	663
4₁(1217)	→	1218
4₁(603)	→	604
4₁(1514)	→	1515
4₁(1333)	→	1334
4₁(445)	→	446
4₁(1508)	→	1509
4₁(822)	→	823
4₁(230)	→	231
4₁(1350)	→	1351
4₁(622)	→	623
4₁(700)	→	701
4₁(721)	→	722
4₁(1432)	→	1433
4₁(612)	→	613
4₁(1343)	→	1344
4₁(620)	→	621
4₁(983)	→	984
4₁(946)	→	947
4₁(688)	→	689
4₁(446)	→	447
4₁(654)	→	655
4₁(484)	→	485
4₁(769)	→	770
4₁(497)	→	498
4₁(1510)	→	1511
4₁(460)	→	461
4₁(846)	→	847
4₁(92)	→	93
4₁(765)	→	766
4₁(1345)	→	1346
4₁(943)	→	944
4₁(464)	→	465
4₁(703)	→	704
4₁(670)	→	671
4₁(694)	→	695
4₁(591)	→	592
4₁(96)	→	97
4₁(713)	→	714
4₁(611)	→	612
4₁(705)	→	706
4₁(718)	→	719
4₁(488)	→	489
4₁(252)	→	253
4₁(1003)	→	1004
4₁(574)	→	575
4₁(1227)	→	1228
4₁(1357)	→	1358
4₁(256)	→	257
4₁(1349)	→	1350
4₁(459)	→	460
4₁(944)	→	945
4₁(837)	→	838
4₁(171)	→	172
4₁(903)	→	904
4₁(1196)	→	1197
4₁(911)	→	912
4₁(671)	→	672
4₁(684)	→	685
4₁(458)	→	459
4₁(486)	→	487
4₁(1219)	→	1220
4₁(480)	→	481
4₁(1199)	→	1200
4₁(609)	→	610
4₁(501)	→	502
4₁(482)	→	483
4₁(711)	→	712
4₁(1512)	→	1513
4₁(1237)	→	1238
4₁(624)	→	625
3₀(3)	→	5
3₀(6)	→	5
3₀(5)	→	5
3₀(4)	→	5
3₀(2)	→	5
3₀(1)	→	5
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
5₂(789)	→	790
5₂(1381)	→	1382
5₂(1393)	→	1394
2₀(1)	→	4
2₀(6)	→	4
2₀(3)	→	4
2₀(5)	→	4
2₀(2)	→	4
2₀(4)	→	4
3₁(170)	→	171
3₁(1143)	→	1144
3₁(1578)	→	1579
3₁(841)	→	842
3₁(191)	→	192
3₁(1292)	→	1293
3₁(1201)	→	1202
3₁(1356)	→	1357
3₁(599)	→	600
3₁(1385)	→	1386
3₁(695)	→	696
3₁(614)	→	615
3₁(1065)	→	1066
3₁(372)	→	373
3₁(764)	→	765
3₁(873)	→	874
3₁(824)	→	825
3₁(208)	→	209
3₁(826)	→	827
3₁(500)	→	501
3₁(370)	→	371
3₁(597)	→	598
3₁(966)	→	967
3₁(282)	→	283
3₁(730)	→	731
3₁(741)	→	742
3₁(682)	→	683
3₁(260)	→	261
3₁(400)	→	401
3₁(465)	→	466
3₁(226)	→	227
3₁(304)	→	305
3₁(616)	→	617
3₁(1377)	→	1378
3₁(1000)	→	1001
3₁(657)	→	658
3₁(821)	→	822
3₁(1339)	→	1340
3₁(13)	→	14
3₁(494)	→	495
3₁(162)	→	163
3₁(234)	→	235
3₁(530)	→	531
3₁(583)	→	584
3₁(280)	→	281
3₁(937)	→	938
3₁(527)	→	528
3₁(736)	→	737
3₁(451)	→	452
3₁(984)	→	985
3₁(545)	→	546
3₁(452)	→	453
3₁(982)	→	983
3₁(848)	→	849
3₁(463)	→	464
3₁(904)	→	905
3₁(735)	→	736
3₁(1560)	→	1561
3₁(453)	→	454
3₁(251)	→	252
3₁(193)	→	194
3₁(840)	→	841
3₁(968)	→	969
3₁(14)	→	15
3₁(938)	→	939
3₁(298)	→	299
3₁(1191)	→	1192
3₁(1335)	→	1336
3₁(206)	→	207
3₁(678)	→	679
3₁(605)	→	606
3₁(454)	→	455
3₁(1562)	→	1563
3₁(724)	→	725
3₁(813)	→	814
3₁(664)	→	665
3₁(229)	→	230
3₁(712)	→	713
3₁(1572)	→	1573
3₁(737)	→	738
3₁(945)	→	946
3₁(656)	→	657
3₁(1438)	→	1439
3₁(1341)	→	1342
3₁(250)	→	251
3₁(1347)	→	1348
3₁(874)	→	875
3₁(836)	→	837
3₁(1141)	→	1142
3₁(967)	→	968
3₁(581)	→	582
3₁(1389)	→	1390
3₁(698)	→	699
3₁(606)	→	607
3₁(1592)	→	1593
3₁(1564)	→	1565
3₁(228)	→	229
3₁(1570)	→	1571
3₁(1296)	→	1297
3₁(303)	→	304
3₁(91)	→	92
3₁(440)	→	441
3₁(965)	→	966
3₁(1580)	→	1581
3₁(1062)	→	1063
3₁(590)	→	591
3₁(710)	→	711
3₁(258)	→	259
3₁(720)	→	721
3₁(742)	→	743
3₁(1584)	→	1585
3₁(723)	→	724
2₁(549)	→	550
2₁(1530)	→	1531
2₁(502)	→	503
2₁(962)	→	963
2₁(1071)	→	1072
2₁(1466)	→	1467
2₁(674)	→	675
2₁(517)	→	518
2₁(743)	→	744
2₁(1460)	→	1461
2₁(1257)	→	1258
2₁(1458)	→	1459
2₁(93)	→	94
2₁(1005)	→	1006
2₁(16)	→	17
2₁(844)	→	845
2₁(576)	→	577
2₁(509)	→	510
2₁(506)	→	507
2₁(1351)	→	1352
2₁(1454)	→	1455
2₁(1073)	→	1074
2₁(233)	→	234
2₁(592)	→	593
2₁(577)	→	578
2₁(462)	→	463
2₁(669)	→	670
2₁(817)	→	818
2₁(1263)	→	1264
2₁(490)	→	491
2₁(531)	→	532
2₁(575)	→	576
2₁(744)	→	745
2₁(166)	→	167
2₁(448)	→	449
2₁(701)	→	702
2₁(232)	→	233
2₁(97)	→	98
2₁(95)	→	96
2₁(1476)	→	1477
2₁(1060)	→	1061
2₁(1456)	→	1457
2₁(1462)	→	1463
2₁(699)	→	700
2₁(1464)	→	1465
2₁(1498)	→	1499
2₁(491)	→	492
2₁(691)	→	692
2₁(1294)	→	1295
2₁(716)	→	717
2₁(661)	→	662
2₁(766)	→	767
2₁(9)	→	10
2₁(627)	→	628
2₁(524)	→	525
2₁(969)	→	970
2₁(667)	→	668
2₁(1240)	→	1241
2₁(1528)	→	1529
2₁(818)	→	819
2₁(1117)	→	1118
2₁(1470)	→	1471
2₁(636)	→	637
2₁(167)	→	168
2₁(1233)	→	1234
2₁(547)	→	548
2₁(907)	→	908
2₁(734)	→	735
2₁(306)	→	307
2₁(499)	→	500
2₁(745)	→	746
2₁(1054)	→	1055
2₁(1538)	→	1539
2₁(1536)	→	1537
2₁(1235)	→	1236
2₁(522)	→	523
2₁(1474)	→	1475
2₁(768)	→	769
2₁(307)	→	308
2₁(1255)	→	1256
2₁(1375)	→	1376
2₁(1516)	→	1517
2₁(770)	→	771
2₁(1234)	→	1235
2₁(1452)	→	1453
2₁(715)	→	716
2₁(726)	→	727
2₁(725)	→	726
2₁(1002)	→	1003
2₁(1056)	→	1057
2₁(1125)	→	1126
2₁(1211)	→	1212
2₁(1534)	→	1535
2₁(845)	→	846
2₁(231)	→	232
2₁(1600)	→	1601
2₁(496)	→	497
2₁(255)	→	256
2₁(374)	→	375
2₁(1472)	→	1473
2₁(658)	→	659
2₁(1290)	→	1291
2₁(546)	→	547
2₁(1058)	→	1059
2₁(1063)	→	1064
2₁(505)	→	506
2₁(1052)	→	1053
2₁(406)	→	407
2₁(455)	→	456
2₁(1352)	→	1353
2₁(1496)	→	1497
2₁(652)	→	653
2₁(403)	→	404
2₁(1236)	→	1237
2₁(660)	→	661
2₁(17)	→	18
2₁(1123)	→	1124
2₁(665)	→	666
2₁(15)	→	16
2₁(254)	→	255
2₁(653)	→	654
2₁(1066)	→	1067
2₁(1532)	→	1533
2₁(515)	→	516
2₁(680)	→	681
2₁(1205)	→	1206
2₁(607)	→	608
2₁(668)	→	669
2₁(910)	→	911
2₁(981)	→	982
2₁(528)	→	529
0₀(3)	→	2
0₀(5)	→	2
0₀(2)	→	2
0₀(4)	→	2
0₀(1)	→	2
0₀(6)	→	2
4₀(2)	→	3
4₀(4)	→	3
4₀(3)	→	3
4₀(6)	→	3
4₀(1)	→	3
4₀(5)	→	3
5₁(689)	→	690
5₁(707)	→	708
5₁(534)	→	535
5₁(584)	→	585
5₁(999)	→	1000
5₁(538)	→	539
5₁(814)	→	815
5₁(257)	→	258
5₁(615)	→	616
5₁(1446)	→	1447
5₁(610)	→	611
5₁(1442)	→	1443
5₁(526)	→	527
5₁(492)	→	493
5₁(683)	→	684
5₁(308)	→	309
5₁(1200)	→	1201
5₁(986)	→	987
5₁(373)	→	374
5₁(964)	→	965
5₁(729)	→	730
5₁(687)	→	688
5₁(169)	→	170
5₁(709)	→	710
5₁(1448)	→	1449
5₁(88)	→	89
5₁(1001)	→	1002
5₁(820)	→	821
5₁(493)	→	494
5₁(719)	→	720
5₁(681)	→	682
5₁(582)	→	583
5₁(871)	→	872
5₁(974)	→	975
5₁(536)	→	537
5₁(976)	→	977
5₁(906)	→	907
5₁(589)	→	590
5₁(467)	→	468
5₁(121)	→	122
5₁(1444)	→	1445
5₁(139)	→	140
5₁(507)	→	508
5₁(540)	→	541
5₁(119)	→	120
5₁(663)	→	664
5₁(1297)	→	1298
5₁(629)	→	630
5₁(961)	→	962
5₁(631)	→	632
5₁(1197)	→	1198
5₁(585)	→	586
5₁(466)	→	467
5₁(985)	→	986
5₁(1145)	→	1146
5₁(613)	→	614
5₁(402)	→	403
5₁(847)	→	848
5₁(542)	→	543
5₁(11)	→	12
5₁(749)	→	750
5₁(1144)	→	1145
5₁(638)	→	639
5₁(10)	→	11
5₁(450)	→	451
5₁(598)	→	599
5₁(1142)	→	1143
5₁(1061)	→	1062
5₁(160)	→	161
5₁(637)	→	638
5₁(1355)	→	1356
5₁(972)	→	973
5₁(495)	→	496
5₁(163)	→	164
5₁(1450)	→	1451
5₁(747)	→	748
5₁(141)	→	142
5₁(998)	→	999
5₁(441)	→	442
5₁(739)	→	740
5₁(1069)	→	1070
5₁(939)	→	940
5₁(301)	→	302
5₁(503)	→	504
5₁(1295)	→	1296
5₁(1440)	→	1441
5₁(579)	→	580
0₁(774)	→	775
0₁(1506)	→	1507
0₁(1492)	→	1493
0₁(685)	→	686
0₁(1494)	→	1495
0₁(165)	→	166
0₁(570)	→	571
0₁(1203)	→	1204
0₁(65)	→	66
0₁(327)	→	328
0₁(305)	→	306
0₁(329)	→	330
0₁(819)	→	820
0₁(1353)	→	1354
0₁(815)	→	816
0₁(596)	→	597
0₁(404)	→	405
0₁(1153)	→	1154
0₁(940)	→	941
0₁(1140)	→	1141
0₁(40)	→	41
0₁(347)	→	348
0₁(551)	→	552
0₁(1478)	→	1479
0₁(1209)	→	1210
0₁(1556)	→	1557
0₁(1490)	→	1491
0₁(908)	→	909
0₁(63)	→	64
0₁(1331)	→	1332
0₁(368)	→	369
0₁(1428)	→	1429
0₁(1484)	→	1485
0₁(1373)	→	1374
0₁(772)	→	773
0₁(444)	→	445
0₁(601)	→	602
0₁(875)	→	876
0₁(580)	→	581
0₁(854)	→	855
0₁(856)	→	857
0₁(1430)	→	1431
0₁(1299)	→	1300
0₁(300)	→	301
0₁(640)	→	641
0₁(877)	→	878
0₁(566)	→	567
0₁(1480)	→	1481
0₁(504)	→	505
0₁(1482)	→	1483
0₁(1193)	→	1194
0₁(1424)	→	1425
0₁(1151)	→	1152
0₁(588)	→	589
0₁(1558)	→	1559
0₁(1293)	→	1294
0₁(443)	→	444
0₁(604)	→	605
0₁(941)	→	942
0₁(679)	→	680
0₁(42)	→	43
0₁(870)	→	871
0₁(90)	→	91
0₁(1111)	→	1112
0₁(635)	→	636
0₁(1416)	→	1417
0₁(349)	→	350
0₁(1488)	→	1489
0₁(633)	→	634
0₁(843)	→	844
0₁(602)	→	603
0₁(733)	→	734
0₁(1068)	→	1069
0₁(1329)	→	1330
0₁(86)	→	87
0₁(869)	→	870
0₁(405)	→	406
0₁(164)	→	165
0₁(639)	→	640
0₁(697)	→	698
0₁(1176)	→	1177
0₁(168)	→	169
0₁(767)	→	768
0₁(544)	→	545
0₁(533)	→	534
0₁(1195)	→	1196
0₁(1207)	→	1208
0₁(909)	→	910
0₁(94)	→	95
0₁(548)	→	549
0₁(816)	→	817
0₁(692)	→	693
0₁(375)	→	376
0₁(1418)	→	1419
0₁(456)	→	457
0₁(963)	→	964
0₁(1422)	→	1423
0₁(628)	→	629
0₁(672)	→	673
0₁(673)	→	674
0₁(970)	→	971
0₁(626)	→	627
0₁(881)	→	882
0₁(727)	→	728
0₁(1504)	→	1505
0₁(1590)	→	1591
0₁(568)	→	569
0₁(787)	→	788
0₁(442)	→	443
0₁(253)	→	254
0₁(942)	→	943
0₁(572)	→	573
0₁(717)	→	718
0₁(728)	→	729
0₁(8)	→	9
0₁(1500)	→	1501
0₁(595)	→	596
0₁(763)	→	764
0₁(449)	→	450
0₁(839)	→	840
3₂(1395)	→	1396
3₂(1400)	→	1401
3₂(1394)	→	1395
3₂(792)	→	793
1₀(1)	→	1
1₀(6)	→	1
1₀(5)	→	1
1₀(2)	→	1
1₀(3)	→	1
1₀(4)	→	1
0₂(1391)	→	1392
0₂(791)	→	792
0₂(1402)	→	1403
0₂(795)	→	796

The automaton is closed under rewriting as it is compatible.