Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96256)

The rewrite relation of the following TRS is considered.

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

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

1(3(2(1(0(x1)))))	→	1(1(0(0(x1))))	(26)
5(3(2(5(4(x1)))))	→	5(0(4(4(x1))))	(27)
2(3(4(2(3(5(x1))))))	→	4(5(0(3(5(x1)))))	(28)
1(2(2(5(5(2(2(x1)))))))	→	0(1(3(3(2(3(x1))))))	(29)
4(3(1(1(2(5(4(x1)))))))	→	0(5(0(1(1(x1)))))	(30)
4(0(5(2(3(3(2(2(0(x1)))))))))	→	4(1(4(3(1(2(2(0(x1))))))))	(31)
4(2(5(0(0(4(0(3(2(x1)))))))))	→	4(0(4(0(3(2(2(2(3(x1)))))))))	(32)
3(1(0(5(3(3(3(4(2(x1)))))))))	→	5(0(5(0(0(1(0(x1)))))))	(33)
2(1(5(1(4(3(3(5(3(2(x1))))))))))	→	2(4(3(1(5(2(5(3(0(2(x1))))))))))	(34)
4(3(3(0(0(4(2(1(0(3(x1))))))))))	→	4(5(2(0(2(4(0(5(1(3(x1))))))))))	(35)
3(5(4(2(1(2(4(0(4(1(1(x1)))))))))))	→	4(2(0(2(2(5(1(0(1(1(x1))))))))))	(36)
5(4(1(3(3(0(0(4(2(1(3(x1)))))))))))	→	5(2(2(2(4(0(4(1(1(3(2(x1)))))))))))	(37)
3(0(5(1(4(0(1(4(0(3(4(x1)))))))))))	→	1(5(5(1(0(0(3(2(4(0(x1))))))))))	(38)
2(2(2(2(1(1(2(2(1(1(0(1(5(0(x1))))))))))))))	→	4(1(3(3(2(4(3(0(3(1(3(5(0(3(0(x1)))))))))))))))	(39)
3(3(3(1(0(2(5(2(4(1(1(2(5(0(x1))))))))))))))	→	2(2(3(0(4(2(0(5(4(4(4(0(4(0(x1))))))))))))))	(40)
3(1(0(2(2(1(2(3(3(0(2(3(2(0(3(x1)))))))))))))))	→	1(3(1(0(4(0(2(2(1(2(3(5(1(2(x1))))))))))))))	(41)
4(3(0(4(2(2(4(2(3(5(0(4(3(2(5(0(x1))))))))))))))))	→	1(2(3(1(0(3(2(2(3(1(5(0(0(0(x1))))))))))))))	(42)
4(1(3(5(0(1(1(3(1(1(3(3(5(2(4(4(x1))))))))))))))))	→	4(5(1(5(0(3(3(4(5(5(1(2(4(4(4(2(4(x1)))))))))))))))))	(43)
3(4(5(0(5(1(4(2(2(4(5(1(1(5(3(5(x1))))))))))))))))	→	1(1(1(5(0(1(2(3(1(2(2(4(0(0(x1))))))))))))))	(44)
2(5(4(5(0(5(0(1(5(2(2(4(5(3(4(1(0(2(2(x1)))))))))))))))))))	→	2(5(4(1(5(3(4(4(0(0(2(5(2(5(4(0(2(4(3(3(x1))))))))))))))))))))	(45)
3(3(4(2(0(1(2(2(1(1(3(5(2(3(1(4(3(5(2(x1)))))))))))))))))))	→	3(2(2(5(0(0(4(3(4(3(0(1(1(3(2(5(3(0(x1))))))))))))))))))	(46)
4(4(0(1(4(0(5(2(3(4(2(4(4(1(0(5(1(3(5(x1)))))))))))))))))))	→	4(5(2(0(2(0(2(5(2(4(3(2(5(1(1(4(2(2(5(x1)))))))))))))))))))	(47)
1(3(2(0(5(2(5(2(4(3(5(2(4(1(1(3(2(3(0(3(2(x1)))))))))))))))))))))	→	1(5(0(3(0(3(3(1(1(0(1(3(3(1(2(3(4(2(3(x1)))))))))))))))))))	(48)
5(4(3(0(2(3(4(4(2(3(1(1(4(2(2(1(3(1(2(1(3(x1)))))))))))))))))))))	→	5(1(1(4(2(5(0(1(3(1(0(1(2(1(1(5(5(2(x1))))))))))))))))))	(49)
3(5(0(3(3(4(2(2(0(4(3(1(0(3(5(4(3(1(3(4(5(x1)))))))))))))))))))))	→	5(3(1(5(0(2(1(0(1(0(0(4(2(5(1(1(5(5(x1))))))))))))))))))	(50)

1.1 Bounds

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

final states:

{7}

transitions:

1303	→	252
33	→	1003
1268	→	1304
793	→	137
176	→	769
899	→	329
1231	→	304
32	→	7
32	→	35
32	→	303
32	→	109
32	→	165
32	→	80
32	→	290
32	→	153
32	→	194
32	→	19
32	→	128
32	→	231
32	→	229
32	→	29
32	→	90
32	→	34
32	→	20
32	→	635
32	→	414
32	→	1004
32	→	1229
89	→	7
89	→	303
89	→	109
89	→	165
89	→	80
89	→	229
89	→	230
89	→	90
89	→	34
89	→	270
89	→	1067
89	→	1045
89	→	1004
89	→	944
89	→	955
128	→	153
128	→	194
128	→	79
128	→	33
128	→	18
128	→	13
128	→	27
128	→	44
128	→	7
128	→	19
745	→	983
830	→	860
1138	→	31
1106	→	109
1106	→	1182
1106	→	1230
1056	→	14
732	→	31
80	→	109
80	→	165
80	→	303
80	→	634
1072	→	332
897	→	304
1166	→	1274
1166	→	1282
1313	→	166
1261	→	16
97	→	30
734	→	730
15	→	182
15	→	218
15	→	842
1046	→	166
1237	→	304
933	→	1129
1209	→	14
1140	→	1154
1140	→	1208
1253	→	304
998	→	109
998	→	1043
998	→	1065
706	→	64
1327	→	304
705	→	937
705	→	985
1098	→	45
978	→	45
815	→	229
815	→	230
815	→	79
815	→	33
815	→	18
815	→	13
815	→	27
815	→	44
815	→	7
815	→	90
815	→	34
815	→	944
815	→	955
39	→	7
39	→	166
39	→	45
39	→	194
39	→	19
39	→	636
39	→	231
39	→	1046
955	→	944
939	→	1131
988	→	70
988	→	1059
382	→	27
382	→	1029
382	→	1037
382	→	1051
772	→	109
772	→	826
772	→	896
817	→	806
980	→	45
907	→	1139
1062	→	252
740	→	92
861	→	219
108	→	31
443	→	430
443	→	864
110	→	944
110	→	955
34	→	90
34	→	229
34	→	800
34	→	230
34	→	79
34	→	33
34	→	18
34	→	13
34	→	27
34	→	44
34	→	7
34	→	954
319	→	21
1048	→	14
1229	→	18
1183	→	166
55	→	31
813	→	935
813	→	958
1110	→	109
1110	→	1184
1110	→	1236
1275	→	34
193	→	16
20	→	1210
1068	→	304
107	→	707
713	→	929
713	→	1013
713	→	1035
713	→	1049
31	→	508
31	→	773
31	→	898
942	→	34
938	→	34
1132	→	109
1132	→	1200
1132	→	1246
246	→	379
246	→	927
380	→	38
841	→	194
841	→	79
841	→	33
841	→	18
841	→	13
841	→	27
841	→	44
841	→	7
841	→	19
841	→	231
936	→	34
71	→	345
71	→	741
716	→	708
716	→	880
127	→	977
127	→	1005
1112	→	109
1112	→	1191
1112	→	1238
1004	→	109
1004	→	1045
1004	→	1067
1004	→	1228
895	→	304
1267	→	413
1066	→	304
940	→	34
1223	→	272
770	→	109
770	→	894
1185	→	166
1319	→	166
1052	→	14
139	→	912
139	→	1254
1130	→	109
1130	→	1193
1130	→	1244
747	→	229
747	→	29
747	→	79
747	→	33
747	→	18
747	→	13
747	→	27
747	→	44
747	→	7
747	→	90
747	→	34
747	→	414
1283	→	70
1283	→	1302
135	→	16
1064	→	273
1194	→	166
881	→	868
1030	→	137
783	→	252
783	→	229
783	→	7
783	→	90
783	→	34
783	→	137
208	→	30
268	→	7
268	→	229
268	→	230
268	→	90
268	→	34
177	→	16
21	→	412
21	→	798
21	→	802
21	→	828
1277	→	944
912	→	1097
912	→	1137
138	→	1290
441	→	430
441	→	862
509	→	503
346	→	111
346	→	7
346	→	45
346	→	91
949	→	636
1311	→	109
1311	→	1318
1311	→	1326
639	→	127
302	→	134
302	→	792
116	→	429
116	→	973
1042	→	156
88	→	442
88	→	715
986	→	70
986	→	1057
799	→	137
982	→	34
1092	→	33
1092	→	1260
22	→	7
22	→	328
22	→	269
22	→	28
22	→	229
22	→	90
22	→	34
22	→	29
22	→	140
22	→	413
22	→	932
22	→	414
431	→	705
431	→	892
288	→	1053
174	→	900
1297	→	14
264	→	1047
264	→	1093
1192	→	166
803	→	816
1014	→	137
1036	→	20
117	→	866
1060	→	252
863	→	31
814	→	941
814	→	989
937	→	1109
941	→	1111
265	→	981
28	→	269
28	→	328
28	→	7
28	→	413
28	→	932
1291	→	137
118	→	21
344	→	21
827	→	166
843	→	831
801	→	138
801	→	1284
904	→	111
45	→	739
45	→	995
959	→	944
1217	→	14
704	→	34
14	→	49
14	→	70
14	→	127
14	→	136
913	→	35
913	→	634
913	→	165
913	→	7
913	→	109
913	→	303
913	→	80
913	→	1004
913	→	635
913	→	1229
1094	→	413
63	→	939
63	→	987
981	→	1105
1012	→	31
1201	→	166
746	→	979
746	→	1011
1247	→	304
1091	→	1266
1091	→	1296
282	→	94
1044	→	166
7	→	13
7	→	18
7	→	27
7	→	33
7	→	44
7	→	79
1006	→	31
1255	→	16
69	→	31
934	→	34
417	→	290
1038	→	20
1038	→	1041
1239	→	304
137	→	252
64	→	79
64	→	33
64	→	18
64	→	13
64	→	27
64	→	44
64	→	7
46	→	1071
1305	→	109
1305	→	1312
1305	→	1320
1321	→	304
35	→	63
35	→	287
893	→	288
990	→	70
990	→	1061
908	→	1091
908	→	1216
909	→	328
909	→	7
909	→	269
909	→	28
909	→	413
909	→	932
48	→	38
245	→	502
245	→	905
17	→	7
17	→	111
17	→	45
17	→	91
17	→	252
17	→	229
17	→	90
17	→	34
17	→	137
17	→	194
17	→	19
17	→	231
47	→	102
1203	→	166
714	→	229
714	→	7
714	→	90
714	→	34
164	→	88
1136	→	109
1136	→	1202
1136	→	1252
1245	→	304
254	→	733
703	→	997
148	→	54
267	→	725
267	→	771
267	→	1222
1153	→	912
974	→	944
928	→	413
865	→	31
1054	→	197
1058	→	252
74	→	20
953	→	944
1165	→	1268
1165	→	1276
932	→	413
1285	→	137
19	→	194
19	→	381
19	→	1063
935	→	1135
1050	→	14
266	→	703
266	→	991
1269	→	34
507	→	194
507	→	79
507	→	33
507	→	18
507	→	13
507	→	27
507	→	44
507	→	7
507	→	19
507	→	231
1211	→	198
27	→	931
27	→	1055
930	→	413
1167	→	944
1167	→	954
1167	→	229
1167	→	230
1167	→	1055
1167	→	1003
1167	→	44
1167	→	27
1167	→	13
1167	→	18
1167	→	33
1167	→	79
1167	→	7
1167	→	90
1167	→	800
1167	→	34
1167	→	955
163	→	440
163	→	952
984	→	70
992	→	81
1274	→	1310
996	→	70
430	→	933
430	→	943
228	→	15
247	→	88
879	→	20
435	→	166
435	→	79
435	→	33
435	→	18
435	→	13
435	→	27
435	→	44
435	→	7
435	→	45
435	→	636
435	→	1046
0₁(71)	→	72
0₁(1208)	→	1209
0₁(434)	→	435
0₁(95)	→	96
0₁(137)	→	138
0₁(828)	→	829
0₁(1011)	→	1012
0₁(313)	→	314
0₁(46)	→	47
0₁(1047)	→	1048
0₁(263)	→	264
0₁(778)	→	779
0₁(381)	→	382
0₁(1155)	→	1156
0₁(777)	→	778
0₁(710)	→	711
0₁(106)	→	107
0₁(335)	→	336
0₁(153)	→	154
0₁(1163)	→	1164
0₁(238)	→	239
0₁(158)	→	159
0₁(989)	→	990
0₁(1296)	→	1297
0₁(987)	→	988
0₁(725)	→	726
0₁(506)	→	507
0₁(1146)	→	1147
0₁(836)	→	837
0₁(1005)	→	1006
0₁(709)	→	710
0₁(985)	→	986
0₁(174)	→	175
0₁(205)	→	206
0₁(66)	→	67
0₁(983)	→	984
0₁(808)	→	809
0₁(80)	→	81
0₁(262)	→	263
0₁(309)	→	310
0₁(232)	→	233
0₁(1139)	→	1140
0₁(340)	→	341
0₁(172)	→	173
0₁(995)	→	996
0₁(113)	→	114
0₁(712)	→	713
0₁(878)	→	879
0₁(299)	→	300
0₁(301)	→	302
0₁(1051)	→	1052
0₁(991)	→	992
0₁(281)	→	282
0₁(29)	→	30
0₁(92)	→	93
0₁(130)	→	131
0₁(744)	→	745
0₁(13)	→	14
0₁(131)	→	132
0₁(1282)	→	1283
0₁(866)	→	867
0₁(1137)	→	1138
0₁(1049)	→	1050
0₁(773)	→	774
0₁(14)	→	15
0₁(1055)	→	1056
0₁(337)	→	338
0₁(225)	→	226
0₁(873)	→	874
0₁(715)	→	716
0₁(20)	→	21
0₁(334)	→	335
0₁(1141)	→	1142
0₁(504)	→	505
0₁(189)	→	190
0₁(257)	→	258
0₁(239)	→	240
0₁(294)	→	295
0₁(1216)	→	1217
0₁(811)	→	812
0₁(38)	→	39
0₁(182)	→	183
0₁(142)	→	143
0₁(707)	→	708
0₁(829)	→	830
0₁(803)	→	804
0₁(1160)	→	1161
0₁(800)	→	801
0₁(68)	→	69
0₁(72)	→	73
0₁(161)	→	162
1₂(903)	→	904
1₂(947)	→	948
1₂(902)	→	903
5₂(412)	→	413
5₂(415)	→	416
5₂(927)	→	928
5₂(931)	→	932
5₂(1266)	→	1267
5₂(1093)	→	1094
5₂(908)	→	909
5₂(929)	→	930
4₂(416)	→	417
4₂(906)	→	907
4₂(905)	→	906
4₁(1035)	→	1036
4₁(87)	→	88
4₁(912)	→	913
4₁(93)	→	94
4₁(112)	→	113
4₁(746)	→	747
4₁(1210)	→	1211
4₁(195)	→	196
4₁(245)	→	246
4₁(810)	→	811
4₁(160)	→	161
4₁(1222)	→	1223
4₁(114)	→	115
4₁(154)	→	155
4₁(271)	→	272
4₁(860)	→	861
4₁(1158)	→	1159
4₁(287)	→	288
4₁(230)	→	231
4₁(805)	→	806
4₁(1041)	→	1042
4₁(277)	→	278
4₁(240)	→	241
4₁(31)	→	32
4₁(18)	→	19
4₁(816)	→	817
4₁(202)	→	203
4₁(1156)	→	1157
4₁(333)	→	334
4₁(144)	→	145
4₁(67)	→	68
4₁(1037)	→	1038
4₁(637)	→	638
4₁(155)	→	156
4₁(802)	→	803
4₁(197)	→	198
4₁(259)	→	260
4₁(877)	→	878
4₁(127)	→	128
4₁(892)	→	893
4₁(1148)	→	1149
4₁(196)	→	197
4₁(804)	→	805
4₁(241)	→	242
4₁(173)	→	174
4₁(806)	→	807
4₁(1157)	→	1158
4₁(261)	→	262
4₁(218)	→	219
4₁(53)	→	54
4₁(1162)	→	1163
4₁(19)	→	20
4₁(233)	→	234
4₁(875)	→	876
4₁(1154)	→	1155
4₁(156)	→	157
4₁(316)	→	317
4₁(774)	→	775
4₁(379)	→	380
4₁(1053)	→	1054
5₀(7)	→	7
4₀(7)	→	7
2₂(944)	→	945
0₀(7)	→	7
5₁(868)	→	869
5₁(341)	→	342
5₁(21)	→	22
5₁(807)	→	808
5₁(246)	→	247
5₁(1230)	→	1231
5₁(201)	→	202
5₁(47)	→	48
5₁(781)	→	782
5₁(82)	→	83
5₁(279)	→	280
5₁(1065)	→	1066
5₁(1260)	→	1261
5₁(1067)	→	1068
5₁(830)	→	831
5₁(741)	→	742
5₁(1254)	→	1255
5₁(27)	→	28
5₁(733)	→	734
5₁(226)	→	227
5₁(304)	→	305
5₁(898)	→	899
5₁(896)	→	897
5₁(157)	→	158
5₁(711)	→	712
5₁(236)	→	237
5₁(84)	→	85
5₁(1252)	→	1253
5₁(505)	→	506
5₁(234)	→	235
5₁(166)	→	167
5₁(739)	→	740
5₁(1159)	→	1160
5₁(1091)	→	1092
5₁(1142)	→	1143
5₁(894)	→	895
5₁(314)	→	315
5₁(729)	→	730
5₁(103)	→	104
5₁(1236)	→	1237
5₁(1246)	→	1247
5₁(30)	→	31
5₁(206)	→	207
5₁(133)	→	134
5₁(274)	→	275
5₁(1244)	→	1245
5₁(1238)	→	1239
5₁(138)	→	139
5₁(780)	→	781
5₁(183)	→	184
5₁(713)	→	714
5₁(134)	→	135
5₁(331)	→	332
5₁(727)	→	728
5₁(842)	→	843
5₁(1326)	→	1327
5₁(328)	→	329
5₁(303)	→	304
5₁(91)	→	92
5₁(1071)	→	1072
5₁(264)	→	265
5₁(1320)	→	1321
5₁(252)	→	253
5₁(73)	→	74
5₁(243)	→	244
5₁(200)	→	201
3₁(267)	→	268
3₁(146)	→	147
3₁(798)	→	799
3₁(176)	→	177
3₁(838)	→	839
3₁(147)	→	148
3₁(935)	→	936
3₁(229)	→	230
3₁(1057)	→	1058
3₁(65)	→	66
3₁(297)	→	298
3₁(432)	→	433
3₁(880)	→	881
3₁(185)	→	186
3₁(1302)	→	1303
3₁(864)	→	865
3₁(862)	→	863
3₁(311)	→	312
3₁(139)	→	140
3₁(874)	→	875
3₁(832)	→	833
3₁(188)	→	189
3₁(1140)	→	1141
3₁(442)	→	443
3₁(792)	→	793
3₁(870)	→	871
3₁(258)	→	259
3₁(939)	→	940
3₁(429)	→	430
3₁(260)	→	261
3₁(933)	→	934
3₁(242)	→	243
3₁(222)	→	223
3₁(191)	→	192
3₁(776)	→	777
3₁(1151)	→	1152
3₁(1284)	→	1285
3₁(109)	→	110
3₁(636)	→	637
3₁(731)	→	732
3₁(167)	→	168
3₁(1145)	→	1146
3₁(876)	→	877
3₁(1147)	→	1148
3₁(1143)	→	1144
3₁(867)	→	868
3₁(300)	→	301
3₁(162)	→	163
3₁(835)	→	836
3₁(726)	→	727
3₁(36)	→	37
3₁(941)	→	942
3₁(431)	→	432
3₁(937)	→	938
3₁(1274)	→	1275
3₁(291)	→	292
3₁(1061)	→	1062
3₁(143)	→	144
3₁(298)	→	299
3₁(129)	→	130
3₁(1029)	→	1030
3₁(28)	→	29
3₁(1164)	→	1165
3₁(35)	→	36
3₁(812)	→	813
3₁(1059)	→	1060
3₁(1290)	→	1291
3₁(292)	→	293
3₁(343)	→	344
3₁(52)	→	53
3₁(276)	→	277
3₁(288)	→	289
3₁(33)	→	34
3₁(136)	→	137
3₁(1013)	→	1014
3₁(1150)	→	1151
3₁(703)	→	704
3₁(1268)	→	1269
3₁(254)	→	255
3₁(86)	→	87
3₁(204)	→	205
3₁(81)	→	82
3₁(440)	→	441
3₁(203)	→	204
3₁(981)	→	982
3₁(141)	→	142
3₀(7)	→	7
2₀(7)	→	7
2₁(186)	→	187
2₁(187)	→	188
2₁(745)	→	746
2₁(237)	→	238
2₁(94)	→	95
2₁(266)	→	267
2₁(430)	→	431
2₁(814)	→	815
2₁(332)	→	333
2₁(1165)	→	1166
2₁(771)	→	772
2₁(1129)	→	1130
2₁(728)	→	729
2₁(1161)	→	1162
2₁(834)	→	835
2₁(117)	→	118
2₁(159)	→	160
2₁(128)	→	129
2₁(105)	→	106
2₁(63)	→	64
2₁(839)	→	840
2₁(220)	→	221
2₁(88)	→	89
2₁(104)	→	105
2₁(809)	→	810
2₁(49)	→	50
2₁(235)	→	236
2₁(775)	→	776
2₁(223)	→	224
2₁(145)	→	146
2₁(1135)	→	1136
2₁(1228)	→	1229
2₁(219)	→	220
2₁(83)	→	84
2₁(869)	→	870
2₁(107)	→	108
2₁(280)	→	281
2₁(168)	→	169
2₁(997)	→	998
2₁(79)	→	80
2₁(34)	→	35
2₁(1111)	→	1112
2₁(1310)	→	1311
2₁(813)	→	814
2₁(1109)	→	1110
2₁(705)	→	706
2₁(1003)	→	1004
2₁(315)	→	316
2₁(833)	→	834
2₁(743)	→	744
2₁(115)	→	116
2₁(269)	→	270
2₁(1149)	→	1150
2₁(634)	→	635
2₁(270)	→	271
2₁(278)	→	279
2₁(253)	→	254
2₁(265)	→	266
2₁(339)	→	340
2₁(1304)	→	1305
2₁(769)	→	770
2₁(198)	→	199
2₁(50)	→	51
2₁(1131)	→	1132
2₁(231)	→	232
2₁(171)	→	172
2₁(289)	→	290
2₁(194)	→	195
2₁(742)	→	743
2₁(1166)	→	1167
2₁(64)	→	65
2₁(163)	→	164
2₁(96)	→	97
2₁(275)	→	276
2₁(170)	→	171
2₁(116)	→	117
2₁(1105)	→	1106
2₁(192)	→	193
2₁(307)	→	308
1₁(296)	→	297
1₁(1152)	→	1153
1₁(165)	→	166
1₁(308)	→	309
1₁(207)	→	208
1₁(318)	→	319
1₁(305)	→	306
1₁(37)	→	38
1₁(44)	→	45
1₁(199)	→	200
1₁(329)	→	330
1₁(708)	→	709
1₁(290)	→	291
1₁(190)	→	191
1₁(831)	→	832
1₁(433)	→	434
1₁(1202)	→	1203
1₁(1045)	→	1046
1₁(16)	→	17
1₁(244)	→	245
1₁(1312)	→	1313
1₁(255)	→	256
1₁(979)	→	980
1₁(779)	→	780
1₁(1191)	→	1192
1₁(840)	→	841
1₁(110)	→	111
1₁(1318)	→	1319
1₁(503)	→	504
1₁(169)	→	170
1₁(111)	→	112
1₁(306)	→	307
1₁(293)	→	294
1₁(638)	→	639
1₁(502)	→	503
1₁(102)	→	103
1₁(1043)	→	1044
1₁(45)	→	46
1₁(175)	→	176
1₁(730)	→	731
1₁(295)	→	296
1₁(336)	→	337
1₁(227)	→	228
1₁(342)	→	343
1₁(872)	→	873
1₁(1193)	→	1194
1₁(51)	→	52
1₁(871)	→	872
1₁(1097)	→	1098
1₁(90)	→	91
1₁(85)	→	86
1₁(273)	→	274
1₁(635)	→	636
1₁(977)	→	978
1₁(224)	→	225
1₁(221)	→	222
1₁(140)	→	141
1₁(1063)	→	1064
1₁(310)	→	311
1₁(312)	→	313
1₁(132)	→	133
1₁(256)	→	257
1₁(70)	→	71
1₁(15)	→	16
1₁(1184)	→	1185
1₁(272)	→	273
1₁(317)	→	318
1₁(826)	→	827
1₁(330)	→	331
1₁(508)	→	509
1₁(54)	→	55
1₁(837)	→	838
1₁(184)	→	185
1₁(1200)	→	1201
1₁(782)	→	783
1₁(1182)	→	1183
1₁(338)	→	339
1₁(345)	→	346
1₁(1144)	→	1145
3₂(1276)	→	1277
3₂(945)	→	946
3₂(943)	→	944
3₂(954)	→	955
3₂(413)	→	414
3₂(973)	→	974
3₂(946)	→	947
3₂(958)	→	959
3₂(952)	→	953
1₀(7)	→	7
0₂(948)	→	949
0₂(907)	→	908
0₂(414)	→	415
0₂(900)	→	901
0₂(901)	→	902

The automaton is closed under rewriting as it is compatible.