Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96119)

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:

  272	→	19
  1067	→	16
  33	→	101
  33	→	206
  33	→	259
  33	→	186
  33	→	63
  33	→	25
  33	→	12
  33	→	32
  33	→	155
  33	→	7
  339	→	79
  871	→	54
  221	→	127
  899	→	888
  958	→	1060
  102	→	242
  102	→	222
  102	→	186
  102	→	63
  102	→	25
  102	→	12
  102	→	32
  102	→	155
  102	→	7
  102	→	187
  102	→	1114
  32	→	1022
  32	→	1048
  32	→	1113
  128	→	7
  128	→	242
  128	→	222
  128	→	187
  128	→	102
  128	→	259
  128	→	101
  128	→	206
  128	→	33
  128	→	208
  128	→	884
  1057	→	54
  1057	→	1105
  1106	→	127
  81	→	30
  897	→	99
  1142	→	423
  809	→	340
  809	→	222
  809	→	186
  809	→	63
  809	→	25
  809	→	12
  809	→	32
  809	→	155
  809	→	7
  809	→	187
  809	→	118
  809	→	1114
  809	→	94
  1166	→	16
  387	→	70
  15	→	7
  15	→	222
  15	→	187
  15	→	156
  15	→	242
  15	→	102
  15	→	443
  15	→	605
  15	→	611
  15	→	1114
  578	→	35
  781	→	983
  303	→	898
  1140	→	423
  998	→	370
  998	→	64
  998	→	7
  998	→	129
  998	→	34
  998	→	1049
  1008	→	1004
  811	→	117
  502	→	73
  502	→	186
  502	→	63
  502	→	25
  502	→	12
  502	→	32
  502	→	155
  502	→	7
  502	→	64
  502	→	35
  502	→	578
  502	→	1049
  119	→	803
  18	→	939
  978	→	306
  1118	→	261
  499	→	1080
  1104	→	127
  1102	→	25
  1102	→	1163
  1114	→	222
  1062	→	1131
  187	→	222
  187	→	1115
  443	→	1109
  37	→	14
  584	→	45
  34	→	129
  34	→	370
  1126	→	372
  1055	→	54
  1055	→	1103
  185	→	164
  55	→	7
  55	→	242
  55	→	222
  55	→	187
  55	→	102
  1134	→	423
  381	→	394
  1110	→	222
  20	→	7
  20	→	222
  20	→	187
  20	→	1114
  397	→	384
  445	→	222
  445	→	186
  445	→	63
  445	→	25
  445	→	12
  445	→	32
  445	→	155
  445	→	7
  445	→	187
  445	→	1114
  304	→	71
  304	→	761
  31	→	7
  31	→	73
  31	→	64
  31	→	176
  31	→	42
  31	→	16
  31	→	13
  31	→	27
  31	→	222
  31	→	187
  31	→	117
  31	→	48
  31	→	207
  31	→	91
  31	→	26
  31	→	260
  31	→	156
  31	→	340
  31	→	118
  31	→	370
  31	→	129
  31	→	34
  31	→	188
  31	→	423
  31	→	443
  31	→	498
  31	→	1114
  31	→	94
  31	→	1023
  31	→	1049
  942	→	222
  1164	→	34
  1132	→	423
  841	→	222
  841	→	186
  841	→	63
  841	→	25
  841	→	12
  841	→	32
  841	→	155
  841	→	7
  841	→	187
  841	→	443
  841	→	1114
  71	→	603
  71	→	828
  71	→	900
  1081	→	16
  127	→	496
  127	→	778
  127	→	941
  901	→	888
  1112	→	222
  13	→	16
  13	→	42
  13	→	1082
  1066	→	1139
  940	→	222
  1130	→	423
  884	→	259
  609	→	101
  1064	→	1141
  769	→	222
  769	→	7
  769	→	341
  769	→	187
  769	→	1116
  769	→	1114
  26	→	48
  26	→	91
  26	→	117
  26	→	610
  26	→	7
  26	→	207
  26	→	867
  26	→	262
  201	→	13
  72	→	7
  72	→	222
  72	→	341
  72	→	187
  72	→	340
  72	→	118
  72	→	117
  72	→	48
  72	→	91
  72	→	26
  72	→	224
  72	→	443
  72	→	1116
  72	→	1114
  72	→	94
  72	→	93
  72	→	497
  72	→	1023
  72	→	1053
  138	→	30
  389	→	222
  389	→	186
  389	→	63
  389	→	25
  389	→	12
  389	→	32
  389	→	155
  389	→	7
  389	→	187
  389	→	1114
  788	→	176
  788	→	42
  788	→	7
  788	→	16
  788	→	13
  788	→	27
  788	→	423
  788	→	498
  1053	→	93
  773	→	763
  773	→	943
  773	→	977
  1041	→	65
  75	→	1119
  237	→	220
  1047	→	73
  1168	→	42
  1188	→	423
  808	→	1058
  808	→	1066
  1060	→	1129
  28	→	887
  118	→	340
  258	→	30
  258	→	575
  188	→	851
  188	→	863
  425	→	18
  959	→	1040
  959	→	1056
  959	→	1064
  1108	→	127
  1015	→	35
  1015	→	883
  1015	→	442
  1015	→	7
  1015	→	73
  1015	→	577
  1015	→	64
  1015	→	578
  1015	→	1049
  66	→	305
  1059	→	54
  1059	→	1107
  14	→	287
  14	→	1001
  1063	→	16
  357	→	30
  1012	→	1165
  12	→	422
  112	→	30
  100	→	71
  7	→	12
  7	→	25
  7	→	32
  7	→	63
  7	→	155
  7	→	186
  1006	→	224
  1006	→	443
  1085	→	178
  1080	→	1133
  1049	→	73
  934	→	207
  444	→	1003
  444	→	1099
  960	→	117
  960	→	48
  960	→	186
  960	→	63
  960	→	25
  960	→	12
  960	→	32
  960	→	155
  960	→	7
  960	→	91
  960	→	26
  960	→	93
  960	→	497
  960	→	1023
  960	→	1053
  64	→	73
  64	→	442
  64	→	577
  64	→	883
  64	→	1052
  1122	→	117
  1100	→	187
  1083	→	158
  47	→	36
  17	→	143
  17	→	810
  1116	→	243
  154	→	127
  870	→	1101
  768	→	1038
  768	→	1054
  768	→	1062
  858	→	242
  858	→	222
  858	→	186
  858	→	63
  858	→	25
  858	→	12
  858	→	32
  858	→	155
  858	→	7
  858	→	187
  858	→	102
  320	→	70
  829	→	933
  388	→	1121
  74	→	1125
  1120	→	328
  1165	→	1187
  92	→	325
  932	→	187
  1002	→	117
  19	→	931
  19	→	1007
  611	→	605
  43	→	583
  43	→	1084
  1065	→	16
  27	→	176
  576	→	34
  1023	→	497
  166	→	80
  864	→	187
  262	→	867
  1061	→	16
  1039	→	14
  1039	→	1167
  156	→	388
  156	→	772
  156	→	1117
  857	→	1009
  857	→	1046
  857	→	1111
  31(388)	→	389
  31(765)	→	766
  31(95)	→	96
  31(766)	→	767
  31(384)	→	385
  31(145)	→	146
  31(259)	→	260
  31(210)	→	211
  31(891)	→	892
  31(45)	→	46
  31(291)	→	292
  31(196)	→	197
  31(104)	→	105
  31(832)	→	833
  31(851)	→	852
  31(106)	→	107
  31(761)	→	762
  31(155)	→	156
  31(103)	→	104
  31(329)	→	330
  31(354)	→	355
  31(889)	→	890
  31(246)	→	247
  31(49)	→	50
  31(989)	→	990
  31(143)	→	144
  31(243)	→	244
  31(111)	→	112
  31(219)	→	220
  31(985)	→	986
  31(946)	→	947
  31(949)	→	950
  31(834)	→	835
  31(378)	→	379
  31(318)	→	319
  31(839)	→	840
  31(955)	→	956
  31(610)	→	611
  31(308)	→	309
  31(309)	→	310
  31(604)	→	605
  31(122)	→	123
  31(64)	→	65
  31(1040)	→	1041
  31(301)	→	302
  31(379)	→	380
  31(852)	→	853
  31(957)	→	958
  31(110)	→	111
  31(295)	→	296
  31(130)	→	131
  31(13)	→	14
  31(249)	→	250
  31(307)	→	308
  31(893)	→	894
  31(250)	→	251
  31(14)	→	15
  31(950)	→	951
  31(310)	→	311
  31(380)	→	381
  31(346)	→	347
  31(302)	→	303
  31(294)	→	295
  31(217)	→	218
  31(300)	→	301
  31(179)	→	180
  31(121)	→	122
  31(256)	→	257
  31(803)	→	804
  31(147)	→	148
  31(373)	→	374
  31(69)	→	70
  31(333)	→	334
  31(956)	→	957
  31(68)	→	69
  31(343)	→	344
  31(838)	→	839
  31(831)	→	832
  02(1141)	→	1142
  02(1129)	→	1130
  02(1003)	→	1004
  02(1133)	→	1134
  02(1007)	→	1008
  02(1187)	→	1188
  02(1131)	→	1132
  02(1139)	→	1140
  02(394)	→	395
  02(422)	→	423
  32(396)	→	397
  32(1005)	→	1006
  32(395)	→	396
  32(423)	→	424
  32(1004)	→	1005
  32(424)	→	425
  41(148)	→	149
  41(108)	→	109
  41(1117)	→	1118
  41(807)	→	808
  41(296)	→	297
  41(828)	→	829
  41(290)	→	291
  41(161)	→	162
  41(129)	→	130
  41(236)	→	237
  41(1101)	→	1102
  41(131)	→	132
  41(227)	→	228
  41(207)	→	208
  41(50)	→	51
  41(1058)	→	1059
  41(606)	→	607
  41(375)	→	376
  41(951)	→	952
  41(337)	→	338
  41(352)	→	353
  41(605)	→	606
  41(315)	→	316
  41(51)	→	52
  41(151)	→	152
  41(32)	→	33
  41(993)	→	994
  41(248)	→	249
  41(257)	→	258
  41(18)	→	19
  41(443)	→	444
  41(251)	→	252
  41(305)	→	306
  41(883)	→	884
  41(1054)	→	1055
  41(125)	→	126
  41(127)	→	128
  41(945)	→	946
  41(182)	→	183
  41(260)	→	261
  41(188)	→	189
  41(317)	→	318
  41(857)	→	858
  41(977)	→	978
  41(1056)	→	1057
  41(209)	→	210
  41(99)	→	100
  41(299)	→	300
  41(233)	→	234
  41(199)	→	200
  41(954)	→	955
  41(894)	→	895
  41(855)	→	856
  41(355)	→	356
  41(836)	→	837
  41(181)	→	182
  50(7)	→	7
  40(7)	→	7
  30(7)	→	7
  11(29)	→	30
  11(868)	→	869
  11(1013)	→	1014
  11(287)	→	288
  11(244)	→	245
  11(135)	→	136
  11(327)	→	328
  11(374)	→	375
  11(870)	→	871
  11(342)	→	343
  11(499)	→	500
  11(164)	→	165
  11(498)	→	499
  11(98)	→	99
  11(349)	→	350
  11(500)	→	501
  11(63)	→	64
  11(952)	→	953
  11(222)	→	223
  11(230)	→	231
  11(136)	→	137
  11(152)	→	153
  11(297)	→	298
  11(27)	→	28
  11(763)	→	764
  11(66)	→	67
  11(575)	→	576
  11(867)	→	868
  11(28)	→	29
  11(184)	→	185
  11(1046)	→	1047
  11(376)	→	377
  11(220)	→	221
  11(385)	→	386
  11(348)	→	349
  11(983)	→	984
  11(984)	→	985
  11(107)	→	108
  11(1048)	→	1049
  11(194)	→	195
  11(350)	→	351
  11(314)	→	315
  11(888)	→	889
  11(16)	→	17
  11(762)	→	763
  11(319)	→	320
  11(1163)	→	1164
  11(1012)	→	1013
  11(806)	→	807
  11(785)	→	786
  11(133)	→	134
  11(577)	→	578
  11(808)	→	809
  11(835)	→	836
  11(869)	→	870
  11(65)	→	66
  11(1125)	→	1126
  11(34)	→	35
  11(958)	→	959
  11(995)	→	996
  11(183)	→	184
  11(144)	→	145
  11(382)	→	383
  11(79)	→	80
  11(134)	→	135
  11(778)	→	779
  11(890)	→	891
  11(33)	→	34
  11(228)	→	229
  11(1119)	→	1120
  11(328)	→	329
  11(303)	→	304
  11(91)	→	92
  11(959)	→	960
  11(772)	→	773
  11(253)	→	254
  11(71)	→	72
  11(1011)	→	1012
  11(768)	→	769
  11(371)	→	372
  11(200)	→	201
  51(224)	→	225
  51(70)	→	71
  51(262)	→	263
  51(132)	→	133
  51(48)	→	49
  51(261)	→	262
  51(331)	→	332
  51(77)	→	78
  51(353)	→	354
  51(105)	→	106
  51(764)	→	765
  51(96)	→	97
  51(189)	→	190
  51(1121)	→	1122
  51(265)	→	266
  51(266)	→	267
  51(335)	→	336
  51(603)	→	604
  51(247)	→	248
  51(780)	→	781
  51(198)	→	199
  51(232)	→	233
  51(1105)	→	1106
  51(157)	→	158
  51(270)	→	271
  51(341)	→	342
  51(92)	→	93
  51(1014)	→	1015
  51(211)	→	212
  51(1082)	→	1083
  51(786)	→	787
  51(190)	→	191
  51(933)	→	934
  51(1103)	→	1104
  51(804)	→	805
  51(214)	→	215
  51(840)	→	841
  51(206)	→	207
  51(109)	→	110
  51(1084)	→	1085
  51(165)	→	166
  51(990)	→	991
  51(833)	→	834
  51(306)	→	307
  51(80)	→	81
  51(74)	→	75
  51(810)	→	811
  51(216)	→	217
  51(344)	→	345
  51(162)	→	163
  51(783)	→	784
  51(177)	→	178
  51(944)	→	945
  51(1107)	→	1108
  51(30)	→	31
  51(987)	→	988
  51(316)	→	317
  51(334)	→	335
  51(1022)	→	1023
  51(231)	→	232
  51(496)	→	497
  51(149)	→	150
  51(326)	→	327
  51(1052)	→	1053
  51(997)	→	998
  51(234)	→	235
  51(767)	→	768
  51(787)	→	788
  51(501)	→	502
  51(1001)	→	1002
  51(313)	→	314
  51(991)	→	992
  51(996)	→	997
  51(289)	→	290
  51(67)	→	68
  51(25)	→	26
  51(153)	→	154
  51(1009)	→	1010
  51(377)	→	378
  51(1038)	→	1039
  51(895)	→	896
  51(837)	→	838
  10(7)	→	7
  00(7)	→	7
  01(187)	→	188
  01(225)	→	226
  01(94)	→	95
  01(497)	→	498
  01(887)	→	888
  01(351)	→	352
  01(1064)	→	1065
  01(332)	→	333
  01(1165)	→	1166
  01(338)	→	339
  01(345)	→	346
  01(212)	→	213
  01(779)	→	780
  01(988)	→	989
  01(854)	→	855
  01(146)	→	147
  01(263)	→	264
  01(1066)	→	1067
  01(986)	→	987
  01(1010)	→	1011
  01(372)	→	373
  01(900)	→	901
  01(102)	→	103
  01(226)	→	227
  01(267)	→	268
  01(12)	→	13
  01(193)	→	194
  01(325)	→	326
  01(288)	→	289
  01(229)	→	230
  01(356)	→	357
  01(898)	→	899
  01(35)	→	36
  01(1080)	→	1081
  01(73)	→	74
  01(1062)	→	1063
  01(943)	→	944
  01(805)	→	806
  01(124)	→	125
  01(215)	→	216
  01(43)	→	44
  01(150)	→	151
  01(892)	→	893
  01(1167)	→	1168
  01(53)	→	54
  01(176)	→	177
  01(1060)	→	1061
  01(953)	→	954
  01(208)	→	209
  01(994)	→	995
  01(19)	→	20
  01(298)	→	299
  01(896)	→	897
  01(830)	→	831
  01(156)	→	157
  01(370)	→	371
  01(123)	→	124
  01(218)	→	219
  01(255)	→	256
  01(195)	→	196
  01(97)	→	98
  01(160)	→	161
  01(381)	→	382
  01(444)	→	445
  01(26)	→	27
  01(330)	→	331
  01(120)	→	121
  01(42)	→	43
  01(293)	→	294
  01(311)	→	312
  01(608)	→	609
  01(853)	→	854
  01(192)	→	193
  01(948)	→	949
  01(118)	→	119
  21(235)	→	236
  21(992)	→	993
  21(383)	→	384
  21(36)	→	37
  21(44)	→	45
  21(268)	→	269
  21(271)	→	272
  21(583)	→	584
  21(931)	→	932
  21(17)	→	18
  21(1113)	→	1114
  21(254)	→	255
  21(1115)	→	1116
  21(180)	→	181
  21(1109)	→	1110
  21(347)	→	348
  21(340)	→	341
  21(159)	→	160
  21(163)	→	164
  21(223)	→	224
  21(781)	→	782
  21(191)	→	192
  21(947)	→	948
  21(137)	→	138
  21(856)	→	857
  21(264)	→	265
  21(252)	→	253
  21(178)	→	179
  21(336)	→	337
  21(607)	→	608
  21(269)	→	270
  21(829)	→	830
  21(186)	→	187
  21(941)	→	942
  21(386)	→	387
  21(1099)	→	1100
  21(1111)	→	1112
  21(292)	→	293
  21(76)	→	77
  21(158)	→	159
  21(863)	→	864
  21(46)	→	47
  21(312)	→	313
  21(93)	→	94
  21(75)	→	76
  21(784)	→	785
  21(197)	→	198
  21(101)	→	102
  21(126)	→	127
  21(242)	→	243
  21(117)	→	118
  21(245)	→	246
  21(54)	→	55
  21(442)	→	443
  21(939)	→	940
  21(782)	→	783
  21(213)	→	214
  21(78)	→	79
  21(119)	→	120
  21(52)	→	53
  20(7)	→	7