Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96029)

The rewrite relation of the following TRS is considered.

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

3(2(1(0(x1))))	→	3(3(2(x1)))	(26)
5(1(4(3(2(x1)))))	→	2(3(0(5(2(x1)))))	(27)
5(1(2(3(2(3(x1))))))	→	0(3(0(0(2(3(x1))))))	(28)
2(3(4(1(4(0(0(x1)))))))	→	1(0(3(3(5(5(x1))))))	(29)
2(3(0(0(1(2(1(5(x1))))))))	→	2(3(0(1(2(0(1(5(x1))))))))	(30)
2(5(0(2(0(4(2(3(4(x1)))))))))	→	2(1(2(2(1(1(5(0(x1))))))))	(31)
5(4(2(5(2(4(1(3(0(2(x1))))))))))	→	0(5(2(5(5(5(4(5(5(x1)))))))))	(32)
2(1(4(0(1(0(5(0(4(4(2(x1)))))))))))	→	2(5(2(0(2(0(4(3(1(4(2(x1)))))))))))	(33)
1(2(4(5(5(4(4(1(3(5(3(x1)))))))))))	→	1(0(3(4(5(4(3(2(5(3(3(x1)))))))))))	(34)
1(2(0(1(4(5(2(5(0(0(5(x1)))))))))))	→	2(3(1(1(1(5(4(5(4(5(x1))))))))))	(35)
1(5(3(1(0(3(2(3(3(4(1(4(x1))))))))))))	→	1(2(3(2(2(5(5(5(3(5(1(2(x1))))))))))))	(36)
5(4(5(5(2(2(4(0(4(0(4(5(x1))))))))))))	→	5(4(1(5(2(2(3(5(2(5(4(5(x1))))))))))))	(37)
1(4(1(0(3(4(1(3(0(5(2(4(5(x1)))))))))))))	→	1(2(2(3(5(5(2(0(5(2(4(4(5(x1)))))))))))))	(38)
3(5(5(5(4(1(3(3(2(0(1(4(4(3(x1))))))))))))))	→	3(3(2(3(1(2(2(0(3(5(5(4(3(1(x1))))))))))))))	(39)
0(4(0(3(2(2(2(3(4(0(5(1(5(2(5(x1)))))))))))))))	→	4(4(5(4(4(3(1(2(2(3(0(4(3(4(5(x1)))))))))))))))	(40)
5(2(4(5(5(4(0(1(4(3(1(1(1(2(5(0(x1))))))))))))))))	→	5(2(0(0(0(1(4(1(2(3(1(3(3(2(2(0(x1))))))))))))))))	(41)
2(0(0(3(3(0(1(4(2(5(1(2(5(4(2(5(x1))))))))))))))))	→	3(1(0(4(4(4(2(3(0(5(0(3(0(2(2(2(x1))))))))))))))))	(42)
5(3(1(5(2(1(1(4(2(0(4(3(5(3(2(0(1(0(x1))))))))))))))))))	→	4(1(3(3(2(1(5(3(2(1(5(0(2(5(3(1(0(x1)))))))))))))))))	(43)
5(3(2(3(3(3(3(3(4(2(2(5(4(2(4(3(0(1(x1))))))))))))))))))	→	1(4(2(3(2(3(0(0(2(4(3(2(5(3(5(2(0(0(1(x1)))))))))))))))))))	(44)
4(5(3(4(3(0(3(0(0(3(3(1(5(5(3(0(2(2(x1))))))))))))))))))	→	4(1(4(2(1(0(5(3(2(0(0(1(4(4(2(5(2(2(x1))))))))))))))))))	(45)
3(2(5(0(3(1(3(4(3(5(3(3(3(4(2(2(1(3(x1))))))))))))))))))	→	3(2(5(1(5(5(2(3(5(5(5(2(3(4(3(5(1(3(x1))))))))))))))))))	(46)
5(4(4(5(1(3(0(2(4(1(5(1(2(2(1(2(0(5(x1))))))))))))))))))	→	2(5(2(0(0(0(4(2(3(5(3(4(5(1(4(1(4(5(x1))))))))))))))))))	(47)
1(0(1(5(1(3(4(2(4(0(2(1(5(3(1(5(4(1(3(4(x1))))))))))))))))))))	→	1(0(0(3(2(4(4(2(0(0(1(5(2(2(4(4(3(5(3(1(5(x1)))))))))))))))))))))	(48)
2(1(4(3(3(4(4(4(1(3(1(3(1(4(4(1(5(4(2(1(1(x1)))))))))))))))))))))	→	4(3(2(5(4(0(1(1(5(4(4(1(2(1(5(2(2(2(2(4(0(x1)))))))))))))))))))))	(49)
5(1(5(5(1(4(1(2(4(3(0(4(4(1(5(0(0(2(0(4(1(x1)))))))))))))))))))))	→	4(3(4(2(1(0(1(2(3(5(4(3(5(0(2(2(2(3(3(1(1(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:

78	→	861
730	→	14
730	→	1079
33	→	43
33	→	92
33	→	432
33	→	120
33	→	94
33	→	65
376	→	14
376	→	996
376	→	1023
964	→	1139
29	→	1027
29	→	1081
128	→	878
263	→	225
789	→	18
791	→	781
967	→	13
87	→	1077
1117	→	326
1109	→	272
1072	→	37
286	→	1061
1142	→	33
15	→	7
15	→	268
15	→	14
15	→	84
15	→	26
15	→	35
15	→	13
15	→	174
15	→	234
15	→	1084
915	→	37
374	→	344
1121	→	357
129	→	7
129	→	778
129	→	33
129	→	17
129	→	1045
1140	→	33
995	→	17
119	→	37
145	→	231
145	→	356
547	→	197
547	→	70
547	→	27
547	→	144
547	→	32
547	→	12
547	→	25
547	→	48
547	→	7
547	→	16
547	→	109
547	→	13
226	→	171
226	→	954
955	→	357
939	→	990
939	→	1073
382	→	14
382	→	994
382	→	1021
1033	→	111
1062	→	73
1119	→	326
1074	→	145
187	→	128
146	→	857
146	→	1122
774	→	1059
37	→	920
1076	→	145
34	→	63
997	→	17
55	→	19
325	→	36
1082	→	234
20	→	7
20	→	92
20	→	43
20	→	33
20	→	197
20	→	70
20	→	27
20	→	16
20	→	109
20	→	13
20	→	145
20	→	110
20	→	121
20	→	729
20	→	1045
20	→	957
20	→	965
20	→	963
99	→	18
1068	→	37
31	→	7
31	→	33
31	→	111
31	→	1045
938	→	1000
49	→	173
49	→	211
49	→	326
49	→	475
1105	→	252
1078	→	216
877	→	13
877	→	174
877	→	234
877	→	1084
840	→	326
840	→	173
840	→	144
840	→	32
840	→	12
840	→	25
840	→	48
840	→	7
840	→	211
840	→	49
1022	→	28
13	→	16
13	→	70
13	→	109
13	→	197
13	→	144
13	→	32
13	→	12
13	→	25
13	→	48
13	→	7
895	→	92
895	→	310
895	→	144
895	→	32
895	→	12
895	→	25
895	→	48
895	→	7
895	→	43
895	→	33
1066	→	86
940	→	1042
940	→	1071
940	→	1114
965	→	13
477	→	962
477	→	964
477	→	1036
1111	→	37
416	→	92
416	→	7
416	→	43
416	→	33
416	→	1045
390	→	14
390	→	268
390	→	84
390	→	26
390	→	88
44	→	308
44	→	7
761	→	33
1064	→	71
26	→	84
26	→	268
26	→	14
1070	→	37
297	→	76
343	→	984
38	→	7
38	→	197
38	→	70
38	→	27
38	→	16
38	→	109
38	→	13
38	→	145
38	→	110
38	→	308
38	→	44
38	→	92
38	→	43
38	→	33
38	→	212
38	→	17
38	→	1066
38	→	1045
38	→	235
79	→	19
79	→	826
91	→	35
1005	→	111
36	→	375
36	→	387
248	→	37
894	→	1038
894	→	1067
894	→	1110
894	→	1120
172	→	7
172	→	326
172	→	173
172	→	211
172	→	49
172	→	92
172	→	310
172	→	43
172	→	33
172	→	285
172	→	134
172	→	159
172	→	93
172	→	197
172	→	70
172	→	16
172	→	109
172	→	13
172	→	95
172	→	1066
172	→	1045
779	→	767
1084	→	234
121	→	1104
171	→	751
171	→	798
171	→	914
810	→	225
839	→	1040
839	→	1069
839	→	1112
345	→	171
799	→	781
1037	→	33
431	→	413
1041	→	49
433	→	414
143	→	118
1060	→	33
941	→	197
941	→	70
941	→	7
941	→	16
941	→	109
941	→	13
232	→	727
344	→	412
344	→	818
876	→	1075
284	→	14
284	→	430
478	→	33
478	→	144
478	→	32
478	→	12
478	→	25
478	→	48
478	→	7
478	→	111
478	→	1045
1035	→	1028
959	→	268
959	→	14
959	→	84
959	→	26
1043	→	49
14	→	820
14	→	1065
913	→	286
1045	→	33
93	→	134
93	→	159
93	→	285
12	→	1044
989	→	33
989	→	111
989	→	1045
112	→	1108
7	→	12
7	→	25
7	→	32
7	→	48
7	→	144
991	→	17
69	→	30
69	→	766
1080	→	233
30	→	381
30	→	541
30	→	960
752	→	49
310	→	882
35	→	1034
198	→	249
821	→	145
47	→	17
17	→	96
154	→	14
768	→	804
858	→	180
1058	→	33
775	→	145
775	→	144
775	→	32
775	→	12
775	→	25
775	→	48
775	→	7
775	→	110
775	→	1063
775	→	729
1113	→	37
19	→	760
546	→	1116
43	→	1118
961	→	957
210	→	153
476	→	1083
767	→	912
966	→	1141
1123	→	359
262	→	780
94	→	120
415	→	1057
1039	→	49
819	→	145
1024	→	28
247	→	790
879	→	862
963	→	957
545	→	956
545	→	966
1115	→	37
1₁(71)	→	72
1₁(260)	→	261
1₁(126)	→	127
1₁(54)	→	55
1₁(934)	→	935
1₁(51)	→	52
1₁(339)	→	340
1₁(371)	→	372
1₁(46)	→	47
1₁(912)	→	913
1₁(820)	→	821
1₁(927)	→	928
1₁(153)	→	154
1₁(728)	→	729
1₁(889)	→	890
1₁(316)	→	317
1₁(885)	→	886
1₁(933)	→	934
1₁(772)	→	773
1₁(771)	→	772
1₁(929)	→	930
1₁(338)	→	339
1₁(1075)	→	1076
1₁(369)	→	370
1₁(875)	→	876
1₁(332)	→	333
1₁(356)	→	357
1₁(954)	→	955
1₁(144)	→	145
1₁(285)	→	286
1₁(96)	→	97
1₁(180)	→	181
1₁(37)	→	38
1₁(1073)	→	1074
1₁(50)	→	51
1₁(281)	→	282
1₁(833)	→	834
1₁(818)	→	819
1₁(165)	→	166
1₁(177)	→	178
1₁(770)	→	771
1₁(893)	→	894
1₁(268)	→	269
1₁(98)	→	99
1₁(225)	→	226
1₁(97)	→	98
1₁(1120)	→	1121
1₁(334)	→	335
1₁(781)	→	782
1₁(253)	→	254
1₁(217)	→	218
1₁(43)	→	44
1₁(182)	→	183
1₁(109)	→	110
1₁(287)	→	288
1₁(211)	→	212
1₁(546)	→	547
1₁(221)	→	222
2₂(1028)	→	1029
2₂(1004)	→	1005
2₂(962)	→	963
2₂(387)	→	388
2₂(988)	→	989
2₂(1000)	→	1001
2₂(984)	→	985
2₂(960)	→	961
2₂(956)	→	957
3₂(388)	→	389
3₂(958)	→	959
3₂(1003)	→	1004
3₂(1027)	→	1028
3₂(957)	→	958
3₂(1031)	→	1032
3₂(987)	→	988
3₂(1034)	→	1035
3₂(389)	→	390
5₁(282)	→	283
5₁(884)	→	885
5₁(220)	→	221
5₁(213)	→	214
5₁(65)	→	66
5₁(269)	→	270
5₁(926)	→	927
5₁(1036)	→	1037
5₁(331)	→	332
5₁(128)	→	129
5₁(93)	→	94
5₁(112)	→	113
5₁(994)	→	995
5₁(867)	→	868
5₁(148)	→	149
5₁(366)	→	367
5₁(113)	→	114
5₁(140)	→	141
5₁(541)	→	542
5₁(363)	→	364
5₁(412)	→	413
5₁(1114)	→	1115
5₁(276)	→	277
5₁(114)	→	115
5₁(78)	→	79
5₁(767)	→	768
5₁(1065)	→	1066
5₁(309)	→	310
5₁(275)	→	276
5₁(236)	→	237
5₁(147)	→	148
5₁(1059)	→	1060
5₁(291)	→	292
5₁(1112)	→	1113
5₁(121)	→	122
5₁(805)	→	806
5₁(337)	→	338
5₁(315)	→	316
5₁(279)	→	280
5₁(32)	→	33
5₁(169)	→	170
5₁(914)	→	915
5₁(888)	→	889
5₁(139)	→	140
5₁(769)	→	770
5₁(202)	→	203
5₁(990)	→	991
5₁(342)	→	343
5₁(85)	→	86
5₁(49)	→	50
5₁(809)	→	810
5₁(542)	→	543
5₁(782)	→	783
5₁(996)	→	997
5₁(66)	→	67
5₁(125)	→	126
5₁(216)	→	217
5₁(89)	→	90
5₁(274)	→	275
5₁(1110)	→	1111
5₁(785)	→	786
5₁(932)	→	933
5₁(33)	→	34
5₁(1141)	→	1142
5₁(1044)	→	1045
5₁(110)	→	111
5₁(258)	→	259
5₁(430)	→	431
5₁(1057)	→	1058
5₁(95)	→	96
5₁(760)	→	761
5₁(837)	→	838
5₁(136)	→	137
5₁(64)	→	65
5₁(786)	→	787
5₁(784)	→	785
5₁(937)	→	938
5₁(249)	→	250
5₁(280)	→	281
5₁(68)	→	69
5₁(1139)	→	1140
5₁(234)	→	235
5₁(288)	→	289
5₁(16)	→	17
5₀(7)	→	7
4₀(7)	→	7
0₀(7)	→	7
4₁(170)	→	171
4₁(286)	→	287
4₁(341)	→	342
4₁(171)	→	172
4₁(160)	→	161
4₁(1063)	→	1064
4₁(336)	→	337
4₁(873)	→	874
4₁(871)	→	872
4₁(88)	→	89
4₁(208)	→	209
4₁(826)	→	827
4₁(335)	→	336
4₁(930)	→	931
4₁(63)	→	64
4₁(320)	→	321
4₁(94)	→	95
4₁(146)	→	147
4₁(940)	→	941
4₁(365)	→	366
4₁(373)	→	374
4₁(1108)	→	1109
4₁(90)	→	91
4₁(207)	→	208
4₁(239)	→	240
4₁(921)	→	922
4₁(936)	→	937
4₁(839)	→	840
4₁(92)	→	93
4₁(167)	→	168
4₁(181)	→	182
4₁(872)	→	873
4₁(894)	→	895
4₁(251)	→	252
4₁(271)	→	272
4₁(289)	→	290
4₁(321)	→	322
4₁(206)	→	207
4₁(70)	→	71
4₁(835)	→	836
4₁(311)	→	312
4₁(828)	→	829
4₁(247)	→	248
4₁(836)	→	837
4₁(262)	→	263
4₁(326)	→	327
4₁(134)	→	135
4₁(294)	→	295
4₁(778)	→	779
4₁(312)	→	313
4₁(931)	→	932
4₁(127)	→	128
4₁(1104)	→	1105
4₁(252)	→	253
4₁(73)	→	74
4₁(768)	→	769
4₁(168)	→	169
4₁(838)	→	839
4₁(766)	→	767
3₁(224)	→	225
3₁(235)	→	236
3₁(176)	→	177
3₁(869)	→	870
3₁(290)	→	291
3₁(87)	→	88
3₁(827)	→	828
3₁(544)	→	545
3₁(72)	→	73
3₁(18)	→	19
3₁(200)	→	201
3₁(166)	→	167
3₁(175)	→	176
3₁(34)	→	35
3₁(270)	→	271
3₁(238)	→	239
3₁(939)	→	940
3₁(543)	→	544
3₁(243)	→	244
3₁(277)	→	278
3₁(145)	→	146
3₁(212)	→	213
3₁(84)	→	85
3₁(308)	→	309
3₁(891)	→	892
3₁(117)	→	118
3₁(876)	→	877
3₁(364)	→	365
3₁(14)	→	15
3₁(887)	→	888
3₁(344)	→	345
3₁(245)	→	246
3₁(162)	→	163
3₁(310)	→	311
3₁(111)	→	112
3₁(783)	→	784
3₁(358)	→	359
3₁(830)	→	831
3₁(865)	→	866
3₁(357)	→	358
3₁(834)	→	835
3₁(806)	→	807
3₁(1061)	→	1062
3₁(1122)	→	1123
3₁(122)	→	123
3₁(367)	→	368
3₁(35)	→	36
3₁(892)	→	893
3₁(292)	→	293
3₁(29)	→	30
3₁(149)	→	150
3₁(476)	→	477
3₁(323)	→	324
3₁(272)	→	273
3₁(13)	→	14
3₁(178)	→	179
3₁(219)	→	220
3₁(414)	→	415
3₁(25)	→	26
3₁(223)	→	224
3₁(204)	→	205
3₁(773)	→	774
3₁(159)	→	160
3₁(257)	→	258
3₁(141)	→	142
2₀(7)	→	7
1₀(7)	→	7
0₁(76)	→	77
0₁(199)	→	200
0₁(324)	→	325
0₁(17)	→	18
0₁(317)	→	318
0₁(1021)	→	1022
0₁(232)	→	233
0₁(864)	→	865
0₁(829)	→	830
0₁(362)	→	363
0₁(477)	→	478
0₁(161)	→	162
0₁(413)	→	414
0₁(254)	→	255
0₁(432)	→	433
0₁(184)	→	185
0₁(729)	→	730
0₁(475)	→	476
0₁(1079)	→	1080
0₁(874)	→	875
0₁(183)	→	184
0₁(920)	→	921
0₁(935)	→	936
0₁(241)	→	242
0₁(868)	→	869
0₁(137)	→	138
0₁(318)	→	319
0₁(1042)	→	1043
0₁(48)	→	49
0₁(203)	→	204
0₁(242)	→	243
0₁(1118)	→	1119
0₁(215)	→	216
0₁(295)	→	296
0₁(866)	→	867
0₁(1038)	→	1039
0₁(209)	→	210
0₁(883)	→	884
0₁(30)	→	31
0₁(74)	→	75
0₁(150)	→	151
0₁(296)	→	297
0₁(545)	→	546
0₁(27)	→	28
0₁(1023)	→	1024
0₁(1077)	→	1078
0₁(28)	→	29
0₁(1116)	→	1117
0₁(36)	→	37
0₁(340)	→	341
0₁(370)	→	371
0₁(44)	→	45
0₁(255)	→	256
0₁(231)	→	232
0₁(751)	→	752
0₁(185)	→	186
0₁(1040)	→	1041
0₁(259)	→	260
0₁(201)	→	202
2₁(774)	→	775
2₁(1083)	→	1084
2₁(359)	→	360
2₁(925)	→	926
2₁(53)	→	54
2₁(890)	→	891
2₁(327)	→	328
2₁(26)	→	27
2₁(329)	→	330
2₁(261)	→	262
2₁(372)	→	373
2₁(360)	→	361
2₁(862)	→	863
2₁(123)	→	124
2₁(831)	→	832
2₁(198)	→	199
2₁(218)	→	219
2₁(857)	→	858
2₁(246)	→	247
2₁(244)	→	245
2₁(237)	→	238
2₁(964)	→	965
2₁(116)	→	117
2₁(780)	→	781
2₁(333)	→	334
2₁(882)	→	883
2₁(966)	→	967
2₁(798)	→	799
2₁(328)	→	329
2₁(115)	→	116
2₁(368)	→	369
2₁(124)	→	125
2₁(163)	→	164
2₁(807)	→	808
2₁(415)	→	416
2₁(205)	→	206
2₁(12)	→	13
2₁(293)	→	294
2₁(343)	→	344
2₁(313)	→	314
2₁(788)	→	789
2₁(319)	→	320
2₁(222)	→	223
2₁(922)	→	923
2₁(45)	→	46
2₁(240)	→	241
2₁(179)	→	180
2₁(138)	→	139
2₁(861)	→	862
2₁(322)	→	323
2₁(67)	→	68
2₁(186)	→	187
2₁(924)	→	925
2₁(870)	→	871
2₁(273)	→	274
2₁(804)	→	805
2₁(173)	→	174
2₁(886)	→	887
2₁(278)	→	279
2₁(878)	→	879
2₁(19)	→	20
2₁(1067)	→	1068
2₁(118)	→	119
2₁(77)	→	78
2₁(86)	→	87
2₁(790)	→	791
2₁(164)	→	165
2₁(152)	→	153
2₁(120)	→	121
2₁(938)	→	939
2₁(863)	→	864
2₁(233)	→	234
2₁(75)	→	76
2₁(361)	→	362
2₁(135)	→	136
2₁(151)	→	152
2₁(314)	→	315
2₁(256)	→	257
2₁(142)	→	143
2₁(923)	→	924
2₁(928)	→	929
2₁(375)	→	376
2₁(1081)	→	1082
2₁(197)	→	198
2₁(1069)	→	1070
2₁(174)	→	175
2₁(832)	→	833
2₁(330)	→	331
2₁(250)	→	251
2₁(727)	→	728
2₁(787)	→	788
2₁(381)	→	382
2₁(1071)	→	1072
2₁(214)	→	215
2₁(808)	→	809
2₁(283)	→	284
2₁(52)	→	53
5₂(1001)	→	1002
5₂(985)	→	986
3₀(7)	→	7
0₂(986)	→	987
0₂(1002)	→	1003
0₂(1030)	→	1031
0₂(1032)	→	1033
0₂(1029)	→	1030

The automaton is closed under rewriting as it is compatible.