Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/86577)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Bounds

• final states:

  {7}

• transitions:

  1182	→	1172
  78	→	20
  1374	→	212
  854	→	169
  854	→	47
  854	→	7
  854	→	16
  854	→	13
  854	→	144
  223	→	1041
  33	→	168
  33	→	247
  33	→	324
  33	→	473
  157	→	69
  1268	→	1260
  221	→	76
  958	→	34
  733	→	1104
  917	→	143
  917	→	324
  917	→	168
  917	→	71
  917	→	42
  917	→	26
  917	→	12
  917	→	32
  917	→	63
  917	→	7
  917	→	247
  917	→	33
  917	→	45
  29	→	222
  1437	→	34
  835	→	264
  202	→	889
  750	→	127
  1406	→	17
  1056	→	143
  1156	→	310
  1109	→	212
  98	→	7
  98	→	324
  98	→	168
  98	→	325
  98	→	247
  98	→	33
  98	→	13
  98	→	365
  98	→	195
  98	→	126
  98	→	87
  98	→	248
  98	→	110
  98	→	27
  98	→	345
  98	→	278
  98	→	142
  98	→	72
  98	→	64
  98	→	265
  98	→	18
  98	→	245
  98	→	427
  98	→	327
  98	→	1162
  98	→	980
  98	→	112
  98	→	1028
  98	→	1127
  1288	→	1276
  1354	→	64
  1166	→	370
  51	→	1010
  97	→	753
  97	→	897
  734	→	345
  734	→	278
  734	→	71
  734	→	42
  734	→	26
  734	→	12
  734	→	32
  734	→	63
  734	→	7
  734	→	142
  734	→	72
  15	→	7
  15	→	126
  15	→	87
  15	→	88
  15	→	110
  15	→	27
  15	→	345
  15	→	278
  15	→	142
  15	→	72
  15	→	14
  15	→	128
  15	→	112
  15	→	1028
  15	→	986
  15	→	934
  15	→	1404
  15	→	370
  15	→	1166
  15	→	949
  15	→	1435
  915	→	1145
  1431	→	950
  1046	→	69
  1479	→	933
  933	→	1267
  1435	→	949
  1386	→	53
  1195	→	1411
  167	→	97
  995	→	1367
  149	→	36
  1107	→	212
  276	→	96
  133	→	45
  1158	→	326
  1172	→	1259
  1327	→	1409
  1103	→	197
  18	→	71
  18	→	42
  18	→	26
  18	→	12
  18	→	32
  18	→	63
  18	→	7
  18	→	1261
  18	→	1266
  365	→	1086
  1362	→	212
  988	→	53
  988	→	1061
  1011	→	96
  1011	→	1327
  980	→	33
  1324	→	36
  1324	→	1455
  838	→	1092
  1062	→	143
  108	→	564
  1340	→	64
  914	→	1183
  1332	→	143
  37	→	7
  37	→	345
  37	→	142
  37	→	72
  37	→	126
  37	→	87
  37	→	248
  37	→	110
  37	→	27
  37	→	194
  37	→	64
  37	→	111
  37	→	169
  37	→	47
  37	→	16
  37	→	13
  37	→	144
  37	→	775
  37	→	14
  37	→	474
  37	→	567
  37	→	602
  37	→	1125
  37	→	1276
  37	→	1306
  37	→	1460
  1190	→	1173
  34	→	162
  34	→	237
  65	→	150
  65	→	183
  1454	→	933
  1048	→	143
  1328	→	69
  947	→	29
  381	→	53
  756	→	163
  696	→	345
  696	→	7
  696	→	142
  696	→	72
  1095	→	64
  193	→	97
  193	→	1157
  20	→	569
  20	→	942
  473	→	1305
  713	→	14
  31	→	20
  1164	→	345
  1162	→	327
  246	→	97
  380	→	855
  1105	→	212
  1040	→	567
  1040	→	345
  1040	→	7
  1040	→	142
  1040	→	72
  1040	→	602
  1298	→	1276
  165	→	836
  695	→	973
  695	→	1029
  695	→	1094
  695	→	1110
  127	→	1151
  13	→	16
  13	→	47
  13	→	426
  13	→	17
  13	→	71
  13	→	42
  13	→	26
  13	→	12
  13	→	32
  13	→	63
  13	→	7
  13	→	933
  13	→	1165
  13	→	311
  13	→	937
  13	→	1260
  13	→	1268
  570	→	565
  570	→	755
  1154	→	47
  1338	→	64
  1318	→	14
  1111	→	33
  1412	→	933
  1317	→	1465
  1173	→	1421
  1173	→	1463
  689	→	339
  689	→	1323
  987	→	1349
  44	→	264
  44	→	601
  1064	→	64
  748	→	47
  748	→	944
  73	→	1112
  1366	→	212
  323	→	245
  125	→	20
  125	→	834
  993	→	1373
  1398	→	345
  1030	→	47
  1099	→	197
  36	→	710
  36	→	712
  36	→	1303
  1385	→	1459
  760	→	64
  994	→	14
  890	→	345
  916	→	1149
  916	→	1387
  177	→	745
  248	→	1161
  21	→	7
  21	→	47
  21	→	17
  21	→	16
  21	→	13
  21	→	127
  21	→	169
  21	→	111
  21	→	194
  21	→	64
  21	→	214
  21	→	1460
  1127	→	975
  72	→	142
  72	→	345
  72	→	1126
  1410	→	933
  178	→	97
  1176	→	1172
  983	→	1355
  346	→	126
  346	→	87
  346	→	7
  346	→	88
  346	→	110
  346	→	27
  976	→	49
  976	→	1114
  311	→	1165
  788	→	111
  788	→	194
  788	→	71
  788	→	42
  788	→	26
  788	→	12
  788	→	32
  788	→	63
  788	→	7
  788	→	64
  788	→	214
  788	→	1460
  337	→	757
  1256	→	12
  1256	→	1436
  1042	→	132
  109	→	36
  1456	→	69
  345	→	1108
  741	→	47
  986	→	53
  986	→	1055
  1356	→	64
  823	→	810
  54	→	7
  54	→	43
  54	→	28
  54	→	73
  54	→	143
  54	→	324
  54	→	168
  54	→	247
  54	→	33
  54	→	45
  54	→	776
  54	→	1109
  54	→	1462
  982	→	53
  982	→	1047
  52	→	948
  1282	→	1108
  1282	→	345
  1282	→	142
  1282	→	1126
  1282	→	72
  75	→	95
  292	→	36
  292	→	749
  363	→	97
  363	→	727
  363	→	800
  1168	→	17
  1101	→	197
  1146	→	47
  1146	→	1255
  853	→	981
  853	→	989
  853	→	1031
  853	→	1275
  53	→	857
  787	→	932
  937	→	933
  937	→	1265
  686	→	680
  954	→	13
  954	→	127
  954	→	1189
  232	→	53
  28	→	71
  28	→	42
  28	→	26
  28	→	12
  28	→	32
  28	→	63
  28	→	7
  1150	→	47
  1174	→	979
  1174	→	1126
  1174	→	775
  1174	→	14
  1174	→	142
  1174	→	345
  1174	→	110
  1174	→	126
  1174	→	7
  1174	→	88
  1174	→	87
  1174	→	27
  1174	→	278
  1174	→	72
  1174	→	128
  1174	→	15
  1174	→	1430
  1174	→	949
  1174	→	1435
  258	→	740
  258	→	957
  1404	→	345
  801	→	28
  754	→	64
  820	→	1063
  820	→	1163
  1043	→	1171
  114	→	1147
  602	→	567
  14	→	775
  14	→	1124
  14	→	1434
  1045	→	1175
  93	→	1181
  981	→	1353
  1125	→	975
  800	→	1153
  985	→	1359
  684	→	126
  684	→	87
  684	→	7
  684	→	248
  684	→	110
  684	→	27
  12	→	936
  169	→	1102
  989	→	1361
  1458	→	64
  1296	→	1276
  1315	→	1457
  1455	→	1478
  944	→	1337
  944	→	1397
  746	→	47
  1044	→	69
  7	→	12
  7	→	26
  7	→	32
  7	→	42
  7	→	63
  7	→	71
  568	→	345
  568	→	7
  568	→	142
  568	→	72
  1184	→	1172
  991	→	1365
  69	→	685
  69	→	747
  69	→	759
  69	→	822
  1085	→	162
  758	→	64
  934	→	1419
  934	→	1461
  1420	→	27
  64	→	194
  64	→	687
  64	→	975
  64	→	1027
  64	→	1155
  46	→	36
  46	→	899
  362	→	1448
  1316	→	53
  1316	→	1331
  752	→	64
  1196	→	13
  856	→	837
  115	→	13
  990	→	14
  48	→	103
  48	→	120
  48	→	277
  48	→	309
  48	→	71
  48	→	42
  48	→	26
  48	→	12
  48	→	32
  48	→	63
  48	→	7
  48	→	775
  48	→	14
  48	→	474
  48	→	1276
  48	→	1306
  1429	→	950
  821	→	345
  821	→	278
  821	→	71
  821	→	42
  821	→	26
  821	→	12
  821	→	32
  821	→	63
  821	→	7
  821	→	142
  821	→	72
  821	→	112
  821	→	1028
  47	→	985
  47	→	993
  47	→	1295
  17	→	1339
  17	→	1403
  683	→	987
  683	→	995
  683	→	1167
  683	→	1297
  945	→	18
  896	→	345
  718	→	96
  718	→	1043
  712	→	1106
  164	→	695
  1148	→	47
  1464	→	212
  567	→	983
  567	→	991
  567	→	1287
  148	→	1045
  858	→	837
  974	→	43
  1087	→	164
  203	→	192
  1266	→	1261
  1368	→	212
  1054	→	143
  1422	→	27
  1360	→	64
  340	→	14
  1093	→	173
  1264	→	1165
  1264	→	311
  1290	→	1276
  259	→	19
  953	→	1195
  711	→	72
  1028	→	112
  474	→	14
  943	→	933
  1113	→	251
  1306	→	1276
  19	→	1098
  935	→	88
  935	→	979
  935	→	1126
  935	→	775
  935	→	14
  935	→	142
  935	→	345
  935	→	110
  935	→	126
  935	→	7
  935	→	87
  935	→	27
  935	→	278
  935	→	72
  935	→	128
  935	→	15
  935	→	1428
  935	→	839
  935	→	949
  935	→	1435
  144	→	1100
  43	→	212
  43	→	364
  43	→	946
  1388	→	36
  1152	→	277
  27	→	87
  27	→	110
  27	→	126
  27	→	979
  27	→	1385
  1350	→	64
  70	→	7
  70	→	345
  70	→	142
  70	→	72
  70	→	249
  70	→	857
  70	→	53
  70	→	1386
  427	→	245
  427	→	1084
  1304	→	1276
  984	→	53
  984	→	1053
  992	→	14
  1123	→	35
  996	→	14
  94	→	69
  94	→	714
  192	→	751
  192	→	895
  1460	→	64
  1039	→	1289
  1039	→	1315
  1039	→	1317
  1039	→	1405
  156	→	679
  156	→	809
  1466	→	212
  1462	→	212
  898	→	345
  41(350)	→	351
  41(817)	→	818
  41(17)	→	18
  41(1047)	→	1048
  41(912)	→	913
  41(820)	→	821
  41(778)	→	779
  41(192)	→	193
  41(326)	→	327
  41(907)	→	908
  41(335)	→	336
  41(153)	→	154
  41(1110)	→	1111
  41(329)	→	330
  41(324)	→	325
  41(91)	→	92
  41(1117)	→	1118
  41(1061)	→	1062
  41(908)	→	909
  41(822)	→	823
  41(243)	→	244
  41(214)	→	215
  41(242)	→	243
  41(107)	→	108
  41(946)	→	947
  41(65)	→	66
  41(315)	→	316
  41(129)	→	130
  41(840)	→	841
  41(1255)	→	1256
  41(1161)	→	1162
  41(122)	→	123
  41(1112)	→	1113
  41(365)	→	366
  41(681)	→	682
  41(32)	→	33
  41(312)	→	313
  41(979)	→	980
  41(1331)	→	1332
  41(809)	→	810
  41(844)	→	845
  41(426)	→	427
  41(816)	→	817
  41(1053)	→	1054
  41(900)	→	901
  41(320)	→	321
  41(283)	→	284
  41(89)	→	90
  41(944)	→	945
  41(250)	→	251
  41(377)	→	378
  41(1055)	→	1056
  41(194)	→	195
  41(269)	→	270
  41(97)	→	98
  41(348)	→	349
  41(279)	→	280
  41(151)	→	152
  41(19)	→	20
  41(784)	→	785
  41(331)	→	332
  41(189)	→	190
  41(257)	→	258
  41(28)	→	29
  41(142)	→	143
  41(1034)	→	1035
  41(202)	→	203
  41(372)	→	373
  41(164)	→	165
  41(152)	→	153
  41(373)	→	374
  41(220)	→	221
  41(44)	→	45
  52(1453)	→	1454
  52(1451)	→	1452
  52(1280)	→	1281
  52(1430)	→	1431
  52(1278)	→	1279
  52(1428)	→	1429
  52(949)	→	950
  02(1263)	→	1264
  02(953)	→	954
  02(1279)	→	1280
  02(1259)	→	1260
  02(1183)	→	1184
  02(1478)	→	1479
  02(1409)	→	1410
  02(1181)	→	1182
  02(1261)	→	1262
  02(1267)	→	1268
  02(1411)	→	1412
  02(1171)	→	1172
  02(932)	→	933
  02(1175)	→	1176
  02(936)	→	937
  02(942)	→	943
  12(948)	→	949
  12(1276)	→	1277
  12(952)	→	953
  12(1434)	→	1435
  12(1173)	→	1174
  12(934)	→	935
  12(1448)	→	1449
  11(247)	→	248
  11(87)	→	88
  11(319)	→	320
  11(842)	→	843
  11(1317)	→	1318
  11(1114)	→	1115
  11(289)	→	290
  11(183)	→	184
  11(1010)	→	1011
  11(217)	→	218
  11(712)	→	713
  11(147)	→	148
  11(776)	→	777
  11(14)	→	15
  11(291)	→	292
  11(1421)	→	1422
  11(849)	→	850
  11(281)	→	282
  11(370)	→	371
  11(993)	→	994
  11(905)	→	906
  11(733)	→	734
  11(347)	→	348
  11(995)	→	996
  11(345)	→	346
  11(52)	→	53
  11(92)	→	93
  11(1120)	→	1121
  11(991)	→	992
  11(155)	→	156
  11(266)	→	267
  11(811)	→	812
  11(176)	→	177
  11(850)	→	851
  11(216)	→	217
  11(237)	→	238
  11(362)	→	363
  11(780)	→	781
  11(989)	→	990
  11(717)	→	718
  11(188)	→	189
  11(225)	→	226
  11(325)	→	326
  11(105)	→	106
  11(26)	→	27
  11(1157)	→	1158
  11(272)	→	273
  11(64)	→	65
  11(1323)	→	1324
  11(781)	→	782
  11(30)	→	31
  11(1419)	→	1420
  11(212)	→	213
  11(184)	→	185
  11(852)	→	853
  11(120)	→	121
  11(288)	→	289
  40(7)	→	7
  50(7)	→	7
  22(1450)	→	1451
  22(1189)	→	1190
  22(933)	→	934
  22(1281)	→	1282
  22(1172)	→	1173
  30(7)	→	7
  51(812)	→	813
  51(42)	→	43
  51(238)	→	239
  51(973)	→	974
  51(112)	→	113
  51(186)	→	187
  51(375)	→	376
  51(327)	→	328
  51(800)	→	801
  51(255)	→	256
  51(906)	→	907
  51(123)	→	124
  51(915)	→	916
  51(1084)	→	1085
  51(1086)	→	1087
  51(53)	→	54
  51(687)	→	688
  51(569)	→	570
  51(124)	→	125
  51(682)	→	683
  51(27)	→	28
  51(66)	→	67
  51(564)	→	565
  51(810)	→	811
  51(957)	→	958
  51(146)	→	147
  51(198)	→	199
  51(128)	→	129
  51(351)	→	352
  51(775)	→	776
  51(1108)	→	1109
  51(284)	→	285
  51(339)	→	340
  51(1365)	→	1366
  51(1361)	→	1362
  51(685)	→	686
  51(731)	→	732
  51(166)	→	167
  51(1463)	→	1464
  51(1121)	→	1122
  51(1436)	→	1437
  51(49)	→	50
  51(249)	→	250
  51(72)	→	73
  51(290)	→	291
  51(273)	→	274
  51(779)	→	780
  51(729)	→	730
  51(103)	→	104
  51(145)	→	146
  51(1373)	→	1374
  51(165)	→	166
  51(1122)	→	1123
  51(338)	→	339
  51(354)	→	355
  51(1038)	→	1039
  51(311)	→	312
  51(274)	→	275
  51(380)	→	381
  51(910)	→	911
  51(916)	→	917
  51(163)	→	164
  51(1033)	→	1034
  51(121)	→	122
  51(1367)	→	1368
  51(114)	→	115
  51(851)	→	852
  51(361)	→	362
  51(45)	→	46
  51(51)	→	52
  51(332)	→	333
  51(33)	→	34
  51(313)	→	314
  51(174)	→	175
  51(68)	→	69
  51(1461)	→	1462
  51(1104)	→	1105
  51(1465)	→	1466
  51(715)	→	716
  51(215)	→	216
  51(252)	→	253
  51(73)	→	74
  51(1106)	→	1107
  51(371)	→	372
  51(845)	→	846
  51(679)	→	680
  51(200)	→	201
  01(224)	→	225
  01(857)	→	858
  01(1405)	→	1406
  01(132)	→	133
  01(1155)	→	1156
  01(368)	→	369
  01(1100)	→	1101
  01(93)	→	94
  01(16)	→	17
  01(782)	→	783
  01(836)	→	837
  01(903)	→	904
  01(20)	→	21
  01(321)	→	322
  01(328)	→	329
  01(18)	→	19
  01(1045)	→	1046
  01(1153)	→	1154
  01(349)	→	350
  01(1167)	→	1168
  01(227)	→	228
  01(1455)	→	1456
  01(819)	→	820
  01(12)	→	13
  01(278)	→	279
  01(1098)	→	1099
  01(268)	→	269
  01(322)	→	323
  01(1043)	→	1044
  01(749)	→	750
  01(190)	→	191
  01(191)	→	192
  01(1031)	→	1032
  01(251)	→	252
  01(899)	→	900
  01(1037)	→	1038
  01(740)	→	741
  01(126)	→	127
  01(745)	→	746
  01(76)	→	77
  01(314)	→	315
  01(1145)	→	1146
  01(755)	→	756
  01(74)	→	75
  01(364)	→	365
  01(1147)	→	1148
  01(201)	→	202
  01(256)	→	257
  01(245)	→	246
  01(162)	→	163
  01(218)	→	219
  01(310)	→	311
  01(358)	→	359
  01(855)	→	856
  01(1119)	→	1120
  01(316)	→	317
  01(170)	→	171
  01(231)	→	232
  01(271)	→	272
  01(1149)	→	1150
  01(1327)	→	1328
  01(168)	→	169
  01(143)	→	144
  01(839)	→	840
  01(1029)	→	1030
  01(367)	→	368
  01(1116)	→	1117
  01(287)	→	288
  01(108)	→	109
  01(785)	→	786
  01(848)	→	849
  01(196)	→	197
  01(1195)	→	1196
  01(787)	→	788
  01(1102)	→	1103
  01(747)	→	748
  01(914)	→	915
  01(67)	→	68
  01(902)	→	903
  01(195)	→	196
  01(309)	→	310
  01(379)	→	380
  01(355)	→	356
  00(7)	→	7
  20(7)	→	7
  21(710)	→	711
  21(732)	→	733
  21(187)	→	188
  21(177)	→	178
  21(1041)	→	1042
  21(346)	→	347
  21(131)	→	132
  21(317)	→	318
  21(127)	→	128
  21(565)	→	566
  21(1165)	→	1166
  21(1403)	→	1404
  21(90)	→	91
  21(357)	→	358
  21(728)	→	729
  21(843)	→	844
  21(277)	→	278
  21(834)	→	835
  21(13)	→	14
  21(254)	→	255
  21(69)	→	70
  21(1035)	→	1036
  21(1036)	→	1037
  21(154)	→	155
  21(1387)	→	1388
  21(169)	→	170
  21(695)	→	696
  21(71)	→	72
  21(88)	→	89
  21(369)	→	370
  21(248)	→	249
  21(360)	→	361
  21(267)	→	268
  21(75)	→	76
  21(680)	→	681
  21(77)	→	78
  21(336)	→	337
  21(229)	→	230
  21(258)	→	259
  21(1032)	→	1033
  21(333)	→	334
  21(318)	→	319
  21(35)	→	36
  21(566)	→	567
  21(1385)	→	1386
  21(230)	→	231
  21(909)	→	910
  21(34)	→	35
  21(359)	→	360
  21(904)	→	905
  21(601)	→	602
  21(1315)	→	1316
  21(1115)	→	1116
  21(282)	→	283
  21(43)	→	44
  21(150)	→	151
  21(985)	→	986
  21(983)	→	984
  21(337)	→	338
  21(222)	→	223
  21(130)	→	131
  21(1027)	→	1028
  21(244)	→	245
  21(156)	→	157
  21(1397)	→	1398
  21(185)	→	186
  21(895)	→	896
  21(786)	→	787
  21(981)	→	982
  21(838)	→	839
  21(275)	→	276
  21(987)	→	988
  21(330)	→	331
  21(889)	→	890
  21(374)	→	375
  21(818)	→	819
  21(111)	→	112
  21(897)	→	898
  21(353)	→	354
  21(1163)	→	1164
  31(36)	→	37
  31(1359)	→	1360
  31(366)	→	367
  31(285)	→	286
  31(1126)	→	1127
  31(199)	→	200
  31(1353)	→	1354
  31(815)	→	816
  31(29)	→	30
  31(1337)	→	1338
  31(777)	→	778
  31(1092)	→	1093
  31(813)	→	814
  31(683)	→	684
  31(913)	→	914
  31(1355)	→	1356
  31(1124)	→	1125
  31(759)	→	760
  31(1118)	→	1119
  31(63)	→	64
  31(219)	→	220
  31(110)	→	111
  31(223)	→	224
  31(50)	→	51
  31(814)	→	815
  31(783)	→	784
  31(334)	→	335
  31(716)	→	717
  31(753)	→	754
  31(264)	→	265
  31(47)	→	48
  31(144)	→	145
  31(48)	→	49
  31(1349)	→	1350
  31(270)	→	271
  31(175)	→	176
  31(240)	→	241
  31(730)	→	731
  31(228)	→	229
  31(106)	→	107
  31(96)	→	97
  31(847)	→	848
  31(1151)	→	1152
  31(356)	→	357
  31(378)	→	379
  31(1339)	→	1340
  31(688)	→	689
  31(1459)	→	1460
  31(173)	→	174
  31(1039)	→	1040
  31(901)	→	902
  31(1063)	→	1064
  31(757)	→	758
  31(975)	→	976
  31(567)	→	568
  31(714)	→	715
  31(846)	→	847
  31(286)	→	287
  31(241)	→	242
  31(751)	→	752
  31(1094)	→	1095
  31(171)	→	172
  31(265)	→	266
  31(104)	→	105
  31(172)	→	173
  31(473)	→	474
  31(197)	→	198
  31(148)	→	149
  31(1457)	→	1458
  31(911)	→	912
  31(280)	→	281
  31(853)	→	854
  31(727)	→	728
  31(376)	→	377
  31(95)	→	96
  31(113)	→	114
  31(837)	→	838
  31(226)	→	227
  31(841)	→	842
  31(253)	→	254
  31(213)	→	214
  31(352)	→	353
  31(239)	→	240
  42(1262)	→	1263
  42(1260)	→	1261
  42(1265)	→	1266
  42(1277)	→	1278
  42(950)	→	951
  10(7)	→	7
  32(1297)	→	1298
  32(1295)	→	1296
  32(1449)	→	1450
  32(951)	→	952
  32(1305)	→	1306
  32(1287)	→	1288
  32(1452)	→	1453
  32(1275)	→	1276
  32(1289)	→	1290
  32(1303)	→	1304