Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/213147)

The rewrite relation of the following TRS is considered.

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

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:

503	→	315
272	→	3
272	→	311
272	→	130
272	→	426
272	→	26
272	→	374
272	→	406
272	→	28
272	→	380
1405	→	25
1067	→	9
854	→	822
1198	→	861
1206	→	169
1197	→	1356
339	→	317
1268	→	1378
1268	→	1384
1268	→	1386
1268	→	1392
1268	→	1406
1268	→	1502
322	→	194
376	→	11
280	→	554
280	→	618
280	→	969
280	→	1000
280	→	1123
280	→	1346
591	→	555
25	→	809
25	→	861
25	→	1017
25	→	1034
494	→	9
1287	→	384
958	→	950
457	→	302
457	→	594
534	→	143
964	→	950
685	→	383
685	→	323
685	→	1
685	→	226
685	→	257
685	→	585
1394	→	1426
1394	→	1435
1394	→	1441
1394	→	1449
1394	→	1463
128	→	510
128	→	568
128	→	825
128	→	917
128	→	949
202	→	54
202	→	801
589	→	555
81	→	52
81	→	395
791	→	459
152	→	143
152	→	377
152	→	463
152	→	458
152	→	204
152	→	334
152	→	142
152	→	65
152	→	27
152	→	121
152	→	256
152	→	6
152	→	373
152	→	163
152	→	161
152	→	520
152	→	528
152	→	1035
152	→	920
152	→	932
152	→	940
152	→	1413
98	→	140
98	→	381
214	→	11
214	→	469
229	→	491
229	→	699
229	→	711
229	→	1042
10	→	504
1379	→	151
915	→	1084
915	→	1119
915	→	1180
915	→	1199
915	→	1201
1393	→	906
640	→	98
303	→	6
303	→	465
303	→	169
303	→	377
303	→	143
303	→	463
303	→	152
303	→	154
303	→	524
303	→	530
303	→	1034
303	→	861
303	→	1048
303	→	25
303	→	1018
303	→	942
303	→	1051
1073	→	52
129	→	95
530	→	143
655	→	316
84	→	12
956	→	950
511	→	143
1273	→	25
436	→	493
436	→	497
436	→	506
436	→	543
436	→	649
436	→	673
436	→	675
436	→	899
436	→	905
119	→	519
119	→	574
119	→	831
119	→	919
119	→	955
595	→	311
595	→	130
595	→	426
595	→	3
595	→	26
1249	→	915
145	→	178
122	→	95
122	→	200
466	→	459
466	→	537
585	→	555
676	→	335
1230	→	998
365	→	335
1395	→	98
226	→	332
226	→	383
226	→	347
226	→	151
226	→	63
226	→	25
226	→	94
226	→	225
226	→	1
226	→	232
226	→	323
226	→	257
226	→	722
226	→	555
226	→	589
226	→	585
226	→	950
226	→	964
226	→	962
226	→	951
226	→	960
39	→	9
39	→	418
39	→	666
120	→	95
3	→	36
3	→	71
3	→	128
3	→	167
3	→	258
3	→	364
583	→	555
1079	→	9
1483	→	213
50	→	9
50	→	424
988	→	259
988	→	569
333	→	324
1003	→	680
218	→	1
218	→	383
218	→	323
218	→	226
218	→	257
218	→	585
218	→	12
218	→	1049
382	→	1
382	→	257
382	→	460
382	→	1024
1033	→	1022
1102	→	864
213	→	308
213	→	454
213	→	467
617	→	271
460	→	535
1114	→	98
405	→	271
1495	→	54
146	→	11
861	→	1354
861	→	1360
861	→	1404
861	→	1412
108	→	95
411	→	4
411	→	361
411	→	348
411	→	536
9	→	90
9	→	130
9	→	191
9	→	426
5	→	8
5	→	51
5	→	119
5	→	162
5	→	244
5	→	360
1200	→	1195
37	→	9
95	→	203
95	→	1
95	→	383
95	→	226
95	→	677
95	→	460
95	→	108
95	→	822
95	→	848
95	→	5
110	→	95
1124	→	950
1124	→	589
1124	→	383
1124	→	323
1124	→	585
1124	→	1034
1124	→	861
1124	→	959
1124	→	839
1124	→	523
1124	→	225
1124	→	94
1124	→	25
1124	→	63
1124	→	151
1124	→	347
1124	→	1
1124	→	226
1027	→	152
1027	→	524
1027	→	1034
1027	→	861
1027	→	1048
1027	→	25
1027	→	1018
361	→	335
55	→	12
55	→	1482
381	→	521
381	→	576
381	→	833
381	→	921
381	→	957
243	→	226
674	→	323
193	→	92
193	→	194
99	→	1
99	→	383
99	→	226
99	→	259
99	→	245
99	→	323
99	→	257
99	→	315
99	→	569
99	→	461
99	→	227
99	→	575
99	→	583
99	→	585
99	→	956
99	→	556
99	→	960
99	→	667
99	→	316
99	→	13
293	→	6
293	→	465
293	→	169
293	→	143
293	→	161
293	→	154
293	→	377
293	→	463
293	→	152
293	→	528
293	→	530
293	→	524
293	→	912
293	→	940
293	→	942
293	→	1034
293	→	861
293	→	1048
293	→	25
293	→	1018
107	→	527
107	→	588
107	→	847
107	→	939
107	→	963
942	→	912
700	→	25
700	→	784
380	→	374
968	→	950
1493	→	54
1	→	25
1	→	63
1	→	94
1	→	151
1	→	225
1	→	347
1077	→	52
826	→	822
826	→	1097
1308	→	1022
1026	→	1066
1026	→	1074
1026	→	1272
1026	→	1309
922	→	912
840	→	822
305	→	92
305	→	438
1489	→	912
13	→	1
13	→	383
13	→	226
13	→	259
13	→	315
13	→	245
13	→	323
13	→	257
13	→	227
13	→	316
13	→	722
13	→	555
13	→	589
13	→	569
13	→	667
13	→	461
13	→	575
13	→	583
13	→	585
13	→	556
13	→	950
13	→	964
13	→	956
13	→	960
13	→	962
13	→	12
13	→	1049
13	→	987
13	→	864
13	→	1102
940	→	912
524	→	143
1387	→	143
490	→	52
392	→	388
1426	→	1488
1426	→	1492
505	→	54
390	→	270
1345	→	1051
1345	→	1022
723	→	384
1376	→	1420
1376	→	1428
1376	→	1437
1376	→	1443
1376	→	1465
1376	→	1496
1208	→	12
402	→	477
970	→	950
488	→	52
179	→	54
179	→	684
842	→	822
842	→	1101
842	→	1246
26	→	9
26	→	311
26	→	3
26	→	862
536	→	12
1232	→	8
816	→	498
920	→	912
1503	→	1497
1413	→	1022
309	→	456
1421	→	151
91	→	321
1099	→	1115
783	→	458
170	→	82
170	→	215
170	→	279
385	→	815
385	→	995
1385	→	900
161	→	143
916	→	232
916	→	585
916	→	12
916	→	1049
268	→	3
268	→	311
268	→	130
268	→	426
268	→	26
177	→	83
72	→	52
619	→	169
619	→	1376
702	→	25
702	→	790
141	→	98
441	→	5
441	→	347
441	→	151
441	→	63
441	→	1
441	→	95
441	→	108
441	→	294
441	→	216
441	→	110
441	→	822
441	→	848
441	→	850
441	→	914
532	→	143
407	→	671
983	→	1194
983	→	1203
983	→	1205
983	→	1231
983	→	1418
526	→	143
824	→	681
257	→	226
257	→	323
389	→	782
389	→	1032
918	→	912
918	→	1248
1310	→	1022
121	→	525
121	→	584
121	→	841
121	→	933
121	→	961
810	→	52
1477	→	294
1477	→	216
1477	→	914
6	→	27
6	→	65
6	→	121
6	→	142
6	→	256
6	→	334
1075	→	52
468	→	302
1051	→	458
577	→	555
109	→	529
109	→	590
109	→	849
109	→	941
109	→	965
1456	→	912
823	→	997
823	→	1013
1438	→	143
52	→	289
52	→	397
455	→	439
555	→	722
1092	→	1207
394	→	388
1450	→	906
386	→	228
522	→	143
1279	→	714
230	→	3
230	→	426
230	→	130
230	→	311
230	→	9
230	→	26
1377	→	94
1377	→	1394
292	→	489
292	→	701
292	→	720
292	→	1044
1181	→	912
1355	→	9
538	→	12
350	→	335
204	→	201
437	→	4
437	→	432
437	→	170
437	→	401
437	→	335
437	→	982
437	→	913
143	→	169
143	→	379
143	→	465
717	→	460
717	→	1049
717	→	1024
569	→	555
951	→	12
951	→	589
951	→	383
951	→	323
951	→	585
951	→	1034
951	→	861
951	→	959
951	→	839
951	→	523
951	→	225
951	→	94
951	→	25
951	→	63
951	→	151
951	→	347
951	→	1
951	→	226
951	→	1049
53	→	264
53	→	304
53	→	314
873	→	863
301	→	383
301	→	226
301	→	259
301	→	569
999	→	909
808	→	52
2	→	49
2	→	80
2	→	107
2	→	160
2	→	231
2	→	358
313	→	11
863	→	1002
11	→	82
954	→	9
954	→	3
954	→	311
954	→	26
954	→	862
954	→	1223
1347	→	912
4	→	38
4	→	73
4	→	109
4	→	153
4	→	242
4	→	349
528	→	143
265	→	269
28	→	9
28	→	406
232	→	226
1018	→	25
1018	→	1048
470	→	302
1501	→	502
557	→	807
850	→	822
419	→	407
419	→	639
520	→	143
478	→	225
904	→	232
904	→	585
904	→	569
904	→	259
904	→	12
904	→	1049
1035	→	1022
1001	→	822
369	→	309
369	→	616
425	→	407
593	→	555
802	→	12
281	→	229
281	→	962
281	→	460
281	→	257
66	→	52
66	→	387
318	→	1
318	→	383
318	→	226
318	→	259
318	→	569
318	→	667
359	→	335
1043	→	1022
913	→	982
913	→	1341
862	→	1019
862	→	9
862	→	3
862	→	311
862	→	26
862	→	1229
862	→	1355
1224	→	998
1045	→	1022
1094	→	956
1094	→	245
1094	→	556
1094	→	227
1094	→	575
1094	→	583
1094	→	461
1094	→	960
1094	→	667
1094	→	316
1094	→	315
1094	→	259
1094	→	569
1094	→	13
93	→	54
1491	→	912
348	→	335
348	→	226
348	→	245
348	→	323
348	→	257
348	→	461
348	→	227
348	→	575
348	→	583
348	→	585
348	→	956
348	→	556
348	→	960
348	→	667
348	→	316
348	→	315
348	→	259
348	→	569
348	→	13
1436	→	900
1458	→	54
834	→	822
672	→	97
335	→	401
335	→	432
1378	→	1455
1378	→	1457
1091	→	1240
1247	→	680
1020	→	713
295	→	292
1202	→	12
1202	→	1286
217	→	531
217	→	592
217	→	853
217	→	947
217	→	967
1085	→	8
290	→	724
1049	→	12
934	→	912
934	→	1278
417	→	408
724	→	1021
724	→	1050
1204	→	12
1204	→	1284
960	→	950
1420	→	1490
1420	→	1494
962	→	950
64	→	52
64	→	391
1442	→	143
216	→	294
1122	→	151
1122	→	1268
453	→	5
1357	→	52
1100	→	556
1100	→	227
1100	→	585
1100	→	257
1100	→	583
1100	→	461
1100	→	960
310	→	12
948	→	912
278	→	271
990	→	524
990	→	161
990	→	373
990	→	458
990	→	377
990	→	6
990	→	463
990	→	204
990	→	163
990	→	152
990	→	1035
990	→	1018
990	→	932
952	→	1072
908	→	1474
83	→	475
1429	→	900
245	→	226
1116	→	865
683	→	226
683	→	569
683	→	259
683	→	461
683	→	227
683	→	583
683	→	556
683	→	13
683	→	1025
712	→	872
154	→	143
168	→	143
1361	→	52
398	→	388
1464	→	212
462	→	292
1407	→	212
567	→	555
464	→	459
832	→	822
492	→	52
1419	→	912
865	→	897
866	→	461
866	→	227
866	→	257
866	→	583
866	→	556
866	→	960
866	→	956
866	→	667
866	→	316
866	→	315
866	→	575
866	→	259
866	→	245
866	→	569
866	→	13
1093	→	1113
132	→	97
132	→	300
131	→	366
74	→	52
74	→	393
1271	→	25
259	→	226
670	→	383
670	→	226
670	→	259
670	→	569
848	→	822
378	→	374
1120	→	143
953	→	1060
953	→	1076
953	→	1270
953	→	1307
932	→	912
932	→	1405
1285	→	384
1444	→	906
452	→	533
452	→	566
452	→	347
452	→	151
452	→	63
452	→	1
452	→	95
452	→	360
452	→	162
452	→	51
452	→	8
452	→	119
452	→	244
452	→	5
452	→	108
452	→	821
452	→	911
452	→	822
452	→	848
575	→	555
195	→	97
1016	→	903
910	→	903
367	→	97
558	→	25
144	→	176
144	→	212
1065	→	950
1065	→	585
1065	→	323
1065	→	332
1065	→	589
1065	→	1034
1065	→	861
1065	→	959
1065	→	839
1065	→	523
1065	→	225
1065	→	94
1065	→	25
1065	→	63
1065	→	151
1065	→	347
1065	→	1
1065	→	226
1065	→	964
266	→	277
372	→	54
1241	→	11
1269	→	94
507	→	143
476	→	469
785	→	459
396	→	388
544	→	200
966	→	950
725	→	270
427	→	407
427	→	660
163	→	143
163	→	373
163	→	458
984	→	953
721	→	712
864	→	987
599	→	311
599	→	130
599	→	426
599	→	3
599	→	26
996	→	650
312	→	416
94	→	523
94	→	582
94	→	839
94	→	931
94	→	959
192	→	368
192	→	370
192	→	596
1061	→	1078
1061	→	1090
1061	→	1121
661	→	11
327	→	12
228	→	487
1466	→	212
408	→	450
1427	→	151
898	→	865
1₁(71)	→	72
1₁(406)	→	407
1₁(1268)	→	1269
1₁(424)	→	425
1₁(51)	→	52
1₁(323)	→	324
1₁(487)	→	488
1₁(82)	→	83
1₁(438)	→	439
1₁(10)	→	11
1₁(1074)	→	1075
1₁(370)	→	371
1₁(1356)	→	1357
1₁(1072)	→	1073
1₁(324)	→	325
1₁(385)	→	386
1₁(73)	→	74
1₁(143)	→	144
1₁(807)	→	808
1₁(401)	→	402
1₁(407)	→	408
1₁(304)	→	305
1₁(397)	→	398
1₁(801)	→	802
1₁(63)	→	64
1₁(212)	→	213
1₁(1076)	→	1077
1₁(1376)	→	1377
1₁(332)	→	333
1₁(65)	→	66
1₁(1062)	→	1063
1₁(80)	→	81
1₁(1360)	→	1361
1₁(809)	→	810
1₁(311)	→	312
1₁(426)	→	427
1₁(418)	→	419
1₁(387)	→	388
1₁(391)	→	392
1₁(402)	→	403
1₁(1482)	→	1483
1₁(395)	→	396
1₁(321)	→	322
1₁(436)	→	437
1₁(337)	→	338
1₁(416)	→	417
1₁(201)	→	202
1₁(454)	→	455
1₁(1394)	→	1395
1₁(489)	→	490
1₁(83)	→	84
1₁(491)	→	492
1₁(393)	→	394
2₂(650)	→	651
2₂(952)	→	953
2₂(1197)	→	1198
2₂(711)	→	712
2₂(953)	→	954
2₂(1026)	→	1027
2₂(861)	→	862
2₂(720)	→	721
2₂(677)	→	678
2₂(998)	→	999
2₂(815)	→	816
2₂(1499)	→	1500
2₂(822)	→	823
2₂(497)	→	498
0₂(1502)	→	1503
0₂(1025)	→	1026
0₂(652)	→	653
0₂(961)	→	962
0₂(897)	→	898
0₂(502)	→	503
0₂(681)	→	682
0₂(909)	→	910
0₂(1248)	→	1249
0₂(914)	→	915
0₂(1098)	→	1099
0₂(965)	→	966
0₂(1195)	→	1196
0₂(1115)	→	1116
0₂(955)	→	956
0₂(903)	→	904
0₂(1024)	→	1025
0₂(1014)	→	1015
0₂(864)	→	865
0₂(1097)	→	1098
0₂(988)	→	989
0₂(680)	→	681
0₂(1023)	→	1024
0₂(957)	→	958
0₂(950)	→	951
0₂(959)	→	960
0₂(1194)	→	1195
0₂(963)	→	964
0₂(967)	→	968
0₂(1199)	→	1200
0₂(654)	→	655
0₂(863)	→	864
0₂(715)	→	716
0₂(1101)	→	1102
0₂(982)	→	983
0₂(949)	→	950
0₂(1496)	→	1497
0₂(969)	→	970
4₂(1196)	→	1197
4₂(849)	→	850
4₂(915)	→	916
4₂(825)	→	826
4₂(908)	→	909
4₂(823)	→	824
4₂(872)	→	873
4₂(951)	→	952
4₂(678)	→	679
4₂(839)	→	840
4₂(899)	→	900
4₂(831)	→	832
4₂(847)	→	848
4₂(841)	→	842
4₂(821)	→	822
4₂(833)	→	834
4₂(1384)	→	1385
4₂(679)	→	680
4₂(1002)	→	1003
4₂(1246)	→	1247
4₂(862)	→	863
4₂(1475)	→	1476
4₂(1000)	→	1001
4₂(1428)	→	1429
4₂(716)	→	717
4₂(1435)	→	1436
4₂(1342)	→	1343
4₂(983)	→	984
4₂(1015)	→	1016
4₂(853)	→	854
4₂(913)	→	914
2₁(373)	→	374
2₁(1465)	→	1466
2₁(377)	→	378
2₁(660)	→	661
2₁(1354)	→	1355
2₁(292)	→	293
2₁(90)	→	91
2₁(229)	→	230
2₁(389)	→	390
2₁(38)	→	39
2₁(1463)	→	1464
2₁(1060)	→	1061
2₁(557)	→	558
2₁(312)	→	313
2₁(8)	→	9
2₁(228)	→	229
2₁(52)	→	53
2₁(49)	→	50
2₁(435)	→	436
2₁(36)	→	37
2₁(325)	→	326
2₁(403)	→	404
2₁(25)	→	26
2₁(95)	→	96
2₁(338)	→	339
2₁(53)	→	54
2₁(724)	→	725
2₁(1078)	→	1079
2₁(1406)	→	1407
2₁(27)	→	28
2₁(493)	→	494
2₁(1066)	→	1067
2₁(379)	→	380
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
1₂(906)	→	907
1₂(501)	→	502
1₂(901)	→	902
1₂(1229)	→	1230
1₂(997)	→	998
1₂(500)	→	501
1₂(995)	→	996
1₂(651)	→	652
1₂(1498)	→	1499
1₂(907)	→	908
1₂(1223)	→	1224
1₂(499)	→	500
1₂(1497)	→	1498
1₂(649)	→	650
1₂(1474)	→	1475
1₂(1341)	→	1342
3₀(1)	→	4
3₀(6)	→	4
3₀(3)	→	4
3₀(5)	→	4
3₀(2)	→	4
3₀(4)	→	4
5₁(699)	→	700
5₁(404)	→	405
5₁(1050)	→	1051
5₁(506)	→	507
5₁(191)	→	192
5₁(529)	→	530
5₁(160)	→	161
5₁(142)	→	143
5₁(533)	→	534
5₁(598)	→	599
5₁(192)	→	193
5₁(151)	→	152
5₁(203)	→	204
5₁(153)	→	154
5₁(1494)	→	1495
5₁(1205)	→	1206
5₁(669)	→	670
5₁(465)	→	466
5₁(510)	→	511
5₁(523)	→	524
5₁(1404)	→	1405
5₁(458)	→	459
5₁(782)	→	783
5₁(162)	→	163
5₁(1017)	→	1018
5₁(167)	→	168
5₁(527)	→	528
5₁(1270)	→	1271
5₁(1121)	→	1122
5₁(790)	→	791
5₁(1386)	→	1387
5₁(1437)	→	1438
5₁(463)	→	464
5₁(271)	→	272
5₁(618)	→	619
5₁(521)	→	522
5₁(701)	→	702
5₁(302)	→	303
5₁(1492)	→	1493
5₁(784)	→	785
5₁(326)	→	327
5₁(519)	→	520
5₁(1441)	→	1442
5₁(1119)	→	1120
5₁(531)	→	532
5₁(291)	→	292
5₁(1457)	→	1458
5₁(434)	→	435
5₁(264)	→	265
5₁(1272)	→	1273
5₁(525)	→	526
5₁(317)	→	318
5₁(200)	→	201
3₁(176)	→	177
3₁(384)	→	385
3₁(1093)	→	1094
3₁(671)	→	672
3₁(410)	→	411
3₁(432)	→	433
3₁(349)	→	350
3₁(98)	→	99
3₁(169)	→	170
3₁(54)	→	55
3₁(388)	→	389
3₁(91)	→	92
3₁(277)	→	278
3₁(360)	→	361
3₁(9)	→	10
3₁(194)	→	195
3₁(596)	→	597
3₁(269)	→	270
3₁(308)	→	309
3₁(364)	→	365
3₁(300)	→	301
3₁(358)	→	359
3₁(334)	→	335
3₁(1061)	→	1062
3₁(535)	→	536
3₁(469)	→	470
3₁(375)	→	376
3₁(294)	→	295
3₁(347)	→	348
3₁(1207)	→	1208
3₁(1123)	→	1124
3₁(178)	→	179
3₁(289)	→	290
3₁(675)	→	676
3₁(451)	→	452
3₁(616)	→	617
3₁(440)	→	441
3₁(537)	→	538
3₁(408)	→	409
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
0₁(92)	→	93
0₁(590)	→	591
0₁(584)	→	585
0₁(574)	→	575
0₁(225)	→	226
0₁(456)	→	457
0₁(266)	→	267
0₁(131)	→	132
0₁(461)	→	462
0₁(1064)	→	1065
0₁(256)	→	257
0₁(568)	→	569
0₁(668)	→	669
0₁(1048)	→	1049
0₁(504)	→	505
0₁(279)	→	280
0₁(684)	→	685
0₁(216)	→	217
0₁(477)	→	478
0₁(290)	→	291
0₁(667)	→	668
0₁(368)	→	369
0₁(592)	→	593
0₁(1203)	→	1204
0₁(335)	→	336
0₁(226)	→	227
0₁(267)	→	268
0₁(12)	→	13
0₁(433)	→	434
0₁(145)	→	146
0₁(582)	→	583
0₁(554)	→	555
0₁(597)	→	598
0₁(336)	→	337
0₁(258)	→	259
0₁(566)	→	567
0₁(467)	→	468
0₁(316)	→	317
0₁(1113)	→	1114
0₁(242)	→	243
0₁(555)	→	556
0₁(459)	→	460
0₁(460)	→	461
0₁(315)	→	316
0₁(588)	→	589
0₁(594)	→	595
0₁(1063)	→	1064
0₁(673)	→	674
0₁(314)	→	315
0₁(11)	→	12
0₁(270)	→	271
0₁(265)	→	266
0₁(244)	→	245
0₁(1092)	→	1093
0₁(576)	→	577
0₁(97)	→	98
0₁(231)	→	232
0₁(140)	→	141
0₁(1091)	→	1092
0₁(1201)	→	1202
0₁(666)	→	667
0₁(301)	→	302
0₁(639)	→	640
4₁(383)	→	384
4₁(366)	→	367
4₁(374)	→	375
4₁(215)	→	216
4₁(409)	→	410
4₁(450)	→	451
4₁(371)	→	372
4₁(543)	→	544
4₁(1231)	→	1232
4₁(217)	→	218
4₁(439)	→	440
4₁(144)	→	145
4₁(109)	→	110
4₁(722)	→	723
4₁(1240)	→	1241
4₁(1420)	→	1421
4₁(1090)	→	1091
4₁(227)	→	228
4₁(1284)	→	1285
4₁(96)	→	97
4₁(107)	→	108
4₁(1286)	→	1287
4₁(452)	→	453
4₁(121)	→	122
4₁(309)	→	310
4₁(130)	→	131
4₁(94)	→	95
4₁(475)	→	476
4₁(1084)	→	1085
4₁(556)	→	557
4₁(280)	→	281
4₁(1426)	→	1427
4₁(1378)	→	1379
4₁(381)	→	382
4₁(213)	→	214
4₁(119)	→	120
4₁(128)	→	129
5₂(1022)	→	1023
5₂(989)	→	990
5₂(1488)	→	1489
5₂(1013)	→	1014
5₂(713)	→	714
5₂(1490)	→	1491
5₂(933)	→	934
5₂(900)	→	901
5₂(1044)	→	1045
5₂(921)	→	922
5₂(941)	→	942
5₂(712)	→	713
5₂(1346)	→	1347
5₂(1500)	→	1501
5₂(1307)	→	1308
5₂(919)	→	920
5₂(1418)	→	1419
5₂(1455)	→	1456
5₂(1032)	→	1033
5₂(1021)	→	1022
5₂(917)	→	918
5₂(1309)	→	1310
5₂(1034)	→	1035
5₂(947)	→	948
5₂(905)	→	906
5₂(1449)	→	1450
5₂(1042)	→	1043
5₂(1344)	→	1345
5₂(1443)	→	1444
5₂(1278)	→	1279
5₂(1392)	→	1393
5₂(931)	→	932
5₂(1412)	→	1413
5₂(911)	→	912
5₂(939)	→	940
5₂(1180)	→	1181
5₂(1019)	→	1020
0₀(1)	→	1
0₀(6)	→	1
0₀(5)	→	1
0₀(2)	→	1
0₀(3)	→	1
0₀(4)	→	1
3₂(714)	→	715
3₂(987)	→	988
3₂(1343)	→	1344
3₂(498)	→	499
3₂(1099)	→	1100
3₂(1476)	→	1477
3₂(902)	→	903
3₂(865)	→	866
3₂(682)	→	683
3₂(912)	→	913
3₂(653)	→	654

The automaton is closed under rewriting as it is compatible.