Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/63142)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Closure Under Flat Contexts

{0(☐), 1(☐), 2(☐)}

1.1 Semantic Labeling

Root-labeling is applied.

There are 123 ruless (increase limit for explicit display).

1.1.1 Bounds

• final states:

  {10}

• transitions:

  78	→	491
  1198	→	29
  1198	→	1270
  223	→	266
  1206	→	53
  1197	→	1290
  314	→	523
  157	→	10
  157	→	406
  157	→	282
  157	→	85
  157	→	328
  157	→	172
  157	→	48
  157	→	33
  111	→	521
  111	→	946
  1301	→	55
  457	→	1059
  315	→	1010
  29	→	1109
  89	→	1155
  745	→	1032
  454	→	10
  454	→	221
  454	→	139
  454	→	119
  454	→	120
  454	→	1150
  1106	→	118
  967	→	235
  87	→	374
  1156	→	337
  152	→	1089
  98	→	69
  98	→	972
  214	→	10
  214	→	188
  214	→	32
  1072	→	29
  1072	→	1165
  1007	→	320
  10	→	29
  10	→	47
  10	→	53
  10	→	117
  10	→	132
  10	→	138
  10	→	170
  10	→	187
  10	→	193
  1166	→	55
  742	→	1207
  1261	→	55
  97	→	976
  1199	→	1292
  743	→	1163
  743	→	1215
  640	→	29
  640	→	1063
  96	→	1071
  383	→	1020
  1073	→	1227
  471	→	1103
  326	→	185
  1195	→	1280
  84	→	1107
  472	→	456
  511	→	1075
  119	→	697
  119	→	1108
  119	→	1110
  119	→	1118
  276	→	964
  1160	→	45
  466	→	418
  668	→	29
  668	→	1065
  133	→	118
  1158	→	138
  1172	→	55
  610	→	233
  610	→	196
  610	→	10
  610	→	283
  610	→	140
  610	→	118
  610	→	101
  610	→	331
  610	→	1110
  610	→	1108
  491	→	1123
  1230	→	118
  1118	→	118
  120	→	221
  955	→	118
  1079	→	1189
  1104	→	118
  57	→	774
  1003	→	196
  382	→	1087
  382	→	1201
  1033	→	30
  1102	→	118
  1011	→	367
  1114	→	118
  1226	→	118
  1074	→	29
  1074	→	1167
  646	→	45
  411	→	948
  1200	→	29
  1200	→	1274
  341	→	185
  341	→	966
  515	→	591
  515	→	609
  1190	→	29
  1190	→	1262
  1276	→	1308
  110	→	499
  110	→	954
  592	→	87
  592	→	31
  592	→	10
  592	→	171
  592	→	407
  698	→	122
  698	→	958
  1076	→	29
  1076	→	1171
  1126	→	118
  1124	→	118
  1071	→	1221
  275	→	639
  275	→	731
  456	→	645
  456	→	1002
  692	→	119
  947	→	196
  947	→	956
  175	→	968
  973	→	252
  130	→	667
  1082	→	53
  1110	→	118
  1275	→	55
  1238	→	118
  1159	→	1211
  1068	→	55
  31	→	55
  31	→	327
  31	→	188
  31	→	32
  1164	→	55
  1132	→	118
  1162	→	45
  246	→	97
  1034	→	1223
  1077	→	1237
  1078	→	29
  1078	→	1173
  1019	→	45
  1009	→	363
  71	→	10
  71	→	406
  71	→	99
  71	→	100
  71	→	86
  71	→	282
  71	→	85
  71	→	328
  71	→	172
  71	→	48
  71	→	54
  71	→	197
  71	→	141
  71	→	174
  71	→	33
  71	→	35
  71	→	57
  71	→	332
  71	→	376
  690	→	123
  1299	→	55
  165	→	10
  165	→	233
  165	→	196
  165	→	236
  165	→	173
  165	→	140
  165	→	118
  165	→	133
  165	→	56
  645	→	1095
  1081	→	1195
  977	→	118
  1112	→	118
  667	→	1125
  895	→	233
  895	→	196
  895	→	236
  895	→	193
  895	→	170
  895	→	132
  895	→	53
  895	→	29
  895	→	47
  895	→	117
  895	→	138
  895	→	187
  895	→	10
  895	→	173
  895	→	140
  895	→	118
  895	→	1108
  895	→	1110
  1066	→	55
  969	→	239
  570	→	55
  222	→	689
  101	→	133
  101	→	56
  101	→	375
  101	→	1118
  524	→	504
  965	→	118
  1228	→	118
  490	→	30
  197	→	296
  197	→	974
  139	→	118
  1130	→	118
  747	→	406
  747	→	30
  747	→	193
  747	→	170
  747	→	132
  747	→	53
  747	→	29
  747	→	47
  747	→	117
  747	→	138
  747	→	187
  747	→	10
  747	→	282
  747	→	85
  44	→	960
  1283	→	118
  1278	→	1306
  609	→	1034
  1208	→	118
  1064	→	55
  1194	→	29
  1194	→	1268
  1161	→	1209
  1070	→	55
  86	→	99
  1232	→	118
  79	→	10
  79	→	233
  79	→	196
  79	→	283
  79	→	140
  79	→	118
  79	→	236
  79	→	173
  79	→	119
  79	→	139
  79	→	284
  79	→	101
  79	→	331
  79	→	1013
  79	→	102
  79	→	524
  79	→	1110
  79	→	1108
  79	→	1150
  1005	→	319
  512	→	1229
  208	→	109
  385	→	1115
  1212	→	118
  186	→	70
  1170	→	55
  1277	→	29
  1277	→	1300
  1214	→	118
  141	→	251
  141	→	313
  894	→	1036
  173	→	1008
  949	→	42
  277	→	111
  639	→	1111
  1075	→	1235
  1193	→	1284
  1032	→	1225
  153	→	1038
  153	→	1099
  109	→	952
  741	→	1127
  54	→	30
  1037	→	30
  308	→	97
  308	→	691
  1092	→	118
  455	→	1105
  386	→	69
  386	→	1079
  1205	→	1276
  1293	→	118
  522	→	500
  498	→	30
  1279	→	29
  1279	→	1298
  1309	→	118
  230	→	1014
  1168	→	55
  67	→	1129
  53	→	1149
  1036	→	1231
  1060	→	53
  937	→	140
  979	→	290
  265	→	76
  265	→	970
  232	→	153
  1291	→	118
  118	→	140
  118	→	233
  1018	→	1093
  1150	→	118
  1174	→	55
  1222	→	118
  188	→	171
  1035	→	30
  252	→	1057
  45	→	421
  45	→	453
  959	→	223
  1108	→	118
  1015	→	138
  66	→	669
  1059	→	1199
  971	→	172
  1224	→	118
  373	→	155
  887	→	327
  887	→	171
  887	→	193
  887	→	170
  887	→	132
  887	→	53
  887	→	29
  887	→	47
  887	→	117
  887	→	138
  887	→	187
  887	→	10
  887	→	55
  887	→	31
  516	→	406
  516	→	30
  516	→	99
  516	→	10
  516	→	100
  516	→	86
  516	→	282
  516	→	85
  1094	→	118
  497	→	1131
  112	→	45
  112	→	213
  112	→	215
  85	→	282
  85	→	406
  85	→	195
  85	→	86
  85	→	10
  85	→	84
  85	→	30
  85	→	330
  85	→	100
  77	→	10
  77	→	87
  77	→	31
  77	→	171
  77	→	407
  77	→	194
  77	→	234
  514	→	1161
  514	→	1203
  1216	→	118
  746	→	886
  746	→	894
  1013	→	140
  736	→	1006
  1021	→	406
  295	→	184
  1202	→	55
  69	→	1018
  69	→	1085
  1080	→	53
  1085	→	1197
  934	→	1119
  1236	→	118
  1204	→	53
  182	→	569
  30	→	84
  30	→	195
  216	→	10
  216	→	133
  216	→	56
  216	→	375
  216	→	1118
  957	→	119
  1307	→	118
  1122	→	118
  46	→	10
  46	→	85
  46	→	172
  46	→	235
  46	→	48
  46	→	408
  46	→	361
  46	→	328
  46	→	313
  46	→	251
  46	→	141
  46	→	54
  46	→	88
  46	→	33
  46	→	958
  46	→	122
  46	→	698
  46	→	364
  453	→	471
  1196	→	29
  1196	→	1260
  1100	→	118
  231	→	1113
  1090	→	118
  48	→	30
  198	→	936
  1128	→	118
  245	→	1073
  47	→	1117
  1116	→	118
  1203	→	1278
  164	→	497
  1017	→	45
  154	→	1016
  154	→	1081
  68	→	1067
  68	→	1101
  215	→	455
  492	→	30
  1087	→	1193
  142	→	926
  142	→	1004
  131	→	67
  1058	→	62
  1281	→	118
  744	→	1159
  744	→	1205
  489	→	1121
  1271	→	55
  670	→	29
  670	→	1069
  1120	→	118
  953	→	118
  775	→	735
  422	→	10
  422	→	194
  422	→	234
  1285	→	118
  1210	→	118
  328	→	361
  1016	→	1091
  935	→	54
  935	→	197
  935	→	141
  935	→	193
  935	→	170
  935	→	132
  935	→	53
  935	→	29
  935	→	47
  935	→	117
  935	→	138
  935	→	187
  935	→	10
  935	→	174
  43	→	1157
  1269	→	55
  961	→	118
  669	→	1151
  194	→	171
  1152	→	118
  70	→	76
  70	→	78
  929	→	978
  163	→	10
  163	→	327
  163	→	171
  163	→	55
  163	→	31
  1088	→	53
  1263	→	55
  975	→	254
  151	→	962
  155	→	489
  1096	→	118
  1039	→	55
  156	→	162
  156	→	164
  1189	→	1282
  1086	→	53
  196	→	1012
  963	→	118
  513	→	1169
  513	→	1213
  420	→	44
  307	→	1077
  011(1010)	→	1011
  011(327)	→	328
  011(42)	→	43
  011(407)	→	408
  011(1004)	→	1005
  011(231)	→	232
  011(87)	→	88
  011(1032)	→	1033
  011(171)	→	172
  011(491)	→	492
  011(1073)	→	1074
  011(229)	→	230
  011(1199)	→	1200
  011(970)	→	971
  011(489)	→	490
  011(32)	→	33
  011(239)	→	240
  011(318)	→	319
  011(366)	→	367
  011(934)	→	935
  011(234)	→	235
  011(460)	→	461
  011(292)	→	293
  011(334)	→	335
  011(47)	→	48
  011(1034)	→	1035
  011(44)	→	45
  011(966)	→	967
  011(254)	→	255
  011(385)	→	386
  011(667)	→	668
  011(417)	→	418
  011(410)	→	411
  011(320)	→	321
  011(202)	→	203
  011(206)	→	207
  011(261)	→	262
  011(304)	→	305
  011(515)	→	516
  011(145)	→	146
  011(204)	→	205
  011(34)	→	35
  011(458)	→	459
  011(70)	→	71
  011(300)	→	301
  011(735)	→	736
  011(199)	→	200
  120(10)	→	10
  220(10)	→	10
  210(10)	→	10
  211(130)	→	131
  211(732)	→	733
  211(63)	→	64
  211(1059)	→	1060
  211(745)	→	746
  211(225)	→	226
  211(263)	→	264
  211(1121)	→	1122
  211(1125)	→	1126
  211(960)	→	961
  211(93)	→	94
  211(1225)	→	1226
  211(258)	→	259
  211(464)	→	465
  211(1117)	→	1118
  211(928)	→	929
  211(142)	→	143
  211(377)	→	378
  211(374)	→	375
  211(1227)	→	1228
  211(315)	→	316
  211(1113)	→	1114
  211(245)	→	246
  211(78)	→	79
  211(38)	→	39
  211(180)	→	181
  211(1123)	→	1124
  211(155)	→	156
  211(241)	→	242
  211(609)	→	610
  211(508)	→	509
  211(1115)	→	1116
  211(288)	→	289
  211(500)	→	501
  211(1119)	→	1120
  211(740)	→	741
  211(132)	→	133
  211(306)	→	307
  211(1223)	→	1224
  211(302)	→	303
  211(1292)	→	1293
  211(150)	→	151
  211(55)	→	56
  001(111)	→	112
  001(183)	→	184
  001(313)	→	314
  001(99)	→	100
  001(36)	→	37
  001(455)	→	456
  001(1197)	→	1198
  001(124)	→	125
  001(237)	→	238
  001(152)	→	153
  001(645)	→	646
  001(368)	→	369
  001(88)	→	89
  001(1276)	→	1277
  001(85)	→	86
  001(379)	→	380
  001(502)	→	503
  001(471)	→	472
  001(29)	→	30
  001(207)	→	208
  001(268)	→	269
  001(35)	→	36
  001(272)	→	273
  001(332)	→	333
  001(95)	→	96
  001(84)	→	85
  001(1193)	→	1194
  001(414)	→	415
  001(1020)	→	1021
  001(743)	→	744
  001(125)	→	126
  001(1189)	→	1190
  001(382)	→	383
  001(1159)	→	1160
  001(369)	→	370
  001(328)	→	329
  001(222)	→	223
  001(91)	→	92
  001(931)	→	932
  001(153)	→	154
  001(1161)	→	1162
  001(462)	→	463
  001(243)	→	244
  001(639)	→	640
  001(57)	→	58
  001(513)	→	514
  001(197)	→	198
  001(930)	→	931
  001(109)	→	110
  001(367)	→	368
  001(1018)	→	1019
  001(1195)	→	1196
  001(182)	→	183
  001(1016)	→	1017
  001(329)	→	330
  001(1278)	→	1279
  001(742)	→	743
  001(364)	→	365
  001(335)	→	336
  001(461)	→	462
  001(271)	→	272
  001(128)	→	129
  001(90)	→	91
  001(298)	→	299
  001(68)	→	69
  001(958)	→	959
  001(1071)	→	1072
  001(338)	→	339
  001(174)	→	175
  001(45)	→	46
  001(89)	→	90
  001(110)	→	111
  111(409)	→	410
  111(324)	→	325
  111(325)	→	326
  111(185)	→	186
  111(224)	→	225
  111(286)	→	287
  111(416)	→	417
  111(178)	→	179
  111(76)	→	77
  111(927)	→	928
  111(287)	→	288
  111(371)	→	372
  111(187)	→	188
  111(419)	→	420
  111(62)	→	63
  111(372)	→	373
  111(41)	→	42
  111(739)	→	740
  111(257)	→	258
  111(256)	→	257
  111(933)	→	934
  111(149)	→	150
  111(926)	→	927
  111(591)	→	592
  111(31)	→	32
  111(457)	→	458
  111(179)	→	180
  111(507)	→	508
  111(201)	→	202
  200(10)	→	10
  101(177)	→	178
  101(421)	→	422
  101(1298)	→	1299
  101(240)	→	241
  101(1300)	→	1301
  101(744)	→	745
  101(376)	→	377
  101(170)	→	171
  101(459)	→	460
  101(37)	→	38
  101(1067)	→	1068
  101(365)	→	366
  101(255)	→	256
  101(370)	→	371
  101(948)	→	949
  101(30)	→	31
  101(69)	→	70
  101(184)	→	185
  101(223)	→	224
  101(144)	→	145
  101(456)	→	457
  101(285)	→	286
  101(86)	→	87
  101(198)	→	199
  101(1260)	→	1261
  101(734)	→	735
  101(238)	→	239
  101(33)	→	34
  101(1171)	→	1172
  101(1262)	→	1263
  101(92)	→	93
  101(1201)	→	1202
  101(244)	→	245
  101(319)	→	320
  101(1167)	→	1168
  101(1038)	→	1039
  101(230)	→	231
  101(1063)	→	1064
  101(418)	→	419
  101(260)	→	261
  101(1069)	→	1070
  101(514)	→	515
  101(213)	→	214
  101(253)	→	254
  101(323)	→	324
  101(305)	→	306
  101(1006)	→	1007
  101(738)	→	739
  101(1065)	→	1066
  101(1270)	→	1271
  101(129)	→	130
  101(141)	→	142
  101(731)	→	732
  101(932)	→	933
  101(521)	→	522
  101(569)	→	570
  101(314)	→	315
  101(40)	→	41
  101(333)	→	334
  101(1268)	→	1269
  101(406)	→	407
  101(154)	→	155
  101(299)	→	300
  101(301)	→	302
  101(43)	→	44
  101(1165)	→	1166
  101(1274)	→	1275
  101(974)	→	975
  101(291)	→	292
  101(774)	→	775
  101(203)	→	204
  101(148)	→	149
  101(1169)	→	1170
  101(205)	→	206
  101(968)	→	969
  101(499)	→	500
  101(317)	→	318
  101(415)	→	416
  101(1163)	→	1164
  101(463)	→	464
  101(1173)	→	1174
  101(408)	→	409
  101(200)	→	201
  101(228)	→	229
  101(262)	→	263
  100(10)	→	10
  201(1014)	→	1015
  201(1085)	→	1086
  201(383)	→	384
  201(505)	→	506
  201(330)	→	331
  201(1207)	→	1208
  201(1284)	→	1285
  201(1203)	→	1204
  201(1308)	→	1309
  201(275)	→	276
  201(1081)	→	1082
  201(273)	→	274
  201(411)	→	412
  201(1211)	→	1212
  201(58)	→	59
  201(235)	→	236
  201(146)	→	147
  201(1101)	→	1102
  201(269)	→	270
  201(122)	→	123
  201(1107)	→	1108
  201(1089)	→	1090
  201(1109)	→	1110
  201(266)	→	267
  201(1157)	→	1158
  201(453)	→	454
  201(100)	→	101
  201(1002)	→	1003
  201(954)	→	955
  201(321)	→	322
  201(1095)	→	1096
  201(1205)	→	1206
  201(215)	→	216
  201(282)	→	283
  201(1091)	→	1092
  201(523)	→	524
  201(1087)	→	1088
  201(736)	→	737
  201(1280)	→	1281
  201(972)	→	973
  201(107)	→	108
  201(339)	→	340
  201(689)	→	690
  201(96)	→	97
  201(1103)	→	1104
  201(251)	→	252
  201(1111)	→	1112
  201(1306)	→	1307
  201(1215)	→	1216
  201(172)	→	173
  201(1213)	→	1214
  201(296)	→	297
  201(936)	→	937
  201(60)	→	61
  201(1290)	→	1291
  201(104)	→	105
  201(946)	→	947
  201(503)	→	504
  201(1099)	→	1100
  201(380)	→	381
  201(1093)	→	1094
  201(195)	→	196
  201(1079)	→	1080
  201(175)	→	176
  201(1209)	→	1210
  201(1105)	→	1106
  201(293)	→	294
  201(952)	→	953
  201(126)	→	127
  201(336)	→	337
  201(1155)	→	1156
  201(361)	→	362
  201(1282)	→	1283
  201(1221)	→	1222
  201(117)	→	118
  020(10)	→	10
  221(66)	→	67
  221(1008)	→	1009
  221(101)	→	102
  221(120)	→	121
  221(164)	→	165
  221(964)	→	965
  221(138)	→	139
  221(976)	→	977
  221(1235)	→	1236
  221(118)	→	119
  221(1131)	→	1132
  221(307)	→	308
  221(1229)	→	1230
  221(1012)	→	1013
  221(978)	→	979
  221(1129)	→	1130
  221(691)	→	692
  221(1237)	→	1238
  221(1127)	→	1128
  221(511)	→	512
  221(956)	→	957
  221(1149)	→	1150
  221(64)	→	65
  221(289)	→	290
  221(283)	→	284
  221(509)	→	510
  221(119)	→	120
  221(412)	→	413
  221(1151)	→	1152
  221(962)	→	963
  221(105)	→	106
  221(362)	→	363
  221(65)	→	66
  221(1231)	→	1232
  221(226)	→	227
  221(894)	→	895
  221(510)	→	511
  221(102)	→	103
  021(337)	→	338
  021(297)	→	298
  021(56)	→	57
  021(236)	→	237
  021(276)	→	277
  021(741)	→	742
  021(176)	→	177
  021(737)	→	738
  021(697)	→	698
  021(59)	→	60
  021(242)	→	243
  021(106)	→	107
  021(140)	→	141
  021(669)	→	670
  021(322)	→	323
  021(413)	→	414
  021(196)	→	197
  021(375)	→	376
  021(127)	→	128
  021(156)	→	157
  021(284)	→	285
  021(94)	→	95
  021(108)	→	109
  021(331)	→	332
  021(252)	→	253
  021(1036)	→	1037
  021(143)	→	144
  021(267)	→	268
  021(97)	→	98
  021(221)	→	222
  021(512)	→	513
  021(67)	→	68
  021(147)	→	148
  021(746)	→	747
  021(121)	→	122
  021(504)	→	505
  021(103)	→	104
  021(929)	→	930
  021(123)	→	124
  021(39)	→	40
  021(363)	→	364
  021(294)	→	295
  021(151)	→	152
  021(53)	→	54
  021(1077)	→	1078
  021(378)	→	379
  021(465)	→	466
  021(274)	→	275
  021(381)	→	382
  021(181)	→	182
  021(501)	→	502
  021(497)	→	498
  021(316)	→	317
  021(173)	→	174
  021(227)	→	228
  021(1075)	→	1076
  021(270)	→	271
  021(259)	→	260
  021(290)	→	291
  021(733)	→	734
  000(10)	→	10
  010(10)	→	10
  121(264)	→	265
  121(340)	→	341
  121(162)	→	163
  121(61)	→	62
  121(193)	→	194
  121(384)	→	385
  121(886)	→	887
  121(1057)	→	1058
  121(506)	→	507
  121(303)	→	304
  121(233)	→	234
  110(10)	→	10