Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4840)

The rewrite relation of the following TRS is considered.

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

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:

272	→	833
272	→	897
223	→	196
223	→	594
279	→	1026
1151	→	298
867	→	1092
280	→	1
280	→	518
280	→	445
280	→	124
280	→	471
176	→	122
176	→	224
534	→	885
964	→	1065
964	→	1127
964	→	1133
917	→	537
1056	→	651
809	→	796
10	→	112
1169	→	222
387	→	363
537	→	723
743	→	732
561	→	1
561	→	518
561	→	445
561	→	469
578	→	305
886	→	371
374	→	363
560	→	692
560	→	769
560	→	812
471	→	445
326	→	298
371	→	694
371	→	763
371	→	808
728	→	551
84	→	472
1008	→	574
811	→	796
436	→	545
119	→	1030
122	→	246
122	→	501
122	→	527
299	→	481
299	→	553
299	→	562
299	→	1032
878	→	870
610	→	595
638	→	627
638	→	916
585	→	451
18	→	1
18	→	518
18	→	445
18	→	123
18	→	465
469	→	445
365	→	903
1118	→	124
41	→	9
41	→	466
41	→	388
41	→	121
41	→	8
41	→	343
41	→	422
41	→	5
41	→	66
41	→	587
41	→	1012
41	→	651
41	→	1050
41	→	1056
120	→	2
120	→	527
120	→	246
120	→	122
120	→	174
120	→	222
120	→	153
120	→	224
120	→	176
120	→	1171
120	→	1087
3	→	63
3	→	173
3	→	345
3	→	373
3	→	424
3	→	454
1079	→	122
772	→	831
691	→	527
691	→	246
691	→	2
691	→	122
691	→	174
1033	→	613
225	→	196
225	→	605
907	→	618
1062	→	9
805	→	527
805	→	246
805	→	122
805	→	464
805	→	386
805	→	193
805	→	81
805	→	327
805	→	420
805	→	2
805	→	224
805	→	176
805	→	1087
919	→	537
9	→	83
9	→	271
9	→	536
9	→	579
5	→	8
5	→	121
5	→	343
5	→	388
5	→	422
5	→	466
931	→	1059
931	→	1119
931	→	1164
443	→	5
443	→	579
443	→	271
443	→	9
443	→	64
592	→	806
1126	→	298
1124	→	298
1027	→	1014
618	→	1028
1134	→	406
813	→	796
130	→	119
1095	→	272
892	→	371
193	→	1061
193	→	1123
193	→	1146
1031	→	1014
445	→	509
445	→	518
446	→	1007
467	→	445
1159	→	298
1132	→	363
1	→	40
1	→	152
1	→	307
1	→	403
1	→	416
1	→	470
40	→	1170
1010	→	580
840	→	579
840	→	271
840	→	9
840	→	466
840	→	388
840	→	121
840	→	8
840	→	343
840	→	422
840	→	5
840	→	64
690	→	1168
695	→	682
695	→	924
1022	→	1034
1022	→	1057
1022	→	1078
1022	→	1150
1081	→	122
1066	→	9
601	→	626
601	→	661
601	→	719
601	→	869
570	→	2
570	→	527
570	→	246
570	→	122
570	→	174
778	→	305
965	→	518
965	→	445
965	→	470
965	→	403
965	→	152
965	→	40
965	→	307
965	→	416
965	→	1
965	→	469
770	→	298
1052	→	651
1130	→	363
884	→	371
480	→	4
480	→	404
1029	→	1014
606	→	595
402	→	363
1064	→	9
488	→	637
488	→	650
488	→	721
488	→	877
634	→	1090
423	→	406
1161	→	371
91	→	781
662	→	651
868	→	403
760	→	518
760	→	445
760	→	1
760	→	124
760	→	471
619	→	4
619	→	404
552	→	1
552	→	518
552	→	572
552	→	11
552	→	509
552	→	445
552	→	653
407	→	586
346	→	298
526	→	488
389	→	363
839	→	1063
839	→	1125
839	→	1148
6	→	42
6	→	154
6	→	297
6	→	401
6	→	405
6	→	468
404	→	363
404	→	4
404	→	519
627	→	918
153	→	122
153	→	222
741	→	423
741	→	3
741	→	580
1037	→	9
308	→	298
308	→	1005
455	→	445
174	→	122
363	→	426
363	→	571
363	→	1011
764	→	298
270	→	3
270	→	423
270	→	580
270	→	421
270	→	419
270	→	1147
204	→	5
204	→	579
204	→	271
204	→	9
204	→	66
204	→	64
204	→	587
204	→	1012
204	→	651
204	→	1050
204	→	1056
525	→	1013
82	→	9
803	→	1160
859	→	448
2	→	81
2	→	193
2	→	327
2	→	386
2	→	420
2	→	464
1060	→	83
1060	→	1094
1060	→	1166
4	→	65
4	→	175
4	→	325
4	→	362
4	→	418
4	→	444
528	→	611
804	→	1129
344	→	298
876	→	413
604	→	595
419	→	406
419	→	3
419	→	113
478	→	742
1035	→	9
425	→	406
593	→	479
508	→	268
66	→	9
16	→	731
602	→	4
602	→	404
766	→	298
421	→	406
421	→	454
421	→	373
421	→	173
421	→	63
421	→	345
421	→	424
421	→	3
516	→	795
535	→	91
306	→	119
1012	→	587
636	→	518
636	→	445
636	→	1
636	→	465
12	→	957
720	→	122
1177	→	222
759	→	1176
1091	→	195
1006	→	574
417	→	406
64	→	9
453	→	203
434	→	414
529	→	858
414	→	771
198	→	264
1128	→	298
1025	→	1014
245	→	196
245	→	603
1149	→	406
664	→	751
664	→	1009
464	→	1131
832	→	427
413	→	883
517	→	269
1153	→	298
1087	→	122
693	→	682
203	→	1024
722	→	122
1093	→	195
1058	→	651
489	→	3
489	→	406
489	→	421
489	→	419
489	→	1147
465	→	445
465	→	470
465	→	403
465	→	152
465	→	40
465	→	307
465	→	416
465	→	1
465	→	455
670	→	568
782	→	772
1120	→	1109
1165	→	371
92	→	1
92	→	518
92	→	445
92	→	455
92	→	471
932	→	518
932	→	572
932	→	1
932	→	11
932	→	509
932	→	445
932	→	653
1002	→	527
1002	→	246
1002	→	2
1002	→	122
1002	→	174
574	→	995
807	→	796
1171	→	222
328	→	298
1050	→	9
43	→	9
418	→	1049
418	→	1055
418	→	1086
418	→	1158
372	→	2
372	→	194
372	→	502
372	→	1081
660	→	123
194	→	122
194	→	244
194	→	2
551	→	663
551	→	891
551	→	1108
544	→	91
442	→	681
442	→	765
442	→	810
1167	→	580
682	→	860
1023	→	404
155	→	122
155	→	195
1147	→	406
415	→	2
415	→	527
415	→	246
415	→	122
415	→	224
415	→	176
415	→	1087
247	→	196
247	→	609
196	→	435
420	→	1036
420	→	1051
420	→	1080
420	→	1152
898	→	512
1₁(123)	→	124
1₁(521)	→	522
1₁(117)	→	118
1₁(545)	→	546
1₁(487)	→	488
1₁(563)	→	564
1₁(538)	→	539
1₁(10)	→	11
1₁(88)	→	89
1₁(466)	→	467
1₁(777)	→	778
1₁(468)	→	469
1₁(91)	→	92
1₁(274)	→	275
1₁(688)	→	689
1₁(513)	→	514
1₁(303)	→	304
1₁(596)	→	597
1₁(412)	→	413
1₁(667)	→	668
1₁(86)	→	87
1₁(122)	→	123
1₁(754)	→	755
1₁(995)	→	996
1₁(571)	→	572
1₁(589)	→	590
1₁(470)	→	471
1₁(524)	→	525
1₁(427)	→	428
1₁(903)	→	904
1₁(414)	→	415
1₁(906)	→	907
1₁(464)	→	465
1₁(925)	→	926
1₁(628)	→	629
1₁(444)	→	445
1₁(454)	→	455
1₁(368)	→	369
1₁(1032)	→	1033
1₁(669)	→	670
1₁(612)	→	613
1₁(584)	→	585
1₁(804)	→	805
1₁(1017)	→	1018
1₁(542)	→	543
1₁(575)	→	576
1₁(802)	→	803
1₂(652)	→	653
1₂(1112)	→	1113
4₂(659)	→	660
4₂(651)	→	652
4₂(654)	→	655
4₂(1114)	→	1115
0₂(1116)	→	1117
0₂(1111)	→	1112
0₂(658)	→	659
4₁(1001)	→	1002
4₁(429)	→	430
4₁(373)	→	374
4₁(269)	→	270
4₁(528)	→	529
4₁(926)	→	927
4₁(514)	→	515
4₁(431)	→	432
4₁(128)	→	129
4₁(449)	→	450
4₁(1021)	→	1022
4₁(569)	→	570
4₁(406)	→	407
4₁(407)	→	408
4₁(635)	→	636
4₁(682)	→	683
4₁(511)	→	512
4₁(475)	→	476
4₁(9)	→	10
4₁(126)	→	127
4₁(276)	→	277
4₁(533)	→	534
4₁(594)	→	595
4₁(114)	→	115
4₁(603)	→	604
4₁(386)	→	387
4₁(401)	→	402
4₁(960)	→	961
4₁(831)	→	832
4₁(90)	→	91
4₁(506)	→	507
4₁(388)	→	389
4₁(756)	→	757
4₁(798)	→	799
4₁(605)	→	606
4₁(426)	→	427
4₁(268)	→	269
4₁(530)	→	531
4₁(446)	→	447
4₁(556)	→	557
4₁(685)	→	686
4₁(771)	→	772
4₁(1129)	→	1130
4₁(600)	→	601
4₁(441)	→	442
4₁(450)	→	451
4₁(85)	→	86
4₁(305)	→	306
4₁(12)	→	13
4₁(630)	→	631
4₁(865)	→	866
4₁(539)	→	540
4₁(1131)	→	1132
4₁(362)	→	363
4₁(476)	→	477
4₁(304)	→	305
4₁(897)	→	898
4₁(546)	→	547
4₁(403)	→	404
4₁(474)	→	475
4₁(479)	→	480
4₁(408)	→	409
4₁(740)	→	741
4₁(518)	→	519
4₁(781)	→	782
4₁(537)	→	538
4₁(627)	→	628
4₁(1015)	→	1016
4₁(532)	→	533
4₁(838)	→	839
4₁(796)	→	797
4₁(369)	→	370
4₁(609)	→	610
4₁(582)	→	583
4₁(864)	→	865
4₁(17)	→	18
4₁(863)	→	864
4₁(666)	→	667
4₁(797)	→	798
4₁(739)	→	740
3₀(3)	→	5
3₀(6)	→	5
3₀(5)	→	5
3₀(4)	→	5
3₀(2)	→	5
3₀(1)	→	5
5₀(2)	→	6
5₀(6)	→	6
5₀(4)	→	6
5₀(1)	→	6
5₀(3)	→	6
5₀(5)	→	6
2₂(1113)	→	1114
2₂(1110)	→	1111
4₀(1)	→	4
4₀(6)	→	4
4₀(3)	→	4
4₀(5)	→	4
4₀(2)	→	4
4₀(4)	→	4
3₁(87)	→	88
3₁(690)	→	691
3₁(125)	→	126
3₁(866)	→	867
3₁(573)	→	574
3₁(1014)	→	1015
3₁(42)	→	43
3₁(617)	→	618
3₁(694)	→	695
3₁(626)	→	627
3₁(246)	→	247
3₁(599)	→	600
3₁(8)	→	9
3₁(201)	→	202
3₁(614)	→	615
3₁(1020)	→	1021
3₁(244)	→	245
3₁(1063)	→	1064
3₁(692)	→	693
3₁(279)	→	280
3₁(1065)	→	1066
3₁(430)	→	431
3₁(203)	→	204
3₁(507)	→	508
3₁(63)	→	64
3₁(222)	→	223
3₁(689)	→	690
3₁(370)	→	371
3₁(124)	→	125
3₁(928)	→	929
3₁(663)	→	664
3₁(510)	→	511
3₁(564)	→	565
3₁(198)	→	199
3₁(1000)	→	1001
3₁(1007)	→	1008
3₁(586)	→	587
3₁(428)	→	429
3₁(522)	→	523
3₁(509)	→	510
3₁(1061)	→	1062
3₁(433)	→	434
3₁(505)	→	506
3₁(1094)	→	1095
3₁(543)	→	544
3₁(411)	→	412
3₁(472)	→	473
3₁(583)	→	584
3₁(118)	→	119
3₁(681)	→	682
3₁(736)	→	737
3₁(89)	→	90
3₁(15)	→	16
3₁(438)	→	439
3₁(904)	→	905
3₁(996)	→	997
3₁(568)	→	569
3₁(271)	→	272
3₁(119)	→	120
3₁(14)	→	15
3₁(40)	→	41
3₁(618)	→	619
3₁(1005)	→	1006
3₁(1034)	→	1035
3₁(580)	→	581
3₁(835)	→	836
3₁(224)	→	225
3₁(724)	→	725
3₁(65)	→	66
3₁(81)	→	82
3₁(799)	→	800
3₁(1059)	→	1060
3₁(195)	→	196
3₁(302)	→	303
3₁(484)	→	485
3₁(548)	→	549
3₁(929)	→	930
3₁(759)	→	760
3₁(874)	→	875
3₁(503)	→	504
3₁(581)	→	582
3₁(633)	→	634
3₁(668)	→	669
3₁(727)	→	728
3₁(924)	→	925
3₁(549)	→	550
3₁(199)	→	200
3₁(531)	→	532
3₁(615)	→	616
3₁(1049)	→	1050
3₁(637)	→	638
3₁(999)	→	1000
3₁(861)	→	862
3₁(725)	→	726
3₁(409)	→	410
3₁(435)	→	436
3₁(265)	→	266
3₁(751)	→	752
3₁(732)	→	733
3₁(632)	→	633
3₁(590)	→	591
3₁(477)	→	478
3₁(525)	→	526
3₁(1011)	→	1012
3₁(567)	→	568
3₁(1036)	→	1037
3₁(540)	→	541
3₁(801)	→	802
3₁(562)	→	563
2₁(962)	→	963
2₁(742)	→	743
2₁(121)	→	122
2₁(275)	→	276
2₁(927)	→	928
2₁(366)	→	367
2₁(860)	→	861
2₁(410)	→	411
2₁(1090)	→	1091
2₁(266)	→	267
2₁(1024)	→	1025
2₁(592)	→	593
2₁(687)	→	688
2₁(197)	→	198
2₁(872)	→	873
2₁(959)	→	960
2₁(193)	→	194
2₁(152)	→	153
2₁(883)	→	884
2₁(175)	→	176
2₁(735)	→	736
2₁(862)	→	863
2₁(442)	→	443
2₁(800)	→	801
2₁(173)	→	174
2₁(686)	→	687
2₁(555)	→	556
2₁(365)	→	366
2₁(1078)	→	1079
2₁(964)	→	965
2₁(558)	→	559
2₁(591)	→	592
2₁(731)	→	732
2₁(547)	→	548
2₁(734)	→	735
2₁(891)	→	892
2₁(737)	→	738
2₁(755)	→	756
2₁(504)	→	505
2₁(364)	→	365
2₁(775)	→	776
2₁(447)	→	448
2₁(560)	→	561
2₁(1168)	→	1169
2₁(719)	→	720
2₁(300)	→	301
2₁(83)	→	84
2₁(1080)	→	1081
2₁(299)	→	300
2₁(664)	→	665
2₁(473)	→	474
2₁(723)	→	724
2₁(452)	→	453
2₁(774)	→	775
2₁(520)	→	521
2₁(721)	→	722
2₁(839)	→	840
2₁(371)	→	372
2₁(1164)	→	1165
2₁(116)	→	117
2₁(264)	→	265
2₁(1160)	→	1161
2₁(1092)	→	1093
2₁(858)	→	859
2₁(1086)	→	1087
2₁(1028)	→	1029
2₁(752)	→	753
2₁(1176)	→	1177
2₁(115)	→	116
2₁(272)	→	273
2₁(1170)	→	1171
2₁(1030)	→	1031
2₁(501)	→	502
2₁(1026)	→	1027
2₁(1013)	→	1014
2₁(482)	→	483
2₁(451)	→	452
2₁(616)	→	617
2₁(154)	→	155
2₁(516)	→	517
2₁(301)	→	302
2₁(440)	→	441
2₁(773)	→	774
2₁(885)	→	886
2₁(837)	→	838
2₀(3)	→	2
2₀(5)	→	2
2₀(2)	→	2
2₀(4)	→	2
2₀(1)	→	2
2₀(6)	→	2
0₀(2)	→	3
0₀(4)	→	3
0₀(3)	→	3
0₀(6)	→	3
0₀(1)	→	3
0₀(5)	→	3
5₁(916)	→	917
5₁(534)	→	535
5₁(574)	→	575
5₁(918)	→	919
5₁(437)	→	438
5₁(127)	→	128
5₁(565)	→	566
5₁(523)	→	524
5₁(595)	→	596
5₁(481)	→	482
5₁(1125)	→	1126
5₁(776)	→	777
5₁(345)	→	346
5₁(541)	→	542
5₁(1150)	→	1151
5₁(129)	→	130
5₁(277)	→	278
5₁(684)	→	685
5₁(834)	→	835
5₁(13)	→	14
5₁(765)	→	766
5₁(413)	→	414
5₁(432)	→	433
5₁(1016)	→	1017
5₁(483)	→	484
5₁(557)	→	558
5₁(367)	→	368
5₁(803)	→	804
5₁(1152)	→	1153
5₁(733)	→	734
5₁(871)	→	872
5₁(536)	→	537
5₁(325)	→	326
5₁(1123)	→	1124
5₁(869)	→	870
5₁(445)	→	446
5₁(529)	→	530
5₁(527)	→	528
5₁(566)	→	567
5₁(84)	→	85
5₁(997)	→	998
5₁(343)	→	344
5₁(297)	→	298
5₁(196)	→	197
5₁(202)	→	203
5₁(559)	→	560
5₁(611)	→	612
5₁(772)	→	773
5₁(629)	→	630
5₁(763)	→	764
5₁(961)	→	962
5₁(631)	→	632
5₁(439)	→	440
5₁(485)	→	486
5₁(519)	→	520
5₁(327)	→	328
5₁(11)	→	12
5₁(113)	→	114
5₁(577)	→	578
5₁(963)	→	964
5₁(1127)	→	1128
5₁(515)	→	516
5₁(769)	→	770
5₁(757)	→	758
5₁(298)	→	299
5₁(576)	→	577
5₁(875)	→	876
5₁(836)	→	837
5₁(877)	→	878
5₁(870)	→	871
5₁(1158)	→	1159
5₁(873)	→	874
5₁(931)	→	932
5₁(448)	→	449
5₁(551)	→	552
5₁(905)	→	906
5₁(998)	→	999
5₁(572)	→	573
5₁(363)	→	364
5₁(486)	→	487
5₁(665)	→	666
5₁(307)	→	308
0₁(267)	→	268
0₁(1019)	→	1020
0₁(930)	→	931
0₁(418)	→	419
0₁(795)	→	796
0₁(1009)	→	1010
0₁(512)	→	513
0₁(478)	→	479
0₁(867)	→	868
0₁(488)	→	489
0₁(16)	→	17
0₁(683)	→	684
0₁(597)	→	598
0₁(1018)	→	1019
0₁(420)	→	421
0₁(1133)	→	1134
0₁(806)	→	807
0₁(550)	→	551
0₁(601)	→	602
0₁(1022)	→	1023
0₁(422)	→	423
0₁(502)	→	503
0₁(753)	→	754
0₁(1166)	→	1167
0₁(958)	→	959
0₁(613)	→	614
0₁(738)	→	739
0₁(588)	→	589
0₁(598)	→	599
0₁(579)	→	580
0₁(112)	→	113
0₁(1146)	→	1147
0₁(273)	→	274
0₁(278)	→	279
0₁(1148)	→	1149
0₁(405)	→	406
0₁(587)	→	588
0₁(810)	→	811
0₁(957)	→	958
0₁(758)	→	759
0₁(726)	→	727
0₁(554)	→	555
0₁(200)	→	201
0₁(553)	→	554
0₁(436)	→	437
0₁(634)	→	635
0₁(416)	→	417
0₁(833)	→	834
0₁(812)	→	813
0₁(808)	→	809
0₁(424)	→	425
5₂(1115)	→	1116
5₂(655)	→	656
5₂(653)	→	654
1₀(1)	→	1
1₀(6)	→	1
1₀(5)	→	1
1₀(2)	→	1
1₀(3)	→	1
1₀(4)	→	1
3₂(661)	→	662
3₂(1057)	→	1058
3₂(1055)	→	1056
3₂(1051)	→	1052
3₂(657)	→	658
3₂(1119)	→	1120
3₂(650)	→	651
3₂(656)	→	657
3₂(1117)	→	1118
3₂(1109)	→	1110
3₂(1108)	→	1109

The automaton is closed under rewriting as it is compatible.