Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96464)

The rewrite relation of the following TRS is considered.

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

33	→	7
33	→	163
33	→	67
33	→	17
33	→	293
111	→	126
867	→	352
329	→	87
25	→	772
486	→	68
486	→	251
486	→	151
1056	→	404
967	→	975
80	→	110
80	→	137
80	→	826
80	→	919
80	→	1055
152	→	267
1089	→	191
214	→	73
874	→	13
880	→	17
809	→	151
15	→	7
15	→	39
15	→	40
15	→	14
15	→	385
15	→	545
15	→	82
15	→	767
15	→	948
15	→	900
15	→	353
743	→	72
294	→	949
640	→	866
640	→	875
561	→	913
96	→	14
641	→	163
641	→	192
641	→	292
641	→	79
641	→	16
641	→	12
641	→	38
641	→	150
641	→	7
641	→	67
641	→	17
882	→	480
543	→	18
136	→	7
136	→	295
136	→	311
136	→	101
136	→	202
136	→	39
136	→	40
136	→	137
136	→	110
136	→	80
136	→	203
136	→	236
136	→	140
956	→	234
211	→	389
119	→	31
145	→	95
878	→	17
18	→	28
18	→	820
978	→	352
815	→	191
39	→	101
39	→	202
39	→	311
39	→	7
988	→	352
980	→	352
1062	→	480
406	→	239
406	→	1034
805	→	140
740	→	993
861	→	219
861	→	995
861	→	1011
108	→	879
108	→	883
108	→	915
108	→	923
108	→	929
219	→	947
914	→	47
95	→	351
95	→	397
1000	→	52
1000	→	1015
483	→	1063
175	→	135
813	→	191
1095	→	79
892	→	1035
1068	→	79
293	→	550
942	→	135
938	→	135
246	→	65
246	→	1067
968	→	151
1034	→	239
786	→	877
786	→	881
786	→	894
786	→	925
786	→	931
786	→	971
1010	→	164
1026	→	135
936	→	135
1022	→	164
901	→	14
901	→	973
316	→	519
13	→	24
13	→	47
13	→	191
13	→	233
1004	→	52
1004	→	1021
895	→	40
895	→	917
1066	→	164
940	→	135
392	→	73
392	→	214
44	→	735
884	→	480
426	→	989
480	→	935
135	→	432
135	→	483
135	→	556
135	→	808
135	→	814
135	→	862
970	→	293
1064	→	52
1064	→	1065
73	→	889
769	→	90
881	→	1001
1070	→	52
1070	→	1084
920	→	139
309	→	806
562	→	967
562	→	969
994	→	90
916	→	101
201	→	133
268	→	334
924	→	151
150	→	979
526	→	29
976	→	352
172	→	842
918	→	102
839	→	293
773	→	113
220	→	292
220	→	79
220	→	16
220	→	12
220	→	38
220	→	150
220	→	7
220	→	293
109	→	17
88	→	18
986	→	352
982	→	352
52	→	371
52	→	424
484	→	1025
522	→	319
433	→	739
433	→	937
433	→	1009
485	→	1027
350	→	18
204	→	804
82	→	385
82	→	1033
923	→	985
53	→	7
53	→	163
53	→	192
53	→	67
53	→	17
53	→	60
53	→	251
53	→	219
53	→	151
53	→	48
53	→	220
53	→	293
53	→	29
53	→	68
53	→	773
53	→	544
53	→	551
1036	→	251
808	→	981
859	→	1061
859	→	1094
863	→	843
787	→	295
787	→	311
787	→	101
787	→	292
787	→	79
787	→	16
787	→	12
787	→	38
787	→	150
787	→	7
787	→	202
787	→	39
787	→	40
265	→	955
232	→	32
1018	→	164
876	→	13
827	→	235
557	→	770
479	→	1003
45	→	828
45	→	838
66	→	52
106	→	902
14	→	542
481	→	939
972	→	312
1012	→	164
925	→	977
738	→	60
738	→	251
738	→	7
738	→	219
738	→	151
738	→	48
738	→	773
236	→	403
1091	→	52
1091	→	1092
282	→	265
736	→	47
7	→	12
7	→	16
7	→	38
7	→	79
7	→	150
7	→	292
563	→	251
563	→	68
563	→	7
563	→	219
563	→	151
69	→	544
1085	→	164
806	→	983
46	→	7
46	→	251
46	→	68
46	→	219
46	→	151
162	→	52
950	→	222
434	→	941
847	→	885
310	→	73
948	→	135
893	→	481
828	→	987
990	→	14
990	→	1053
48	→	60
821	→	202
245	→	479
245	→	812
771	→	102
17	→	67
17	→	163
17	→	7
926	→	151
398	→	13
68	→	89
858	→	1086
858	→	1088
974	→	312
1087	→	480
865	→	352
1054	→	312
829	→	151
353	→	900
1093	→	164
482	→	53
482	→	996
482	→	993
482	→	740
388	→	85
74	→	52
932	→	191
1002	→	52
1002	→	1017
1028	→	135
807	→	151
903	→	47
19	→	7
19	→	219
19	→	151
19	→	68
19	→	220
19	→	312
19	→	544
19	→	551
328	→	523
1016	→	164
266	→	135
372	→	14
372	→	737
354	→	39
354	→	15
354	→	770
354	→	557
354	→	239
354	→	1034
354	→	901
27	→	18
551	→	544
888	→	850
767	→	82
70	→	637
930	→	191
427	→	40
427	→	39
427	→	295
427	→	770
427	→	557
427	→	239
427	→	1034
737	→	864
737	→	873
984	→	352
151	→	219
151	→	251
151	→	766
151	→	768
996	→	89
192	→	778
1061	→	1069
1086	→	1090
883	→	999
545	→	87
435	→	219
435	→	151
435	→	12
435	→	38
435	→	150
435	→	292
435	→	79
435	→	16
435	→	7
0₁(95)	→	96
0₁(828)	→	829
0₁(82)	→	83
0₁(196)	→	197
0₁(558)	→	559
0₁(741)	→	742
0₁(159)	→	160
0₁(344)	→	345
0₁(140)	→	141
0₁(106)	→	107
0₁(923)	→	924
0₁(240)	→	241
0₁(158)	→	159
0₁(236)	→	237
0₁(306)	→	307
0₁(166)	→	167
0₁(243)	→	244
0₁(740)	→	741
0₁(772)	→	773
0₁(114)	→	115
0₁(806)	→	807
0₁(198)	→	199
0₁(275)	→	276
0₁(67)	→	68
0₁(129)	→	130
0₁(52)	→	53
0₁(318)	→	319
0₁(808)	→	809
0₁(780)	→	781
0₁(80)	→	81
0₁(86)	→	87
0₁(144)	→	145
0₁(340)	→	341
0₁(150)	→	151
0₁(561)	→	562
0₁(93)	→	94
0₁(995)	→	996
0₁(341)	→	342
0₁(173)	→	174
0₁(112)	→	113
0₁(852)	→	853
0₁(849)	→	850
0₁(295)	→	296
0₁(230)	→	231
0₁(281)	→	282
0₁(1035)	→	1036
0₁(131)	→	132
0₁(209)	→	210
0₁(640)	→	641
0₁(307)	→	308
0₁(321)	→	322
0₁(268)	→	269
0₁(267)	→	268
0₁(925)	→	926
0₁(47)	→	48
0₁(194)	→	195
0₁(967)	→	968
0₁(737)	→	738
0₁(70)	→	71
0₁(41)	→	42
0₁(28)	→	29
0₁(253)	→	254
0₁(300)	→	301
0₁(742)	→	743
0₁(782)	→	783
0₁(739)	→	740
0₁(254)	→	255
0₁(69)	→	70
0₁(211)	→	212
0₁(68)	→	69
0₁(48)	→	49
0₁(161)	→	162
0₁(193)	→	194
0₁(550)	→	551
0₁(44)	→	45
3₂(892)	→	893
4₂(1086)	→	1087
4₂(885)	→	886
4₂(479)	→	480
4₂(881)	→	882
4₂(483)	→	484
4₂(883)	→	884
4₂(519)	→	520
4₂(523)	→	524
4₂(1061)	→	1062
5₂(521)	→	522
5₂(481)	→	482
5₂(887)	→	888
5₂(886)	→	887
5₂(485)	→	486
5₂(524)	→	525
5₂(525)	→	526
5₂(520)	→	521
5₂(480)	→	481
5₂(484)	→	485
4₁(1001)	→	1002
4₁(143)	→	144
4₁(65)	→	66
4₁(142)	→	143
4₁(87)	→	88
4₁(128)	→	129
4₁(1021)	→	1022
4₁(303)	→	304
4₁(221)	→	222
4₁(559)	→	560
4₁(1009)	→	1010
4₁(163)	→	164
4₁(126)	→	127
4₁(154)	→	155
4₁(271)	→	272
4₁(860)	→	861
4₁(999)	→	1000
4₁(1065)	→	1066
4₁(62)	→	63
4₁(779)	→	780
4₁(1011)	→	1012
4₁(191)	→	192
4₁(32)	→	33
4₁(993)	→	994
4₁(1017)	→	1018
4₁(277)	→	278
4₁(257)	→	258
4₁(224)	→	225
4₁(63)	→	64
4₁(228)	→	229
4₁(342)	→	343
4₁(153)	→	154
4₁(879)	→	880
4₁(49)	→	50
4₁(637)	→	638
4₁(949)	→	950
4₁(43)	→	44
4₁(848)	→	849
4₁(877)	→	878
4₁(89)	→	90
4₁(1092)	→	1093
4₁(1003)	→	1004
4₁(768)	→	769
4₁(1084)	→	1085
4₁(258)	→	259
4₁(260)	→	261
4₁(225)	→	226
4₁(1090)	→	1091
4₁(265)	→	266
4₁(317)	→	318
4₁(105)	→	106
4₁(432)	→	433
4₁(560)	→	561
4₁(104)	→	105
4₁(30)	→	31
4₁(1069)	→	1070
4₁(1015)	→	1016
4₁(336)	→	337
4₁(199)	→	200
4₁(60)	→	61
4₁(200)	→	201
4₁(156)	→	157
4₁(855)	→	856
4₁(116)	→	117
4₁(324)	→	325
4₁(42)	→	43
4₁(278)	→	279
4₁(1063)	→	1064
4₁(16)	→	17
3₀(7)	→	7
5₀(7)	→	7
4₀(7)	→	7
5₁(170)	→	171
5₁(301)	→	302
5₁(299)	→	300
5₁(17)	→	18
5₁(973)	→	974
5₁(160)	→	161
5₁(919)	→	920
5₁(192)	→	193
5₁(203)	→	204
5₁(61)	→	62
5₁(335)	→	336
5₁(50)	→	51
5₁(850)	→	851
5₁(320)	→	321
5₁(117)	→	118
5₁(242)	→	243
5₁(304)	→	305
5₁(241)	→	242
5₁(433)	→	434
5₁(339)	→	340
5₁(862)	→	863
5₁(276)	→	277
5₁(155)	→	156
5₁(334)	→	335
5₁(971)	→	972
5₁(273)	→	274
5₁(103)	→	104
5₁(347)	→	348
5₁(298)	→	299
5₁(319)	→	320
5₁(346)	→	347
5₁(31)	→	32
5₁(311)	→	312
5₁(219)	→	220
5₁(292)	→	293
5₁(969)	→	970
5₁(638)	→	639
5₁(345)	→	346
5₁(138)	→	139
5₁(18)	→	19
5₁(262)	→	263
5₁(851)	→	852
5₁(51)	→	52
5₁(64)	→	65
5₁(842)	→	843
5₁(1053)	→	1054
5₁(174)	→	175
5₁(115)	→	116
5₁(434)	→	435
5₁(337)	→	338
5₁(639)	→	640
5₁(838)	→	839
1₁(1033)	→	1034
1₁(935)	→	936
1₁(261)	→	262
1₁(293)	→	294
1₁(229)	→	230
1₁(305)	→	306
1₁(1094)	→	1095
1₁(544)	→	545
1₁(778)	→	779
1₁(349)	→	350
1₁(227)	→	228
1₁(118)	→	119
1₁(205)	→	206
1₁(157)	→	158
1₁(270)	→	271
1₁(169)	→	170
1₁(947)	→	948
1₁(238)	→	239
1₁(939)	→	940
1₁(766)	→	767
1₁(133)	→	134
1₁(237)	→	238
1₁(894)	→	895
1₁(325)	→	326
1₁(1025)	→	1026
1₁(280)	→	281
1₁(915)	→	916
1₁(1067)	→	1068
1₁(213)	→	214
1₁(212)	→	213
1₁(84)	→	85
1₁(127)	→	128
1₁(38)	→	39
1₁(314)	→	315
1₁(989)	→	990
1₁(14)	→	15
1₁(239)	→	240
1₁(279)	→	280
1₁(171)	→	172
1₁(83)	→	84
1₁(784)	→	785
1₁(941)	→	942
1₁(845)	→	846
1₁(231)	→	232
1₁(937)	→	938
1₁(168)	→	169
1₁(296)	→	297
1₁(820)	→	821
1₁(29)	→	30
1₁(785)	→	786
1₁(259)	→	260
1₁(856)	→	857
1₁(134)	→	135
1₁(226)	→	227
1₁(13)	→	14
1₁(234)	→	235
1₁(294)	→	295
1₁(826)	→	827
1₁(900)	→	901
1₁(39)	→	40
1₁(556)	→	557
1₁(207)	→	208
1₁(25)	→	26
1₁(204)	→	205
1₁(81)	→	82
1₁(1027)	→	1028
1₁(141)	→	142
1₁(220)	→	221
0₀(7)	→	7
2₀(7)	→	7
2₁(101)	→	102
2₁(72)	→	73
2₁(164)	→	165
2₁(814)	→	815
2₁(90)	→	91
2₁(917)	→	918
2₁(338)	→	339
2₁(854)	→	855
2₁(263)	→	264
2₁(308)	→	309
2₁(272)	→	273
2₁(902)	→	903
2₁(1088)	→	1089
2₁(24)	→	25
2₁(326)	→	327
2₁(165)	→	166
2₁(783)	→	784
2₁(71)	→	72
2₁(206)	→	207
2₁(12)	→	13
2₁(929)	→	930
2₁(735)	→	736
2₁(107)	→	108
2₁(913)	→	914
2₁(343)	→	344
2₁(151)	→	152
2₁(152)	→	153
2₁(73)	→	74
2₁(812)	→	813
2₁(371)	→	372
2₁(110)	→	111
2₁(274)	→	275
2₁(323)	→	324
2₁(132)	→	133
2₁(562)	→	563
2₁(857)	→	858
2₁(244)	→	245
2₁(208)	→	209
2₁(91)	→	92
2₁(875)	→	876
2₁(770)	→	771
2₁(873)	→	874
2₁(931)	→	932
2₁(45)	→	46
2₁(264)	→	265
2₁(397)	→	398
2₁(111)	→	112
3₁(235)	→	236
3₁(327)	→	328
3₁(26)	→	27
3₁(92)	→	93
3₁(955)	→	956
3₁(40)	→	41
3₁(255)	→	256
3₁(859)	→	860
3₁(328)	→	329
3₁(786)	→	787
3₁(223)	→	224
3₁(781)	→	782
3₁(137)	→	138
3₁(102)	→	103
3₁(313)	→	314
3₁(222)	→	223
3₁(252)	→	253
3₁(858)	→	859
3₁(322)	→	323
3₁(542)	→	543
3₁(269)	→	270
3₁(847)	→	848
3₁(316)	→	317
3₁(85)	→	86
3₁(804)	→	805
3₁(843)	→	844
3₁(844)	→	845
3₁(210)	→	211
3₁(309)	→	310
3₁(79)	→	80
3₁(139)	→	140
3₁(233)	→	234
3₁(312)	→	313
3₁(167)	→	168
3₁(135)	→	136
3₁(846)	→	847
3₁(130)	→	131
3₁(94)	→	95
3₁(256)	→	257
3₁(297)	→	298
3₁(172)	→	173
3₁(197)	→	198
3₁(302)	→	303
3₁(557)	→	558
3₁(202)	→	203
3₁(348)	→	349
3₁(315)	→	316
3₁(853)	→	854
3₁(245)	→	246
3₁(113)	→	114
3₁(195)	→	196
3₁(251)	→	252
3₁(108)	→	109
2₂(981)	→	982
2₂(864)	→	865
2₂(403)	→	404
2₂(975)	→	976
2₂(889)	→	890
2₂(979)	→	980
2₂(389)	→	390
2₂(385)	→	386
2₂(987)	→	988
2₂(983)	→	984
2₂(890)	→	891
2₂(866)	→	867
2₂(985)	→	986
2₂(351)	→	352
2₂(977)	→	978
2₂(1055)	→	1056
2₂(424)	→	425
1₀(7)	→	7
1₂(386)	→	387
1₂(387)	→	388
1₂(426)	→	427
1₂(405)	→	406
1₂(390)	→	391
1₂(891)	→	892
1₂(425)	→	426
1₂(404)	→	405
1₂(352)	→	353
1₂(391)	→	392
1₂(353)	→	354

The automaton is closed under rewriting as it is compatible.