Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/88283)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

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

final states:

{5}

transitions:

1182	→	361
1405	→	1438
1405	→	1489
78	→	1215
1067	→	1467
1206	→	1513
1268	→	151
1268	→	566
1268	→	5
1268	→	243
1268	→	65
1268	→	82
1268	→	946
25	→	200
25	→	1031
1437	→	25
1579	→	58
1496	→	277
202	→	215
1441	→	25
1106	→	246
1406	→	345
1406	→	25
1406	→	555
1406	→	114
1406	→	42
1406	→	24
1406	→	81
1406	→	5
1406	→	134
1406	→	44
81	→	1442
80	→	5
80	→	591
80	→	115
80	→	567
80	→	151
80	→	566
80	→	243
80	→	65
80	→	82
80	→	1105
80	→	245
80	→	499
80	→	1104
80	→	946
80	→	571
80	→	1549
152	→	605
152	→	995
1089	→	1578
214	→	57
286	→	1049
1142	→	403
1354	→	557
401	→	1039
1284	→	472
1046	→	200
448	→	78
781	→	1436
781	→	1487
1435	→	25
1073	→	1054
1209	→	1477
1209	→	1505
608	→	1495
129	→	645
129	→	1389
1544	→	1580
1498	→	58
84	→	1564
998	→	116
1008	→	139
119	→	302
119	→	1568
595	→	1111
145	→	1183
1575	→	200
133	→	1119
1408	→	1391
226	→	179
1118	→	233
41	→	5
41	→	591
41	→	115
41	→	499
41	→	151
41	→	453
41	→	498
41	→	83
41	→	244
41	→	82
41	→	566
41	→	243
41	→	65
41	→	67
41	→	245
41	→	1104
41	→	454
41	→	946
41	→	153
41	→	1032
120	→	1091
120	→	1125
39	→	1127
1506	→	43
499	→	1105
1104	→	245
1565	→	606
213	→	997
146	→	79
1332	→	1317
647	→	1523
5	→	24
5	→	42
5	→	81
5	→	114
59	→	5
59	→	591
59	→	115
59	→	347
59	→	151
59	→	436
59	→	116
59	→	82
59	→	498
59	→	83
59	→	566
59	→	243
59	→	65
59	→	358
59	→	64
59	→	131
59	→	43
59	→	554
59	→	167
59	→	511
59	→	132
59	→	200
59	→	592
59	→	25
59	→	345
59	→	555
59	→	134
59	→	44
59	→	454
59	→	946
59	→	1181
59	→	246
59	→	1106
59	→	945
59	→	117
59	→	1004
59	→	1512
59	→	1443
1276	→	40
1000	→	116
1524	→	391
1126	→	289
65	→	243
65	→	566
1071	→	1054
1048	→	200
1328	→	1483
361	→	378
325	→	40
130	→	40
1110	→	276
1275	→	1497
467	→	1277
1068	→	1440
1068	→	1446
246	→	1181
1403	→	1450
1034	→	131
40	→	765
1443	→	43
1010	→	136
287	→	58
287	→	1001
1040	→	201
1545	→	40
165	→	1033
1112	→	277
1004	→	117
1267	→	1473
1267	→	1554
1066	→	1574
524	→	402
524	→	1072
1478	→	200
1052	→	200
44	→	345
44	→	1175
1278	→	453
1376	→	200
1376	→	5
1376	→	592
1376	→	25
1547	→	557
1329	→	1479
1329	→	1507
179	→	1047
26	→	273
297	→	286
1514	→	43
79	→	1041
79	→	1359
556	→	1009
662	→	591
662	→	114
662	→	42
662	→	24
662	→	81
662	→	5
662	→	115
58	→	663
58	→	1089
512	→	1043
512	→	1548
994	→	83
1402	→	1475
1553	→	591
201	→	466
614	→	210
912	→	591
912	→	114
912	→	42
912	→	24
912	→	81
912	→	5
912	→	115
1176	→	362
346	→	390
346	→	1546
257	→	58
311	→	255
389	→	129
1358	→	567
911	→	1471
911	→	1552
648	→	1109
404	→	5
404	→	151
404	→	566
404	→	243
404	→	65
404	→	82
404	→	358
404	→	64
404	→	131
404	→	43
404	→	946
404	→	945
404	→	117
404	→	1004
404	→	1443
1032	→	153
1042	→	201
1042	→	1217
1092	→	1059
1168	→	43
565	→	509
67	→	1283
82	→	151
82	→	1003
82	→	1103
82	→	453
82	→	498
82	→	114
82	→	42
82	→	24
82	→	81
82	→	5
82	→	83
82	→	244
1490	→	65
1490	→	1562
117	→	945
180	→	57
180	→	999
313	→	1258
118	→	1269
1504	→	58
1174	→	43
604	→	464
400	→	1193
244	→	453
1069	→	151
1069	→	436
1069	→	114
1069	→	42
1069	→	24
1069	→	81
1069	→	5
1069	→	116
1069	→	82
212	→	1045
479	→	39
1451	→	116
66	→	231
66	→	943
359	→	435
1470	→	58
766	→	898
766	→	1037
766	→	1254
373	→	40
93	→	54
357	→	213
1012	→	153
1270	→	312
1555	→	591
1482	→	65
1216	→	1194
1216	→	1275
1216	→	1314
944	→	901
1559	→	605
1044	→	204
1006	→	135
1006	→	1353
1184	→	244
1255	→	359
234	→	288
1563	→	605
1204	→	1481
1207	→	1469
1038	→	167
1038	→	1117
1581	→	58
434	→	323
115	→	591
115	→	1511
1090	→	1054
1090	→	1357
1090	→	1407
1090	→	1544
393	→	1007
1447	→	83
83	→	498
1484	→	65
1512	→	43
946	→	65
510	→	213
1569	→	121
360	→	423
1486	→	65
1486	→	1558
1549	→	571
1439	→	25
242	→	164
168	→	312
398	→	1053
68	→	1289
1476	→	200
664	→	646
664	→	1011
1508	→	43
324	→	1167
1474	→	58
203	→	1331
1266	→	1519
132	→	167
132	→	511
132	→	554
1445	→	43
465	→	57
1290	→	471
1561	→	605
1472	→	58
782	→	591
782	→	114
782	→	42
782	→	24
782	→	81
782	→	5
782	→	115
1120	→	288
1002	→	116
1210	→	151
1210	→	566
1210	→	5
1210	→	243
1210	→	65
1210	→	82
1210	→	946
1520	→	43
1375	→	1434
1375	→	1485
910	→	1517
1518	→	43
1050	→	200
144	→	1070
43	→	64
43	→	131
43	→	358
1480	→	200
1218	→	1195
660	→	1503
767	→	1005
403	→	1051
403	→	1173
576	→	355
166	→	58
166	→	993
1330	→	358
1330	→	64
1330	→	114
1330	→	42
1330	→	24
1330	→	81
1330	→	5
1330	→	131
1330	→	43
1330	→	945
1330	→	117
1330	→	1004
1330	→	1443
1468	→	58
1488	→	65
1488	→	1560
996	→	85
661	→	1444
3₁(51)	→	52
3₁(1560)	→	1561
3₁(1061)	→	1062
3₁(1564)	→	1565
3₁(471)	→	472
3₁(900)	→	901
3₁(31)	→	32
3₁(239)	→	240
3₁(1267)	→	1268
3₁(203)	→	204
3₁(46)	→	47
3₁(1562)	→	1563
3₁(292)	→	293
3₁(387)	→	388
3₁(78)	→	79
3₁(310)	→	311
3₁(372)	→	373
3₁(554)	→	555
3₁(1045)	→	1046
3₁(317)	→	318
3₁(210)	→	211
3₁(1367)	→	1368
3₁(1195)	→	1196
3₁(508)	→	509
3₁(1391)	→	1392
3₁(603)	→	604
3₁(478)	→	479
3₁(910)	→	911
3₁(1181)	→	1182
3₁(454)	→	455
3₁(86)	→	87
3₁(25)	→	26
3₁(1005)	→	1006
3₁(1207)	→	1208
3₁(1477)	→	1478
3₁(1361)	→	1362
3₁(366)	→	367
3₁(766)	→	767
3₁(663)	→	664
3₁(365)	→	366
3₁(1475)	→	1476
3₁(1217)	→	1218
3₁(591)	→	592
3₁(1194)	→	1195
3₁(207)	→	208
3₁(77)	→	78
3₁(307)	→	308
3₁(1371)	→	1372
3₁(1390)	→	1391
3₁(273)	→	274
3₁(24)	→	25
3₁(121)	→	122
3₁(1049)	→	1050
3₁(313)	→	314
3₁(592)	→	593
3₁(520)	→	521
3₁(602)	→	603
3₁(50)	→	51
3₁(256)	→	257
3₁(555)	→	556
3₁(206)	→	207
3₁(134)	→	135
3₁(89)	→	90
3₁(1434)	→	1435
3₁(902)	→	903
3₁(356)	→	357
3₁(506)	→	507
3₁(133)	→	134
3₁(315)	→	316
3₁(1394)	→	1395
3₁(608)	→	609
3₁(652)	→	653
3₁(769)	→	770
3₁(645)	→	646
3₁(1131)	→	1132
3₁(56)	→	57
3₁(68)	→	69
3₁(237)	→	238
3₁(1283)	→	1284
3₁(774)	→	775
3₁(208)	→	209
3₁(314)	→	315
3₁(70)	→	71
3₁(151)	→	152
3₁(773)	→	774
3₁(1206)	→	1207
3₁(83)	→	84
3₁(302)	→	303
3₁(345)	→	346
3₁(779)	→	780
3₁(79)	→	80
3₁(247)	→	248
3₁(204)	→	205
3₁(557)	→	558
3₁(401)	→	402
3₁(1366)	→	1367
3₁(1324)	→	1325
3₁(1436)	→	1437
3₁(284)	→	285
3₁(770)	→	771
3₁(1132)	→	1133
3₁(1440)	→	1441
3₁(1266)	→	1267
3₁(349)	→	350
3₁(220)	→	221
3₁(318)	→	319
3₁(605)	→	606
3₁(1438)	→	1439
3₁(1574)	→	1575
3₁(1400)	→	1401
3₁(124)	→	125
3₁(597)	→	598
3₁(646)	→	647
3₁(160)	→	161
3₁(1407)	→	1408
3₁(43)	→	44
3₁(163)	→	164
3₁(1047)	→	1048
3₁(47)	→	48
3₁(911)	→	912
3₁(1360)	→	1361
3₁(499)	→	500
3₁(1133)	→	1134
3₁(1135)	→	1136
3₁(360)	→	361
3₁(1043)	→	1044
3₁(562)	→	563
3₁(476)	→	477
3₁(909)	→	910
3₁(505)	→	506
3₁(385)	→	386
3₁(400)	→	401
3₁(943)	→	944
3₁(1372)	→	1373
3₁(216)	→	217
3₁(1051)	→	1052
3₁(598)	→	599
3₁(1558)	→	1559
3₁(1479)	→	1480
3₁(153)	→	154
3₁(219)	→	220
3₁(1063)	→	1064
3₁(1136)	→	1137
1₁(82)	→	83
1₁(561)	→	562
1₁(1446)	→	1447
1₁(175)	→	176
1₁(440)	→	441
1₁(120)	→	121
1₁(1089)	→	1090
1₁(388)	→	389
1₁(575)	→	576
1₁(1397)	→	1398
1₁(1072)	→	1073
1₁(152)	→	153
1₁(1259)	→	1260
1₁(205)	→	206
1₁(435)	→	436
1₁(202)	→	203
1₁(361)	→	362
1₁(441)	→	442
1₁(162)	→	163
1₁(395)	→	396
1₁(908)	→	909
1₁(1001)	→	1002
1₁(559)	→	560
1₁(509)	→	510
1₁(1481)	→	1482
1₁(1483)	→	1484
1₁(87)	→	88
1₁(558)	→	559
1₁(477)	→	478
1₁(362)	→	363
1₁(1326)	→	1327
1₁(660)	→	661
1₁(115)	→	116
1₁(136)	→	137
1₁(1389)	→	1390
1₁(1321)	→	1322
1₁(173)	→	174
1₁(997)	→	998
1₁(174)	→	175
1₁(224)	→	225
1₁(517)	→	518
1₁(1175)	→	1176
1₁(76)	→	77
1₁(1111)	→	1112
1₁(254)	→	255
1₁(140)	→	141
1₁(165)	→	166
1₁(611)	→	612
1₁(243)	→	244
1₁(466)	→	467
1₁(993)	→	994
1₁(468)	→	469
1₁(1289)	→	1290
1₁(123)	→	124
1₁(571)	→	572
1₁(453)	→	454
1₁(1060)	→	1061
1₁(1568)	→	1569
1₁(176)	→	177
1₁(1011)	→	1012
1₁(141)	→	142
1₁(457)	→	458
1₁(135)	→	136
1₁(172)	→	173
1₁(1523)	→	1524
1₁(390)	→	391
1₁(1373)	→	1374
1₁(470)	→	471
1₁(1315)	→	1316
1₁(1201)	→	1202
1₁(290)	→	291
1₁(999)	→	1000
1₁(251)	→	252
1₁(444)	→	445
1₁(1009)	→	1010
1₁(347)	→	348
1₁(511)	→	512
1₁(560)	→	561
1₁(27)	→	28
1₁(1450)	→	1451
1₁(217)	→	218
1₁(648)	→	649
1₁(64)	→	65
1₁(507)	→	508
1₁(1067)	→	1068
1₁(945)	→	946
1₁(276)	→	277
1₁(1275)	→	1276
1₁(367)	→	368
1₁(1258)	→	1259
1₁(661)	→	662
1₁(250)	→	251
1₁(236)	→	237
1₁(1277)	→	1278
1₁(456)	→	457
1₁(304)	→	305
1₁(522)	→	523
1₁(1197)	→	1198
1₁(1031)	→	1032
1₁(1196)	→	1197
1₁(66)	→	67
1₁(39)	→	40
1₁(168)	→	169
1₁(1487)	→	1488
1₁(898)	→	899
1₁(355)	→	356
1₁(569)	→	570
1₁(178)	→	179
1₁(1495)	→	1496
1₁(352)	→	353
1₁(1070)	→	1071
1₁(464)	→	465
1₁(1053)	→	1054
1₁(1399)	→	1400
1₁(81)	→	82
1₁(391)	→	392
1₁(613)	→	614
1₁(40)	→	41
1₁(1262)	→	1263
1₁(1489)	→	1490
1₁(1485)	→	1486
1₁(1544)	→	1545
0₁(295)	→	296
0₁(114)	→	115
0₁(244)	→	245
0₁(280)	→	281
0₁(346)	→	347
0₁(73)	→	74
0₁(225)	→	226
0₁(170)	→	171
0₁(653)	→	654
0₁(459)	→	460
0₁(1402)	→	1403
0₁(513)	→	514
0₁(279)	→	280
0₁(655)	→	656
0₁(518)	→	519
0₁(30)	→	31
0₁(1329)	→	1330
0₁(1317)	→	1318
0₁(159)	→	160
0₁(1365)	→	1366
0₁(1260)	→	1261
0₁(212)	→	213
0₁(322)	→	323
0₁(394)	→	395
0₁(519)	→	520
0₁(293)	→	294
0₁(905)	→	906
0₁(383)	→	384
0₁(1323)	→	1324
0₁(179)	→	180
0₁(498)	→	499
0₁(34)	→	35
0₁(382)	→	383
0₁(386)	→	387
0₁(358)	→	359
0₁(574)	→	575
0₁(32)	→	33
0₁(778)	→	779
0₁(500)	→	501
0₁(167)	→	168
0₁(1359)	→	1360
0₁(566)	→	567
0₁(515)	→	516
0₁(1103)	→	1104
0₁(1269)	→	1270
0₁(1357)	→	1358
0₁(1140)	→	1141
0₁(403)	→	404
0₁(393)	→	394
0₁(1129)	→	1130
0₁(92)	→	93
0₁(323)	→	324
0₁(55)	→	56
0₁(1254)	→	1255
0₁(1062)	→	1063
0₁(282)	→	283
0₁(1200)	→	1201
0₁(238)	→	239
0₁(370)	→	371
0₁(1209)	→	1210
0₁(1548)	→	1549
0₁(249)	→	250
0₁(570)	→	571
0₁(1141)	→	1142
0₁(164)	→	165
0₁(286)	→	287
0₁(324)	→	325
0₁(399)	→	400
0₁(288)	→	289
0₁(308)	→	309
0₁(429)	→	430
0₁(777)	→	778
0₁(145)	→	146
0₁(430)	→	431
0₁(1125)	→	1126
0₁(54)	→	55
0₁(463)	→	464
0₁(248)	→	249
0₁(564)	→	565
0₁(651)	→	652
0₁(1552)	→	1553
0₁(72)	→	73
0₁(460)	→	461
0₁(127)	→	128
0₁(1554)	→	1555
0₁(1199)	→	1200
0₁(596)	→	597
0₁(215)	→	216
0₁(1319)	→	1320
0₁(438)	→	439
0₁(384)	→	385
0₁(904)	→	905
0₁(1066)	→	1067
0₁(442)	→	443
0₁(1322)	→	1323
0₁(775)	→	776
0₁(296)	→	297
0₁(291)	→	292
0₁(573)	→	574
0₁(157)	→	158
0₁(431)	→	432
0₁(473)	→	474
0₁(1205)	→	1206
0₁(52)	→	53
0₀(5)	→	5
1₀(5)	→	5
3₀(5)	→	5
2₁(1396)	→	1397
2₁(1393)	→	1394
2₁(1056)	→	1057
2₁(1511)	→	1512
2₁(397)	→	398
2₁(443)	→	444
2₁(1068)	→	1069
2₁(514)	→	515
2₁(1109)	→	1110
2₁(501)	→	502
2₁(1204)	→	1205
2₁(563)	→	564
2₁(516)	→	517
2₁(274)	→	275
2₁(475)	→	476
2₁(177)	→	178
2₁(899)	→	900
2₁(28)	→	29
2₁(1517)	→	1518
2₁(424)	→	425
2₁(156)	→	157
2₁(275)	→	276
2₁(472)	→	473
2₁(117)	→	118
2₁(1369)	→	1370
2₁(91)	→	92
2₁(1316)	→	1317
2₁(425)	→	426
2₁(1578)	→	1579
2₁(363)	→	364
2₁(306)	→	307
2₁(1374)	→	1375
2₁(371)	→	372
2₁(90)	→	91
2₁(351)	→	352
2₁(65)	→	66
2₁(1105)	→	1106
2₁(657)	→	658
2₁(128)	→	129
2₁(1395)	→	1396
2₁(1127)	→	1128
2₁(49)	→	50
2₁(398)	→	399
2₁(1203)	→	1204
2₁(1091)	→	1092
2₁(359)	→	360
2₁(353)	→	354
2₁(568)	→	569
2₁(1003)	→	1004
2₁(277)	→	278
2₁(364)	→	365
2₁(213)	→	214
2₁(48)	→	49
2₁(1328)	→	1329
2₁(67)	→	68
2₁(246)	→	247
2₁(378)	→	379
2₁(380)	→	381
2₁(649)	→	650
2₁(901)	→	902
2₁(1505)	→	1506
2₁(309)	→	310
2₁(593)	→	594
2₁(232)	→	233
2₁(907)	→	908
2₁(252)	→	253
2₁(255)	→	256
2₁(1193)	→	1194
2₁(1331)	→	1332
2₁(1058)	→	1059
2₁(350)	→	351
2₁(303)	→	304
2₁(348)	→	349
2₁(36)	→	37
2₁(1497)	→	1498
2₁(1033)	→	1034
2₁(1513)	→	1514
2₁(654)	→	655
2₁(235)	→	236
2₁(572)	→	573
2₁(1404)	→	1405
2₁(768)	→	769
2₁(294)	→	295
2₁(131)	→	132
2₁(71)	→	72
2₁(1261)	→	1262
2₁(1167)	→	1168
2₁(1368)	→	1369
2₁(1208)	→	1209
2₁(772)	→	773
2₁(1117)	→	1118
2₁(1405)	→	1406
2₁(1320)	→	1321
2₁(423)	→	424
2₁(233)	→	234
2₁(26)	→	27
2₁(37)	→	38
2₁(234)	→	235
2₁(647)	→	648
2₁(436)	→	437
2₁(222)	→	223
2₁(771)	→	772
2₁(1403)	→	1404
2₁(155)	→	156
2₁(1173)	→	1174
2₁(402)	→	403
2₁(1138)	→	1139
2₁(138)	→	139
2₁(433)	→	434
2₁(469)	→	470
2₁(74)	→	75
2₁(38)	→	39
2₁(281)	→	282
2₁(223)	→	224
2₁(594)	→	595
2₁(84)	→	85
2₁(1507)	→	1508
2₁(1469)	→	1470
2₁(218)	→	219
2₁(211)	→	212
2₁(461)	→	462
2₁(245)	→	246
2₁(1546)	→	1547
2₁(118)	→	119
2₁(600)	→	601
2₁(53)	→	54
2₁(1139)	→	1140
2₁(512)	→	513
2₁(320)	→	321
2₁(1057)	→	1058
2₁(1442)	→	1443
2₁(132)	→	133
2₁(125)	→	126
2₁(316)	→	317
2₁(379)	→	380
2₁(221)	→	222
2₁(241)	→	242
2₁(658)	→	659
2₁(1580)	→	1581
2₁(1327)	→	1328
2₁(599)	→	600
2₁(995)	→	996
2₁(161)	→	162
2₁(1064)	→	1065
2₁(139)	→	140
2₁(305)	→	306
2₁(610)	→	611
2₁(474)	→	475
2₁(29)	→	30
2₁(1318)	→	1319
2₁(1055)	→	1056
2₁(137)	→	138
2₁(656)	→	657
2₁(1392)	→	1393
2₁(312)	→	313
2₁(33)	→	34
2₁(523)	→	524
2₁(767)	→	768
2₁(906)	→	907
2₁(595)	→	596
2₁(1065)	→	1066
2₁(439)	→	440
2₁(609)	→	610
2₁(612)	→	613
2₁(503)	→	504
2₁(35)	→	36
2₁(240)	→	241
2₁(45)	→	46
2₁(129)	→	130
2₁(455)	→	456
2₁(1198)	→	1199
2₁(765)	→	766
2₁(1362)	→	1363
2₁(42)	→	43
2₁(75)	→	76
2₁(369)	→	370
2₁(650)	→	651
2₁(1264)	→	1265
2₁(1263)	→	1264
2₁(85)	→	86
2₁(426)	→	427
2₁(1398)	→	1399
2₁(201)	→	202
2₁(319)	→	320
2₁(381)	→	382
2₁(607)	→	608
2₁(1130)	→	1131
2₁(126)	→	127
2₁(289)	→	290
2₁(437)	→	438
2₁(1119)	→	1120
2₁(1370)	→	1371
2₁(1137)	→	1138
2₁(57)	→	58
2₁(143)	→	144
2₁(368)	→	369
2₁(428)	→	429
2₁(447)	→	448
2₁(396)	→	397
2₁(321)	→	322
2₁(154)	→	155
2₁(1183)	→	1184
2₁(354)	→	355
2₁(462)	→	463
2₁(142)	→	143
2₁(556)	→	557
2₁(209)	→	210
2₁(1039)	→	1040
2₁(659)	→	660
2₁(278)	→	279
2₁(1325)	→	1326
2₁(1041)	→	1042
2₁(1314)	→	1315
2₁(1473)	→	1474
2₁(781)	→	782
2₁(44)	→	45
2₁(253)	→	254
2₁(285)	→	286
2₁(502)	→	503
2₁(1215)	→	1216
2₁(458)	→	459
2₁(58)	→	59
2₁(1202)	→	1203
2₁(144)	→	145
2₁(231)	→	232
2₁(776)	→	777
2₁(467)	→	468
2₁(1054)	→	1055
2₁(1265)	→	1266
2₁(283)	→	284
2₁(1401)	→	1402
2₁(392)	→	393
2₁(1059)	→	1060
2₁(780)	→	781
2₁(1363)	→	1364
2₁(1503)	→	1504
2₁(1467)	→	1468
2₁(1364)	→	1365
2₁(200)	→	201
2₁(903)	→	904
2₁(88)	→	89
2₁(1353)	→	1354
2₁(1519)	→	1520
2₁(1007)	→	1008
2₁(169)	→	170
2₁(1134)	→	1135
2₁(446)	→	447
2₁(158)	→	159
2₁(445)	→	446
2₁(606)	→	607
2₁(1037)	→	1038
2₁(116)	→	117
2₁(1471)	→	1472
2₁(427)	→	428
2₁(432)	→	433
2₁(1128)	→	1129
2₁(122)	→	123
2₁(1375)	→	1376
2₁(119)	→	120
2₁(521)	→	522
2₁(1444)	→	1445
2₁(504)	→	505
2₁(171)	→	172
2₁(69)	→	70
2₁(601)	→	602
2₁(567)	→	568
2₀(5)	→	5

The automaton is closed under rewriting as it is compatible.