Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3989)

The rewrite relation of the following TRS is considered.

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

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

2(2(x1))	→	2(1(1(2(3(1(0(1(1(5(x1))))))))))	(31)
2(2(2(x1)))	→	5(0(2(3(4(3(1(0(3(5(x1))))))))))	(32)
4(2(2(x1)))	→	1(4(0(5(5(3(1(0(1(5(x1))))))))))	(33)
2(5(4(x1)))	→	5(0(5(3(1(4(1(0(3(0(x1))))))))))	(34)
2(5(4(x1)))	→	2(1(0(3(0(1(2(0(1(1(x1))))))))))	(35)
2(5(4(x1)))	→	2(3(1(3(4(0(1(2(0(3(x1))))))))))	(36)
2(2(2(2(x1))))	→	5(5(3(4(4(4(0(2(1(4(x1))))))))))	(37)
4(4(2(2(x1))))	→	4(2(4(1(2(3(1(0(0(2(x1))))))))))	(38)
5(4(2(2(x1))))	→	2(1(5(2(0(4(0(3(3(4(x1))))))))))	(39)
3(2(2(0(2(x1)))))	→	1(2(1(2(0(5(5(1(0(4(x1))))))))))	(40)
4(5(4(2(2(x1)))))	→	4(3(5(3(1(0(4(2(0(5(x1))))))))))	(41)
2(2(2(4(2(x1)))))	→	5(5(1(1(0(1(1(2(4(0(x1))))))))))	(42)
3(5(2(2(4(x1)))))	→	1(0(0(5(5(5(0(4(3(3(x1))))))))))	(43)
5(2(3(2(4(x1)))))	→	2(1(5(3(0(4(0(3(4(1(x1))))))))))	(44)
4(2(5(2(5(x1)))))	→	1(3(0(5(3(1(1(5(5(2(x1))))))))))	(45)
2(4(4(5(5(x1)))))	→	2(1(4(1(0(2(3(0(5(5(x1))))))))))	(46)
4(4(2(4(4(1(x1))))))	→	4(1(4(3(4(5(1(0(1(4(x1))))))))))	(47)
1(4(3(2(2(2(x1))))))	→	3(0(2(4(0(5(3(1(3(0(x1))))))))))	(48)
0(0(5(2(2(2(x1))))))	→	3(4(0(5(3(3(2(1(5(5(x1))))))))))	(49)
4(5(4(2(2(3(x1))))))	→	1(4(5(3(5(5(0(2(3(3(x1))))))))))	(50)
2(5(4(1(5(3(x1))))))	→	5(2(1(5(2(4(0(4(1(2(x1))))))))))	(51)
2(2(3(0(1(5(x1))))))	→	5(0(2(1(3(4(5(0(1(4(x1))))))))))	(52)
2(2(1(4(2(5(x1))))))	→	1(1(3(3(3(5(0(4(5(3(x1))))))))))	(53)
1(4(2(2(3(5(x1))))))	→	1(4(3(3(5(5(1(1(2(1(x1))))))))))	(54)
4(3(5(4(5(0(0(x1)))))))	→	4(0(0(2(2(5(5(1(5(5(x1))))))))))	(55)
4(4(5(4(5(2(2(x1)))))))	→	0(4(0(5(4(1(0(4(5(5(x1))))))))))	(56)
4(1(2(2(2(4(2(x1)))))))	→	2(2(3(5(1(3(1(4(4(3(x1))))))))))	(57)
0(2(2(2(0(1(5(x1)))))))	→	3(1(2(3(4(4(5(4(5(1(x1))))))))))	(58)
3(2(2(0(0(4(5(x1)))))))	→	1(2(0(0(4(3(0(3(3(4(x1))))))))))	(59)
3(2(2(2(5(4(5(x1)))))))	→	3(2(2(1(2(0(0(2(1(0(x1))))))))))	(60)

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:

1405	→	265
223	→	197
1301	→	699
1287	→	1276
733	→	724
731	→	599
917	→	332
1437	→	514
1459	→	332
128	→	503
128	→	757
128	→	920
263	→	197
263	→	662
263	→	732
750	→	1348
791	→	608
791	→	406
791	→	423
1117	→	601
1475	→	592
1475	→	1496
1142	→	608
10	→	118
273	→	17
273	→	1116
742	→	477
289	→	265
289	→	702
289	→	1124
1379	→	1148
1487	→	608
915	→	332
1284	→	1324
1284	→	1356
1284	→	1414
1284	→	1422
1284	→	1500
1391	→	128
1393	→	197
1431	→	491
1431	→	1466
96	→	1
96	→	532
96	→	545
96	→	449
96	→	608
96	→	423
641	→	631
1435	→	492
560	→	548
129	→	575
129	→	977
1140	→	608
882	→	332
882	→	380
882	→	1459
1253	→	561
701	→	6
701	→	362
701	→	524
701	→	610
1363	→	9
995	→	332
956	→	481
502	→	492
638	→	1002
18	→	1
18	→	406
18	→	617
18	→	449
18	→	608
18	→	423
18	→	619
18	→	425
18	→	1491
624	→	609
978	→	551
41	→	9
3	→	40
3	→	153
3	→	222
3	→	288
3	→	359
3	→	416
583	→	2
583	→	736
583	→	523
583	→	333
583	→	197
583	→	246
333	→	567
600	→	4
600	→	757
600	→	755
600	→	128
600	→	491
600	→	175
600	→	743
600	→	407
600	→	156
600	→	921
600	→	1391
1003	→	332
772	→	874
1289	→	1276
1011	→	332
500	→	492
225	→	197
225	→	652
225	→	723
1495	→	1230
1062	→	1269
406	→	545
406	→	623
1119	→	604
1325	→	760
919	→	332
1467	→	575
9	→	87
9	→	480
9	→	561
620	→	609
647	→	631
5	→	62
5	→	127
5	→	196
5	→	264
5	→	377
5	→	422
95	→	973
95	→	1149
95	→	1155
95	→	1211
95	→	1294
1415	→	332
515	→	601
65	→	9
997	→	332
618	→	609
175	→	128
175	→	491
175	→	755
756	→	744
1365	→	793
674	→	834
749	→	813
616	→	95
622	→	609
1164	→	1452
700	→	759
700	→	826
700	→	916
700	→	927
700	→	1290
246	→	197
246	→	2
380	→	332
968	→	491
968	→	1025
1493	→	652
1	→	85
1	→	155
1	→	224
1	→	290
1	→	403
1	→	448
542	→	533
1026	→	1014
1022	→	736
1022	→	523
1022	→	333
1022	→	2
1022	→	197
1022	→	246
645	→	631
667	→	653
332	→	450
332	→	470
1387	→	118
1323	→	760
197	→	523
197	→	666
197	→	736
884	→	118
1283	→	1350
1283	→	1384
1283	→	1406
1283	→	1460
1283	→	1480
135	→	94
970	→	491
970	→	1031
751	→	1147
488	→	414
687	→	6
687	→	470
687	→	332
687	→	380
687	→	1459
423	→	406
423	→	608
769	→	619
769	→	406
769	→	425
769	→	1491
573	→	994
735	→	724
330	→	265
330	→	640
330	→	717
330	→	1126
125	→	1004
1070	→	757
1070	→	755
1070	→	128
1070	→	405
1070	→	309
1070	→	174
1070	→	8
1070	→	243
1070	→	331
1070	→	4
1070	→	491
1070	→	175
1070	→	921
86	→	9
86	→	547
1413	→	332
1421	→	127
1005	→	332
1212	→	1292
1385	→	87
1385	→	1386
1385	→	1428
1385	→	1474
562	→	548
562	→	592
562	→	679
177	→	128
1499	→	414
1127	→	551
552	→	1118
540	→	125
844	→	676
1453	→	332
976	→	550
311	→	1490
911	→	265
779	→	1322
779	→	1362
779	→	1412
779	→	1420
779	→	1430
779	→	1498
639	→	1
639	→	623
639	→	617
639	→	406
639	→	532
639	→	449
6	→	64
6	→	176
6	→	245
6	→	311
6	→	379
6	→	424
554	→	16
404	→	332
404	→	424
404	→	311
404	→	176
404	→	64
404	→	245
404	→	379
404	→	6
404	→	380
404	→	1459
1336	→	1148
1032	→	1014
823	→	751
1351	→	771
1293	→	724
522	→	478
498	→	339
699	→	770
699	→	872
699	→	912
699	→	1012
699	→	1128
615	→	1364
665	→	653
204	→	16
873	→	87
873	→	883
873	→	955
873	→	1061
2	→	42
2	→	194
2	→	262
2	→	329
2	→	361
2	→	418
814	→	1370
686	→	1252
4	→	8
4	→	174
4	→	243
4	→	309
4	→	331
4	→	405
265	→	514
265	→	646
265	→	719
1291	→	1276
449	→	406
449	→	532
449	→	617
1150	→	332
244	→	197
244	→	664
244	→	734
582	→	1139
1069	→	1486
827	→	9
1501	→	414
419	→	406
419	→	541
478	→	996
479	→	3
479	→	719
479	→	514
479	→	265
479	→	630
479	→	291
479	→	88
479	→	1405
1451	→	523
425	→	406
425	→	619
593	→	672
754	→	744
802	→	406
802	→	617
802	→	449
802	→	974
1461	→	128
504	→	492
913	→	332
481	→	975
1224	→	652
972	→	492
1491	→	608
63	→	9
1125	→	551
1270	→	680
925	→	1436
925	→	1450
720	→	693
1497	→	680
697	→	1223
697	→	1229
663	→	653
1021	→	1484
568	→	625
758	→	744
678	→	414
417	→	406
417	→	621
126	→	6
126	→	332
126	→	404
126	→	378
1239	→	333
362	→	332
453	→	738
752	→	3
752	→	719
752	→	514
752	→	265
752	→	630
752	→	291
752	→	1405
1357	→	9
529	→	456
310	→	265
310	→	644
310	→	692
825	→	9
458	→	781
458	→	828
458	→	914
458	→	967
458	→	1286
414	→	895
414	→	897
414	→	910
1429	→	481
771	→	849
245	→	1458
17	→	792
17	→	824
17	→	918
17	→	969
17	→	1288
1349	→	1327
896	→	128
360	→	332
718	→	693
926	→	17
1148	→	608
154	→	128
154	→	499
1129	→	550
1407	→	332
703	→	693
413	→	965
413	→	1275
858	→	425
858	→	608
858	→	1491
974	→	532
928	→	407
928	→	971
928	→	1027
1469	→	575
829	→	9
340	→	95
629	→	93
1281	→	1492
1281	→	1494
378	→	332
1165	→	623
1165	→	617
1165	→	406
1165	→	448
1165	→	290
1165	→	155
1165	→	85
1165	→	224
1165	→	403
1165	→	1
1165	→	532
1165	→	449
1285	→	362
1285	→	524
1285	→	424
1285	→	311
1285	→	176
1285	→	64
1285	→	245
1285	→	379
1285	→	6
1285	→	610
1028	→	1014
574	→	414
195	→	128
195	→	501
195	→	753
546	→	533
43	→	9
43	→	559
1218	→	487
1481	→	550
660	→	1010
822	→	1326
403	→	1390
403	→	1392
403	→	1404
1423	→	407
1423	→	1434
1423	→	1468
966	→	491
737	→	724
1485	→	608
599	→	1141
312	→	265
312	→	416
312	→	288
312	→	153
312	→	40
312	→	222
312	→	359
312	→	3
312	→	630
312	→	291
312	→	1405
780	→	6
780	→	701
780	→	1285
415	→	6
415	→	470
415	→	332
415	→	380
415	→	378
415	→	693
415	→	720
415	→	360
415	→	1459
661	→	2
661	→	736
661	→	523
661	→	333
661	→	197
661	→	246
607	→	124
156	→	128
156	→	743
291	→	265
291	→	630
459	→	5
459	→	87
459	→	561
459	→	65
459	→	533
459	→	546
459	→	547
459	→	86
898	→	197
0₁(406)	→	407
0₁(123)	→	124
0₁(680)	→	681
0₁(521)	→	522
0₁(1020)	→	1021
0₁(965)	→	966
0₁(527)	→	528
0₁(483)	→	484
0₁(741)	→	742
0₁(520)	→	521
0₁(265)	→	266
0₁(538)	→	539
0₁(88)	→	89
0₁(895)	→	896
0₁(480)	→	481
0₁(1422)	→	1423
0₁(602)	→	603
0₁(927)	→	928
0₁(597)	→	598
0₁(920)	→	921
0₁(155)	→	156
0₁(452)	→	453
0₁(1294)	→	1295
0₁(153)	→	154
0₁(684)	→	685
0₁(745)	→	746
0₁(1430)	→	1431
0₁(740)	→	741
0₁(407)	→	408
0₁(174)	→	175
0₁(198)	→	199
0₁(127)	→	128
0₁(129)	→	130
0₁(1012)	→	1013
0₁(955)	→	956
0₁(610)	→	611
0₁(118)	→	119
0₁(525)	→	526
0₁(1298)	→	1299
0₁(581)	→	582
0₁(203)	→	204
0₁(94)	→	95
0₁(470)	→	471
0₁(495)	→	496
0₁(677)	→	678
0₁(632)	→	633
0₁(1158)	→	1159
0₁(551)	→	552
0₁(176)	→	177
0₁(548)	→	549
0₁(686)	→	687
0₁(1390)	→	1391
0₁(474)	→	475
0₁(11)	→	12
0₁(1428)	→	1429
0₁(578)	→	579
0₁(1297)	→	1298
0₁(268)	→	269
0₁(746)	→	747
0₁(194)	→	195
0₁(967)	→	968
0₁(334)	→	335
0₁(676)	→	677
0₁(201)	→	202
0₁(454)	→	455
0₁(969)	→	970
0₁(1017)	→	1018
0₁(567)	→	568
0₁(516)	→	517
0₁(1460)	→	1461
0₁(1067)	→	1068
2₂(776)	→	777
2₂(798)	→	799
2₂(787)	→	788
2₂(1335)	→	1336
2₂(1332)	→	1333
2₂(1376)	→	1377
2₂(840)	→	841
2₂(1230)	→	1231
2₂(765)	→	766
2₂(801)	→	802
2₂(819)	→	820
2₂(768)	→	769
2₂(779)	→	780
2₂(855)	→	856
2₂(843)	→	844
2₂(790)	→	791
2₂(822)	→	823
1₂(761)	→	762
1₂(772)	→	773
1₂(1238)	→	1239
1₂(763)	→	764
1₂(774)	→	775
1₂(785)	→	786
1₂(1334)	→	1335
1₂(815)	→	816
1₂(782)	→	783
1₂(1328)	→	1329
1₂(799)	→	800
1₂(875)	→	876
1₂(778)	→	779
1₂(788)	→	789
1₂(777)	→	778
1₂(783)	→	784
1₂(796)	→	797
1₂(835)	→	836
1₂(841)	→	842
1₂(821)	→	822
1₂(767)	→	768
1₂(1327)	→	1328
1₂(789)	→	790
1₂(1333)	→	1334
1₂(814)	→	815
1₂(1372)	→	1373
1₂(836)	→	837
1₂(817)	→	818
1₂(771)	→	772
1₂(1229)	→	1230
1₂(1330)	→	1331
1₂(794)	→	795
1₂(842)	→	843
1₂(1232)	→	1233
1₂(820)	→	821
1₂(766)	→	767
1₂(793)	→	794
1₂(760)	→	761
1₂(1494)	→	1495
1₂(1231)	→	1232
1₂(881)	→	882
1₂(800)	→	801
1₂(851)	→	852
1₂(838)	→	839
4₂(880)	→	881
4₂(1374)	→	1375
4₂(1237)	→	1238
4₂(853)	→	854
5₁(134)	→	135
5₁(40)	→	41
5₁(644)	→	645
5₁(517)	→	518
5₁(1016)	→	1017
5₁(1384)	→	1385
5₁(1118)	→	1119
5₁(569)	→	570
5₁(559)	→	560
5₁(541)	→	542
5₁(734)	→	735
5₁(1474)	→	1475
5₁(547)	→	548
5₁(1356)	→	1357
5₁(828)	→	829
5₁(533)	→	534
5₁(1292)	→	1293
5₁(603)	→	604
5₁(1061)	→	1062
5₁(1215)	→	1216
5₁(633)	→	634
5₁(625)	→	626
5₁(613)	→	614
5₁(62)	→	63
5₁(606)	→	607
5₁(826)	→	827
5₁(121)	→	122
5₁(472)	→	473
5₁(604)	→	605
5₁(673)	→	674
5₁(672)	→	673
5₁(697)	→	698
5₁(545)	→	546
5₁(646)	→	647
5₁(8)	→	9
5₁(1156)	→	1157
5₁(519)	→	520
5₁(1362)	→	1363
5₁(85)	→	86
5₁(630)	→	631
5₁(872)	→	873
5₁(456)	→	457
5₁(1252)	→	1253
5₁(473)	→	474
5₁(732)	→	733
5₁(736)	→	737
5₁(339)	→	340
5₁(655)	→	656
5₁(95)	→	96
5₁(596)	→	597
5₁(518)	→	519
5₁(577)	→	578
5₁(640)	→	641
5₁(1281)	→	1282
5₁(64)	→	65
5₁(122)	→	123
5₁(537)	→	538
5₁(723)	→	724
5₁(824)	→	825
5₁(532)	→	533
5₁(683)	→	684
5₁(486)	→	487
5₁(656)	→	657
5₁(725)	→	726
5₁(1159)	→	1160
5₁(42)	→	43
5₁(1066)	→	1067
5₁(1216)	→	1217
5₁(561)	→	562
5₀(3)	→	5
5₀(6)	→	5
5₀(5)	→	5
5₀(4)	→	5
5₀(2)	→	5
5₀(1)	→	5
4₀(2)	→	6
4₀(6)	→	6
4₀(4)	→	6
4₀(1)	→	6
4₀(3)	→	6
4₀(5)	→	6
0₂(850)	→	851
0₂(816)	→	817
0₂(773)	→	774
0₂(874)	→	875
0₂(1377)	→	1378
0₂(1371)	→	1372
0₂(762)	→	763
0₂(856)	→	857
0₂(837)	→	838
0₂(784)	→	785
0₂(1329)	→	1330
0₂(795)	→	796
0₂(879)	→	880
0₀(1)	→	4
0₀(6)	→	4
0₀(3)	→	4
0₀(5)	→	4
0₀(2)	→	4
0₀(4)	→	4
3₁(87)	→	88
3₁(1288)	→	1289
3₁(524)	→	525
3₁(1013)	→	1014
3₁(599)	→	600
3₁(636)	→	637
3₁(695)	→	696
3₁(1064)	→	1065
3₁(1279)	→	1280
3₁(1286)	→	1287
3₁(120)	→	121
3₁(1155)	→	1156
3₁(582)	→	583
3₁(1065)	→	1066
3₁(634)	→	635
3₁(1128)	→	1129
3₁(1282)	→	1283
3₁(594)	→	595
3₁(728)	→	729
3₁(1162)	→	1163
3₁(1069)	→	1070
3₁(202)	→	203
3₁(128)	→	129
3₁(657)	→	658
3₁(1404)	→	1405
3₁(539)	→	540
3₁(975)	→	976
3₁(536)	→	537
3₁(90)	→	91
3₁(270)	→	271
3₁(13)	→	14
3₁(738)	→	739
3₁(1275)	→	1276
3₁(1116)	→	1117
3₁(576)	→	577
3₁(571)	→	572
3₁(1466)	→	1467
3₁(288)	→	289
3₁(487)	→	488
3₁(92)	→	93
3₁(658)	→	659
3₁(451)	→	452
3₁(1436)	→	1437
3₁(450)	→	451
3₁(290)	→	291
3₁(1217)	→	1218
3₁(595)	→	596
3₁(1160)	→	1161
3₁(922)	→	923
3₁(1290)	→	1291
3₁(1025)	→	1026
3₁(1027)	→	1028
3₁(338)	→	339
3₁(133)	→	134
3₁(329)	→	330
3₁(605)	→	606
3₁(528)	→	529
3₁(311)	→	312
3₁(910)	→	911
3₁(1161)	→	1162
3₁(1031)	→	1032
3₁(514)	→	515
3₁(1015)	→	1016
3₁(627)	→	628
3₁(698)	→	699
3₁(1498)	→	1499
3₁(549)	→	550
3₁(1021)	→	1022
3₁(1500)	→	1501
3₁(409)	→	410
3₁(485)	→	486
3₁(1468)	→	1469
3₁(751)	→	752
3₁(264)	→	265
3₁(635)	→	636
3₁(1480)	→	1481
3₁(272)	→	273
3₁(309)	→	310
2₁(601)	→	602
2₁(674)	→	675
2₁(1283)	→	1284
2₁(333)	→	334
2₁(418)	→	419
2₁(750)	→	751
2₁(93)	→	94
2₁(923)	→	924
2₁(410)	→	411
2₁(1212)	→	1213
2₁(266)	→	267
2₁(1126)	→	1127
2₁(1141)	→	1142
2₁(615)	→	616
2₁(593)	→	594
2₁(744)	→	745
2₁(448)	→	449
2₁(477)	→	478
2₁(550)	→	551
2₁(413)	→	414
2₁(1299)	→	1300
2₁(699)	→	700
2₁(475)	→	476
2₁(481)	→	482
2₁(1490)	→	1491
2₁(749)	→	750
2₁(1484)	→	1485
2₁(1486)	→	1487
2₁(199)	→	200
2₁(580)	→	581
2₁(1284)	→	1285
2₁(1139)	→	1140
2₁(1420)	→	1421
2₁(14)	→	15
2₁(1147)	→	1148
2₁(492)	→	493
2₁(416)	→	417
2₁(664)	→	665
2₁(422)	→	423
2₁(612)	→	613
2₁(1124)	→	1125
2₁(666)	→	667
2₁(729)	→	730
2₁(700)	→	701
2₁(1296)	→	1297
2₁(977)	→	978
2₁(662)	→	663
2₁(1063)	→	1064
2₁(424)	→	425
2₁(455)	→	456
2₁(652)	→	653
2₁(17)	→	18
2₁(747)	→	748
2₁(675)	→	676
2₁(973)	→	974
2₁(1019)	→	1020
2₁(405)	→	406
2₁(458)	→	459
1₀(3)	→	2
1₀(5)	→	2
1₀(2)	→	2
1₀(4)	→	2
1₀(1)	→	2
1₀(6)	→	2
3₀(2)	→	3
3₀(4)	→	3
3₀(3)	→	3
3₀(6)	→	3
3₀(1)	→	3
3₀(5)	→	3
4₁(916)	→	917
4₁(414)	→	415
4₁(918)	→	919
4₁(131)	→	132
4₁(912)	→	913
4₁(523)	→	524
4₁(1018)	→	1019
4₁(1276)	→	1277
4₁(692)	→	693
4₁(526)	→	527
4₁(331)	→	332
4₁(726)	→	727
4₁(1010)	→	1011
4₁(1157)	→	1158
4₁(1277)	→	1278
4₁(501)	→	502
4₁(1002)	→	1003
4₁(1004)	→	1005
4₁(335)	→	336
4₁(491)	→	492
4₁(1434)	→	1435
4₁(377)	→	378
4₁(719)	→	720
4₁(971)	→	972
4₁(336)	→	337
4₁(1496)	→	1497
4₁(361)	→	362
4₁(499)	→	500
4₁(403)	→	404
4₁(682)	→	683
4₁(359)	→	360
4₁(124)	→	125
4₁(659)	→	660
4₁(611)	→	612
4₁(482)	→	483
4₁(631)	→	632
4₁(1269)	→	1270
4₁(626)	→	627
4₁(337)	→	338
4₁(453)	→	454
4₁(269)	→	270
4₁(1149)	→	1150
4₁(1452)	→	1453
4₁(570)	→	571
4₁(702)	→	703
4₁(1068)	→	1069
4₁(609)	→	610
4₁(1412)	→	1413
4₁(925)	→	926
4₁(727)	→	728
4₁(515)	→	516
4₁(91)	→	92
4₁(994)	→	995
4₁(914)	→	915
4₁(1406)	→	1407
4₁(598)	→	599
4₁(553)	→	554
4₁(724)	→	725
4₁(996)	→	997
4₁(685)	→	686
4₁(1458)	→	1459
4₁(679)	→	680
4₁(1414)	→	1415
4₁(572)	→	573
4₁(693)	→	694
4₁(739)	→	740
4₁(379)	→	380
4₁(717)	→	718
4₁(412)	→	413
4₁(503)	→	504
4₁(579)	→	580
1₁(267)	→	268
1₁(1492)	→	1493
1₁(1295)	→	1296
1₁(592)	→	593
1₁(1214)	→	1215
1₁(484)	→	485
1₁(271)	→	272
1₁(573)	→	574
1₁(478)	→	479
1₁(653)	→	654
1₁(1014)	→	1015
1₁(1300)	→	1301
1₁(16)	→	17
1₁(696)	→	697
1₁(408)	→	409
1₁(535)	→	536
1₁(497)	→	498
1₁(1280)	→	1281
1₁(89)	→	90
1₁(411)	→	412
1₁(332)	→	333
1₁(1278)	→	1279
1₁(743)	→	744
1₁(1223)	→	1224
1₁(494)	→	495
1₁(12)	→	13
1₁(638)	→	639
1₁(921)	→	922
1₁(753)	→	754
1₁(222)	→	223
1₁(748)	→	749
1₁(730)	→	731
1₁(623)	→	624
1₁(608)	→	609
1₁(196)	→	197
1₁(471)	→	472
1₁(476)	→	477
1₁(1392)	→	1393
1₁(1164)	→	1165
1₁(575)	→	576
1₁(694)	→	695
1₁(924)	→	925
1₁(1213)	→	1214
1₁(1450)	→	1451
1₁(614)	→	615
1₁(755)	→	756
1₁(125)	→	126
1₁(243)	→	244
1₁(10)	→	11
1₁(224)	→	225
1₁(493)	→	494
1₁(262)	→	263
1₁(757)	→	758
1₁(897)	→	898
1₁(132)	→	133
1₁(457)	→	458
1₁(130)	→	131
1₁(681)	→	682
1₁(883)	→	884
1₁(1211)	→	1212
1₁(1062)	→	1063
1₁(15)	→	16
1₁(637)	→	638
1₁(660)	→	661
1₁(619)	→	620
1₁(197)	→	198
1₁(628)	→	629
1₁(1163)	→	1164
1₁(621)	→	622
1₁(496)	→	497
1₁(200)	→	201
1₁(654)	→	655
1₁(245)	→	246
1₁(617)	→	618
1₁(568)	→	569
1₁(1386)	→	1387
1₁(534)	→	535
1₁(552)	→	553
1₁(9)	→	10
1₁(119)	→	120
5₂(1378)	→	1379
5₂(1326)	→	1327
5₂(1234)	→	1235
5₂(781)	→	782
5₂(1324)	→	1325
5₂(1348)	→	1349
5₂(813)	→	814
5₂(878)	→	879
5₂(1233)	→	1234
5₂(770)	→	771
5₂(877)	→	878
5₂(1322)	→	1323
5₂(759)	→	760
5₂(857)	→	858
5₂(1350)	→	1351
5₂(1364)	→	1365
5₂(834)	→	835
5₂(792)	→	793
2₀(1)	→	1
2₀(6)	→	1
2₀(5)	→	1
2₀(2)	→	1
2₀(3)	→	1
2₀(4)	→	1
3₂(852)	→	853
3₂(764)	→	765
3₂(1235)	→	1236
3₂(775)	→	776
3₂(849)	→	850
3₂(786)	→	787
3₂(797)	→	798
3₂(839)	→	840
3₂(876)	→	877
3₂(818)	→	819
3₂(1236)	→	1237
3₂(1373)	→	1374
3₂(854)	→	855
3₂(1331)	→	1332
3₂(1370)	→	1371
3₂(1375)	→	1376

The automaton is closed under rewriting as it is compatible.