Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/95858)

The rewrite relation of the following TRS is considered.

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

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:

1067	→	1491
854	→	583
854	→	601
23	→	9
23	→	594
23	→	821
25	→	9
25	→	582
25	→	803
457	→	439
731	→	59
1191	→	663
1496	→	703
202	→	10
830	→	804
1492	→	679
1072	→	1059
1072	→	1146
10	→	765
10	→	935
10	→	992
1379	→	56
537	→	6
537	→	748
537	→	439
537	→	455
1546	→	1013
571	→	511
96	→	56
96	→	619
1209	→	679
471	→	1331
1544	→	1013
1498	→	527
543	→	528
1195	→	662
472	→	1025
502	→	297
119	→	56
119	→	617
595	→	583
145	→	121
122	→	330
878	→	1384
878	→	1443
1408	→	198
491	→	465
491	→	542
491	→	576
260	→	198
547	→	528
1098	→	748
1098	→	439
1098	→	488
1098	→	227
1098	→	76
1098	→	24
1098	→	169
1098	→	452
1098	→	6
1098	→	455
1098	→	1454
226	→	198
3	→	37
3	→	93
3	→	142
3	→	257
3	→	454
3	→	490
1246	→	716
57	→	650
1254	→	737
1033	→	74
1033	→	1499
1011	→	378
500	→	1259
907	→	713
1226	→	592
626	→	603
1074	→	1059
1074	→	1132
805	→	933
298	→	1
298	→	143
298	→	337
298	→	145
298	→	583
298	→	601
298	→	561
298	→	581
298	→	573
298	→	981
1424	→	198
1340	→	1495
9	→	423
9	→	600
9	→	662
9	→	715
9	→	829
1332	→	804
620	→	603
5	→	8
5	→	55
5	→	167
5	→	197
5	→	438
5	→	484
341	→	123
59	→	872
59	→	900
59	→	980
59	→	1023
59	→	1073
59	→	1370
1454	→	439
199	→	293
199	→	1036
483	→	465
483	→	527
483	→	560
618	→	603
1252	→	737
1446	→	378
445	→	10
473	→	5
473	→	75
473	→	94
473	→	585
473	→	1379
473	→	1472
942	→	143
942	→	464
942	→	225
942	→	74
942	→	22
942	→	195
942	→	446
942	→	1
942	→	337
1448	→	378
1416	→	198
1530	→	1013
1	→	22
1	→	74
1	→	195
1	→	225
1	→	446
1	→	464
40	→	9
40	→	378
40	→	596
40	→	825
826	→	804
1430	→	378
877	→	1483
877	→	1493
936	→	1091
690	→	472
716	→	1253
549	→	528
549	→	648
1022	→	439
901	→	713
601	→	583
940	→	1423
570	→	986
570	→	1012
524	→	6
524	→	628
524	→	459
524	→	663
524	→	649
524	→	737
524	→	1254
524	→	1189
524	→	1191
1387	→	198
490	→	1415
490	→	1439
490	→	1517
60	→	3
60	→	492
60	→	336
60	→	198
60	→	765
60	→	10
60	→	292
60	→	466
60	→	260
60	→	226
60	→	258
60	→	493
60	→	584
60	→	1131
60	→	1091
60	→	936
60	→	1410
60	→	853
60	→	1402
60	→	1471
60	→	1404
60	→	1416
60	→	338
1215	→	1339
747	→	469
987	→	378
677	→	1
677	→	561
677	→	678
677	→	425
677	→	503
677	→	121
677	→	581
677	→	145
677	→	583
677	→	597
677	→	601
677	→	1265
677	→	337
677	→	981
488	→	1413
488	→	1437
488	→	1527
573	→	561
1070	→	628
1070	→	459
1070	→	6
1070	→	663
1070	→	649
1070	→	1189
1070	→	1191
993	→	378
297	→	1124
38	→	9
1428	→	337
296	→	953
1232	→	1215
1414	→	198
1373	→	852
512	→	2
512	→	831
512	→	379
512	→	54
512	→	294
512	→	702
512	→	424
512	→	378
512	→	1436
512	→	1434
512	→	1013
512	→	1014
512	→	1530
512	→	1536
58	→	851
58	→	876
58	→	1058
58	→	1427
170	→	121
1385	→	198
1402	→	198
1499	→	1551
1127	→	563
1410	→	198
614	→	523
983	→	338
1528	→	1013
526	→	514
257	→	1372
257	→	1376
257	→	1378
257	→	1453
257	→	1461
679	→	1126
121	→	425
121	→	503
121	→	678
121	→	1130
121	→	1537
597	→	583
6	→	24
6	→	76
6	→	169
6	→	227
6	→	452
6	→	488
1193	→	662
337	→	1265
1032	→	1497
577	→	561
1456	→	59
54	→	9
54	→	385
54	→	598
54	→	827
1438	→	378
384	→	10
1037	→	495
455	→	439
1282	→	145
1282	→	583
1282	→	464
1282	→	225
1282	→	74
1282	→	22
1282	→	195
1282	→	446
1282	→	1
1282	→	597
1282	→	601
431	→	340
75	→	56
75	→	602
75	→	5
75	→	679
1234	→	1216
1450	→	1013
386	→	379
484	→	1407
484	→	1433
484	→	1535
124	→	4
124	→	580
124	→	525
124	→	330
124	→	122
124	→	548
124	→	465
124	→	540
124	→	513
124	→	574
124	→	485
124	→	542
124	→	576
124	→	491
124	→	1456
124	→	1481
124	→	1462
1131	→	584
1377	→	9
292	→	198
764	→	297
764	→	1042
485	→	465
485	→	513
485	→	540
485	→	574
1500	→	472
143	→	121
1490	→	662
1516	→	1013
873	→	856
873	→	931
873	→	1188
873	→	1214
873	→	1243
2	→	53
2	→	118
2	→	144
2	→	291
2	→	458
2	→	474
11	→	1
11	→	583
11	→	678
11	→	425
11	→	121
11	→	145
11	→	601
11	→	597
11	→	626
11	→	563
11	→	168
11	→	599
11	→	1127
11	→	581
11	→	577
11	→	575
11	→	1265
11	→	337
11	→	981
954	→	936
4	→	39
4	→	95
4	→	120
4	→	259
4	→	456
4	→	482
528	→	783
528	→	1333
941	→	1469
1069	→	1421
1069	→	1441
258	→	198
258	→	3
258	→	1408
850	→	4
850	→	580
850	→	525
850	→	330
850	→	122
850	→	548
850	→	465
501	→	1034
1404	→	198
1404	→	1471
1538	→	1013
801	→	855
801	→	904
801	→	1021
801	→	1071
1035	→	1026
593	→	59
802	→	1
802	→	678
802	→	425
802	→	121
802	→	170
820	→	730
1452	→	439
1043	→	198
1470	→	74
504	→	984
887	→	607
1244	→	716
1244	→	1251
1334	→	806
535	→	1192
981	→	337
1125	→	561
1536	→	1013
738	→	1291
581	→	561
985	→	379
636	→	297
1143	→	561
1143	→	678
1143	→	425
1143	→	464
1143	→	225
1143	→	74
1143	→	22
1143	→	195
1143	→	446
1143	→	1
1143	→	503
1143	→	121
1143	→	581
1143	→	1265
1143	→	337
1143	→	981
1436	→	378
77	→	56
1482	→	627
335	→	59
1432	→	378
1440	→	378
753	→	880
1020	→	563
1020	→	1127
991	→	378
934	→	10
934	→	1152
1442	→	378
1307	→	678
1307	→	425
1307	→	1
1307	→	121
1307	→	170
579	→	561
453	→	439
1494	→	423
1357	→	464
856	→	1190
856	→	1231
856	→	1245
856	→	1485
948	→	936
828	→	804
763	→	906
198	→	336
198	→	492
905	→	713
1484	→	540
946	→	936
946	→	1128
714	→	58
1486	→	540
168	→	121
424	→	379
424	→	702
424	→	831
1129	→	585
1260	→	748
1464	→	513
1464	→	1479
464	→	1403
464	→	1431
464	→	1543
832	→	1233
858	→	583
858	→	678
858	→	425
858	→	1
858	→	121
858	→	145
858	→	601
1153	→	629
521	→	1208
1422	→	198
523	→	947
523	→	990
340	→	1194
482	→	1401
482	→	1429
482	→	1545
1434	→	378
489	→	465
489	→	546
489	→	578
74	→	1455
465	→	525
465	→	548
465	→	580
465	→	330
465	→	482
465	→	259
465	→	95
465	→	39
465	→	120
465	→	456
465	→	4
465	→	122
465	→	1370
465	→	1023
465	→	900
465	→	59
465	→	1456
1472	→	585
782	→	676
649	→	628
932	→	200
1444	→	378
541	→	528
541	→	627
575	→	561
474	→	1409
474	→	1435
474	→	1529
1306	→	1374
1306	→	1380
1306	→	1451
1306	→	1463
1375	→	9
1518	→	1013
1480	→	627
660	→	1447
660	→	1449
1552	→	439
822	→	804
603	→	884
447	→	439
1371	→	852
439	→	734
439	→	748
539	→	528
56	→	625
475	→	465
475	→	538
475	→	572
599	→	583
94	→	56
1147	→	627
849	→	945
849	→	1010
849	→	1515
1381	→	56
1096	→	1489
661	→	334
228	→	198
1189	→	663
1462	→	513
1462	→	1481
1024	→	439
459	→	439
879	→	678
879	→	425
879	→	1
879	→	121
879	→	145
883	→	757
196	→	121
196	→	982
857	→	1386
857	→	1445
5₁(941)	→	942
5₁(680)	→	681
5₁(1094)	→	1095
5₁(339)	→	340
5₁(438)	→	439
5₁(749)	→	750
5₁(627)	→	628
5₁(832)	→	833
5₁(532)	→	533
5₁(446)	→	447
5₁(1093)	→	1094
5₁(1251)	→	1252
5₁(1354)	→	1355
5₁(458)	→	459
5₁(1353)	→	1354
5₁(1188)	→	1189
5₁(452)	→	453
5₁(1023)	→	1024
5₁(679)	→	680
5₁(443)	→	444
5₁(1340)	→	1341
5₁(846)	→	847
5₁(533)	→	534
5₁(836)	→	837
5₁(933)	→	934
5₁(730)	→	731
5₁(1068)	→	1069
5₁(1152)	→	1153
5₁(806)	→	807
5₁(752)	→	753
5₁(1451)	→	1452
5₁(1036)	→	1037
5₁(1062)	→	1063
5₁(743)	→	744
5₁(635)	→	636
5₁(1259)	→	1260
5₁(1253)	→	1254
5₁(812)	→	813
5₁(609)	→	610
5₁(1190)	→	1191
5₁(425)	→	426
5₁(683)	→	684
5₁(589)	→	590
5₁(494)	→	495
5₁(788)	→	789
5₁(845)	→	846
5₁(297)	→	298
5₁(818)	→	819
5₁(1293)	→	1294
5₁(1280)	→	1281
5₁(456)	→	457
5₁(330)	→	331
5₁(608)	→	609
5₁(736)	→	737
5₁(1142)	→	1143
5₁(813)	→	814
5₁(662)	→	663
5₁(746)	→	747
5₁(1344)	→	1345
5₁(1453)	→	1454
5₁(628)	→	629
5₁(565)	→	566
5₁(1021)	→	1022
5₁(784)	→	785
5₁(1134)	→	1135
5₁(1141)	→	1142
5₁(201)	→	202
5₁(454)	→	455
5₁(726)	→	727
5₁(781)	→	782
5₁(648)	→	649
5₁(1551)	→	1552
5₁(739)	→	740
5₁(516)	→	517
5₁(1133)	→	1134
5₁(663)	→	664
5₁(522)	→	523
3₂(1014)	→	1015
3₂(1016)	→	1017
3₂(1019)	→	1020
3₂(886)	→	887
3₂(882)	→	883
3₂(853)	→	854
4₂(1018)	→	1019
4₁(1296)	→	1297
4₁(1276)	→	1277
4₁(675)	→	676
4₁(331)	→	332
4₁(659)	→	660
4₁(93)	→	94
4₁(585)	→	586
4₁(1225)	→	1226
4₁(1277)	→	1278
4₁(807)	→	808
4₁(1243)	→	1244
4₁(810)	→	811
4₁(469)	→	470
4₁(513)	→	514
4₁(1380)	→	1381
4₁(495)	→	496
4₁(791)	→	792
4₁(427)	→	428
4₁(840)	→	841
4₁(525)	→	526
4₁(1292)	→	1293
4₁(1348)	→	1349
4₁(841)	→	842
4₁(1215)	→	1216
4₁(778)	→	779
4₁(900)	→	901
4₁(712)	→	713
4₁(1471)	→	1472
4₁(776)	→	777
4₁(1059)	→	1060
4₁(1245)	→	1246
4₁(715)	→	716
4₁(584)	→	585
4₁(1304)	→	1305
4₁(906)	→	907
4₁(1223)	→	1224
4₁(472)	→	473
4₁(672)	→	673
4₁(1495)	→	1496
4₁(710)	→	711
4₁(904)	→	905
4₁(799)	→	800
4₁(1208)	→	1209
4₁(769)	→	770
4₁(748)	→	749
4₁(1064)	→	1065
4₁(787)	→	788
4₁(1345)	→	1346
4₁(811)	→	812
4₁(442)	→	443
4₁(74)	→	75
4₁(1268)	→	1269
4₁(713)	→	714
4₁(729)	→	730
4₁(496)	→	497
4₁(592)	→	593
4₁(678)	→	679
4₁(56)	→	57
4₁(1030)	→	1031
4₁(1233)	→	1234
4₁(777)	→	778
4₁(118)	→	119
4₁(55)	→	56
4₁(1491)	→	1492
4₁(759)	→	760
4₁(655)	→	656
4₁(95)	→	96
4₁(1349)	→	1350
4₁(657)	→	658
4₁(760)	→	761
4₁(783)	→	784
4₁(76)	→	77
4₁(702)	→	703
4₁(518)	→	519
4₁(837)	→	838
4₁(724)	→	725
4₁(735)	→	736
4₁(667)	→	668
4₁(1275)	→	1276
4₁(383)	→	384
4₁(817)	→	818
4₁(671)	→	672
4₁(681)	→	682
4₁(1128)	→	1129
4₁(501)	→	502
4₁(652)	→	653
4₁(1378)	→	1379
4₁(561)	→	562
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
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
3₁(827)	→	828
3₁(843)	→	844
3₁(849)	→	850
3₁(1497)	→	1498
3₁(506)	→	507
3₁(825)	→	826
3₁(1058)	→	1059
3₁(296)	→	297
3₁(1136)	→	1137
3₁(490)	→	491
3₁(1279)	→	1280
3₁(1063)	→	1064
3₁(1343)	→	1344
3₁(1065)	→	1066
3₁(771)	→	772
3₁(488)	→	489
3₁(829)	→	830
3₁(686)	→	687
3₁(1483)	→	1484
3₁(857)	→	858
3₁(1069)	→	1070
3₁(523)	→	524
3₁(1331)	→	1332
3₁(940)	→	941
3₁(789)	→	790
3₁(1137)	→	1138
3₁(821)	→	822
3₁(1073)	→	1074
3₁(467)	→	468
3₁(474)	→	475
3₁(530)	→	531
3₁(793)	→	794
3₁(685)	→	686
3₁(10)	→	11
3₁(1485)	→	1486
3₁(1455)	→	1456
3₁(1463)	→	1464
3₁(660)	→	661
3₁(688)	→	689
3₁(1270)	→	1271
3₁(1351)	→	1352
3₁(803)	→	804
3₁(1091)	→	1092
3₁(630)	→	631
3₁(631)	→	632
3₁(722)	→	723
3₁(439)	→	440
3₁(1025)	→	1026
3₁(665)	→	666
3₁(1034)	→	1035
3₁(805)	→	806
3₁(835)	→	836
3₁(1028)	→	1029
3₁(381)	→	382
3₁(878)	→	879
3₁(484)	→	485
3₁(707)	→	708
3₁(587)	→	588
3₁(379)	→	380
3₁(656)	→	657
3₁(121)	→	122
3₁(1298)	→	1299
3₁(780)	→	781
3₁(464)	→	465
3₁(633)	→	634
3₁(727)	→	728
3₁(517)	→	518
3₁(786)	→	787
3₁(1220)	→	1221
3₁(1333)	→	1334
3₁(773)	→	774
3₁(519)	→	520
3₁(199)	→	200
3₁(1342)	→	1343
3₁(931)	→	932
3₁(1139)	→	1140
3₁(1297)	→	1298
3₁(1294)	→	1295
3₁(1071)	→	1072
3₁(570)	→	571
3₁(1461)	→	1462
3₁(1272)	→	1273
3₁(482)	→	483
3₁(632)	→	633
3₁(1138)	→	1139
3₁(590)	→	591
3₁(1291)	→	1292
3₁(834)	→	835
3₁(792)	→	793
0₁(794)	→	795
0₁(798)	→	799
0₁(572)	→	573
0₁(602)	→	603
0₁(588)	→	589
0₁(765)	→	766
0₁(598)	→	599
0₁(606)	→	607
0₁(562)	→	563
0₁(758)	→	759
0₁(844)	→	845
0₁(576)	→	577
0₁(1301)	→	1302
0₁(566)	→	567
0₁(625)	→	626
0₁(669)	→	670
0₁(772)	→	773
0₁(1126)	→	1127
0₁(531)	→	532
0₁(756)	→	757
0₁(819)	→	820
0₁(582)	→	583
0₁(728)	→	729
0₁(709)	→	710
0₁(534)	→	535
0₁(1060)	→	1061
0₁(169)	→	170
0₁(796)	→	797
0₁(120)	→	121
0₁(1271)	→	1272
0₁(1299)	→	1300
0₁(594)	→	595
0₁(1469)	→	1470
0₁(429)	→	430
0₁(670)	→	671
0₁(766)	→	767
0₁(1266)	→	1267
0₁(1265)	→	1266
0₁(1303)	→	1304
0₁(596)	→	597
0₁(580)	→	581
0₁(591)	→	592
0₁(167)	→	168
0₁(574)	→	575
0₁(499)	→	500
0₁(745)	→	746
0₁(790)	→	791
0₁(611)	→	612
0₁(938)	→	939
0₁(144)	→	145
0₁(613)	→	614
0₁(560)	→	561
0₁(1095)	→	1096
0₁(718)	→	719
0₁(142)	→	143
0₁(514)	→	515
0₁(520)	→	521
0₁(612)	→	613
0₁(761)	→	762
0₁(1124)	→	1125
0₁(721)	→	722
0₁(1032)	→	1033
0₁(426)	→	427
0₁(471)	→	472
0₁(1295)	→	1296
0₁(666)	→	667
0₁(839)	→	840
0₁(617)	→	618
0₁(336)	→	337
0₁(1356)	→	1357
0₁(1092)	→	1093
0₁(619)	→	620
0₁(600)	→	601
0₁(508)	→	509
0₁(1352)	→	1353
0₁(848)	→	849
0₁(767)	→	768
0₁(294)	→	295
0₁(1222)	→	1223
0₁(567)	→	568
0₁(578)	→	579
0₁(1427)	→	1428
0₁(332)	→	333
0₁(1066)	→	1067
0₁(444)	→	445
0₁(195)	→	196
0₁(980)	→	981
0₁(1347)	→	1348
0₁(682)	→	683
0₁(668)	→	669
0₁(338)	→	339
1₀(3)	→	2
1₀(5)	→	2
1₀(2)	→	2
1₀(4)	→	2
1₀(1)	→	2
1₀(6)	→	2
2₀(2)	→	3
2₀(4)	→	3
2₀(3)	→	3
2₀(6)	→	3
2₀(1)	→	3
2₀(5)	→	3
2₁(816)	→	817
2₁(711)	→	712
2₁(225)	→	226
2₁(1413)	→	1414
2₁(1409)	→	1410
2₁(497)	→	498
2₁(1278)	→	1279
2₁(801)	→	802
2₁(947)	→	948
2₁(774)	→	775
2₁(814)	→	815
2₁(257)	→	258
2₁(1221)	→	1222
2₁(1403)	→	1404
2₁(58)	→	59
2₁(568)	→	569
2₁(563)	→	564
2₁(741)	→	742
2₁(610)	→	611
2₁(9)	→	10
2₁(504)	→	505
2₁(779)	→	780
2₁(720)	→	721
2₁(708)	→	709
2₁(684)	→	685
2₁(492)	→	493
2₁(856)	→	857
2₁(382)	→	383
2₁(1499)	→	1500
2₁(1306)	→	1307
2₁(1300)	→	1301
2₁(59)	→	60
2₁(674)	→	675
2₁(719)	→	720
2₁(1350)	→	1351
2₁(1346)	→	1347
2₁(750)	→	751
2₁(653)	→	654
2₁(1026)	→	1027
2₁(1130)	→	1131
2₁(935)	→	936
2₁(1421)	→	1422
2₁(1386)	→	1387
2₁(982)	→	983
2₁(795)	→	796
2₁(529)	→	530
2₁(333)	→	334
2₁(1042)	→	1043
2₁(1224)	→	1225
2₁(740)	→	741
2₁(1401)	→	1402
2₁(227)	→	228
2₁(295)	→	296
2₁(500)	→	501
2₁(945)	→	946
2₁(785)	→	786
2₁(763)	→	764
2₁(725)	→	726
2₁(753)	→	754
2₁(1269)	→	1270
2₁(603)	→	604
2₁(466)	→	467
2₁(842)	→	843
2₁(1096)	→	1097
2₁(1384)	→	1385
2₁(723)	→	724
2₁(833)	→	834
2₁(337)	→	338
2₁(673)	→	674
2₁(1423)	→	1424
2₁(1027)	→	1028
2₁(528)	→	529
2₁(953)	→	954
2₁(569)	→	570
2₁(515)	→	516
2₁(340)	→	341
2₁(583)	→	584
2₁(57)	→	58
2₁(197)	→	198
2₁(535)	→	536
2₁(754)	→	755
2₁(1061)	→	1062
2₁(877)	→	878
2₁(737)	→	738
2₁(738)	→	739
2₁(770)	→	771
2₁(1415)	→	1416
2₁(838)	→	839
2₁(465)	→	466
2₁(259)	→	260
2₁(1341)	→	1342
2₁(291)	→	292
2₁(939)	→	940
2₁(604)	→	605
2₁(1407)	→	1408
2₁(1273)	→	1274
1₁(1218)	→	1219
1₁(992)	→	993
1₁(441)	→	442
1₁(1219)	→	1220
1₁(53)	→	54
1₁(704)	→	705
1₁(505)	→	506
1₁(37)	→	38
1₁(1214)	→	1215
1₁(1135)	→	1136
1₁(470)	→	471
1₁(687)	→	688
1₁(1429)	→	1430
1₁(815)	→	816
1₁(876)	→	877
1₁(538)	→	539
1₁(676)	→	677
1₁(24)	→	25
1₁(123)	→	124
1₁(831)	→	832
1₁(428)	→	429
1₁(800)	→	801
1₁(198)	→	199
1₁(1140)	→	1141
1₁(1479)	→	1480
1₁(689)	→	690
1₁(855)	→	856
1₁(1355)	→	1356
1₁(22)	→	23
1₁(1437)	→	1438
1₁(1194)	→	1195
1₁(703)	→	704
1₁(498)	→	499
1₁(775)	→	776
1₁(39)	→	40
1₁(1192)	→	1193
1₁(1481)	→	1482
1₁(937)	→	938
1₁(510)	→	511
1₁(503)	→	504
1₁(564)	→	565
1₁(1231)	→	1232
1₁(1267)	→	1268
1₁(1029)	→	1030
1₁(334)	→	335
1₁(1302)	→	1303
1₁(293)	→	294
1₁(716)	→	717
1₁(664)	→	665
1₁(762)	→	763
1₁(1374)	→	1375
1₁(122)	→	123
1₁(536)	→	537
1₁(1439)	→	1440
1₁(1445)	→	1446
1₁(1217)	→	1218
1₁(607)	→	608
1₁(521)	→	522
1₁(542)	→	543
1₁(1489)	→	1490
1₁(546)	→	547
1₁(629)	→	630
1₁(872)	→	873
1₁(706)	→	707
1₁(847)	→	848
1₁(990)	→	991
1₁(705)	→	706
1₁(1447)	→	1448
1₁(511)	→	512
1₁(378)	→	379
1₁(1441)	→	1442
1₁(1097)	→	1098
1₁(1146)	→	1147
1₁(1339)	→	1340
1₁(1281)	→	1282
1₁(468)	→	469
1₁(755)	→	756
1₁(1443)	→	1444
1₁(804)	→	805
1₁(658)	→	659
1₁(1067)	→	1068
1₁(768)	→	769
1₁(493)	→	494
1₁(385)	→	386
1₁(380)	→	381
1₁(430)	→	431
1₁(527)	→	528
1₁(757)	→	758
1₁(605)	→	606
1₁(1493)	→	1494
1₁(742)	→	743
1₁(1433)	→	1434
1₁(751)	→	752
1₁(548)	→	549
1₁(651)	→	652
1₁(1031)	→	1032
1₁(507)	→	508
1₁(797)	→	798
1₁(809)	→	810
1₁(1216)	→	1217
1₁(650)	→	651
1₁(984)	→	985
1₁(1274)	→	1275
1₁(734)	→	735
1₁(586)	→	587
1₁(423)	→	424
1₁(986)	→	987
1₁(1431)	→	1432
1₁(1376)	→	1377
1₁(200)	→	201
1₁(1435)	→	1436
1₁(744)	→	745
1₁(509)	→	510
1₁(1010)	→	1011
1₁(634)	→	635
1₁(654)	→	655
1₁(936)	→	937
1₁(540)	→	541
1₁(440)	→	441
1₁(1132)	→	1133
1₁(808)	→	809
1₁(717)	→	718
1₁(8)	→	9
1₁(1305)	→	1306
1₂(1515)	→	1516
1₂(1545)	→	1546
1₂(1013)	→	1014
1₂(851)	→	852
1₂(1517)	→	1518
1₂(1535)	→	1536
1₂(1370)	→	1371
1₂(880)	→	881
1₂(1529)	→	1530
1₂(1449)	→	1450
1₂(1012)	→	1013
1₂(884)	→	885
1₂(1543)	→	1544
1₂(1537)	→	1538
1₂(1527)	→	1528
1₂(1372)	→	1373
1₂(1015)	→	1016
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
2₂(852)	→	853
2₂(1017)	→	1018
2₂(885)	→	886
2₂(881)	→	882

The automaton is closed under rewriting as it is compatible.