Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/96370)

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:

  503	→	485
  272	→	712
  272	→	750
  23	→	529
  23	→	798
  239	→	716
  329	→	19
  376	→	26
  964	→	122
  486	→	304
  80	→	287
  80	→	706
  80	→	834
  1156	→	35
  715	→	72
  715	→	112
  715	→	811
  715	→	56
  715	→	271
  715	→	78
  715	→	22
  715	→	15
  715	→	37
  715	→	241
  715	→	7
  715	→	38
  715	→	700
  715	→	35
  715	→	1026
  98	→	7
  98	→	165
  98	→	48
  98	→	17
  98	→	111
  98	→	16
  98	→	72
  98	→	73
  98	→	56
  98	→	38
  98	→	36
  98	→	361
  98	→	200
  98	→	1018
  98	→	1150
  286	→	219
  97	→	739
  97	→	832
  97	→	868
  97	→	909
  15	→	937
  781	→	72
  781	→	73
  781	→	271
  781	→	78
  781	→	22
  781	→	15
  781	→	37
  781	→	241
  781	→	7
  781	→	56
  781	→	38
  781	→	36
  781	→	361
  781	→	200
  781	→	1018
  781	→	1150
  96	→	813
  129	→	27
  530	→	862
  728	→	165
  728	→	48
  728	→	7
  728	→	17
  728	→	111
  728	→	16
  167	→	227
  998	→	242
  1097	→	49
  1107	→	48
  119	→	35
  145	→	54
  1160	→	35
  1158	→	35
  610	→	72
  610	→	73
  610	→	271
  610	→	78
  610	→	22
  610	→	15
  610	→	37
  610	→	241
  610	→	7
  610	→	56
  610	→	38
  610	→	360
  610	→	112
  610	→	111
  610	→	165
  610	→	700
  610	→	35
  610	→	1026
  610	→	48
  610	→	16
  610	→	199
  610	→	36
  610	→	1150
  705	→	54
  1103	→	20
  39	→	99
  39	→	7
  39	→	242
  1104	→	1157
  812	→	180
  907	→	1151
  805	→	179
  740	→	864
  914	→	165
  914	→	48
  914	→	271
  914	→	78
  914	→	22
  914	→	15
  914	→	37
  914	→	241
  914	→	7
  914	→	111
  914	→	16
  209	→	724
  1124	→	1159
  765	→	48
  55	→	7
  55	→	165
  55	→	48
  55	→	111
  55	→	16
  55	→	17
  55	→	138
  55	→	180
  55	→	812
  255	→	18
  1095	→	48
  1095	→	1102
  749	→	165
  749	→	48
  749	→	7
  749	→	180
  749	→	111
  749	→	16
  749	→	812
  20	→	714
  20	→	1124
  304	→	484
  304	→	856
  713	→	58
  713	→	815
  62	→	27
  942	→	27
  938	→	79
  49	→	136
  49	→	385
  380	→	136
  380	→	208
  380	→	178
  380	→	7
  380	→	18
  380	→	195
  380	→	79
  380	→	49
  1105	→	23
  40	→	271
  40	→	78
  40	→	22
  40	→	15
  40	→	37
  40	→	241
  40	→	7
  40	→	932
  1026	→	35
  936	→	35
  305	→	766
  305	→	768
  1022	→	35
  755	→	189
  833	→	242
  940	→	27
  222	→	53
  222	→	802
  1154	→	35
  723	→	79
  609	→	935
  748	→	905
  748	→	989
  748	→	1021
  73	→	91
  73	→	330
  73	→	1017
  38	→	56
  38	→	72
  38	→	811
  38	→	903
  38	→	991
  86	→	27
  816	→	198
  1030	→	869
  79	→	178
  79	→	195
  79	→	208
  79	→	377
  1099	→	57
  36	→	7
  36	→	165
  36	→	48
  36	→	111
  36	→	16
  36	→	72
  36	→	112
  36	→	56
  36	→	38
  36	→	73
  36	→	199
  36	→	700
  36	→	35
  36	→	1026
  36	→	1150
  994	→	208
  916	→	910
  177	→	118
  21	→	7
  21	→	136
  21	→	208
  21	→	178
  21	→	18
  21	→	195
  21	→	79
  21	→	49
  21	→	72
  21	→	73
  21	→	56
  21	→	38
  21	→	23
  21	→	165
  21	→	48
  21	→	111
  21	→	16
  21	→	272
  21	→	753
  21	→	938
  21	→	360
  21	→	112
  21	→	700
  21	→	35
  21	→	1026
  21	→	199
  21	→	36
  21	→	904
  21	→	962
  21	→	1150
  912	→	1094
  532	→	165
  532	→	48
  532	→	271
  532	→	78
  532	→	22
  532	→	15
  532	→	37
  532	→	241
  532	→	7
  532	→	111
  532	→	16
  207	→	85
  918	→	910
  726	→	985
  1032	→	869
  1042	→	360
  1042	→	112
  1042	→	111
  1042	→	165
  1042	→	991
  1042	→	811
  1042	→	56
  1042	→	700
  1042	→	73
  1042	→	7
  1042	→	35
  1042	→	1026
  1042	→	72
  1042	→	903
  1042	→	38
  1042	→	48
  1042	→	16
  1042	→	199
  1042	→	36
  1042	→	1150
  986	→	105
  54	→	722
  799	→	168
  1037	→	1104
  22	→	1025
  1041	→	1155
  386	→	378
  1131	→	79
  1101	→	27
  831	→	208
  906	→	23
  717	→	79
  803	→	179
  1036	→	1098
  1036	→	1100
  859	→	35
  859	→	1027
  863	→	330
  814	→	196
  28	→	7
  28	→	99
  28	→	242
  28	→	39
  28	→	165
  28	→	48
  28	→	180
  28	→	111
  28	→	16
  28	→	208
  28	→	178
  28	→	195
  28	→	79
  28	→	378
  28	→	812
  28	→	753
  28	→	815
  28	→	58
  28	→	713
  28	→	938
  118	→	764
  1018	→	73
  1150	→	35
  904	→	23
  106	→	27
  379	→	933
  16	→	48
  16	→	111
  16	→	165
  16	→	271
  16	→	78
  16	→	22
  16	→	15
  16	→	37
  16	→	241
  16	→	7
  913	→	1035
  887	→	907
  887	→	993
  887	→	1023
  348	→	27
  306	→	7
  306	→	136
  306	→	208
  306	→	178
  306	→	195
  306	→	79
  306	→	49
  306	→	938
  306	→	932
  1125	→	23
  112	→	360
  77	→	54
  77	→	804
  100	→	120
  7	→	15
  7	→	22
  7	→	37
  7	→	78
  7	→	241
  7	→	271
  934	→	35
  962	→	122
  189	→	1106
  35	→	700
  240	→	189
  990	→	208
  531	→	931
  707	→	703
  908	→	23
  905	→	1153
  727	→	917
  727	→	941
  727	→	997
  727	→	1031
  190	→	20
  1148	→	35
  154	→	96
  865	→	330
  74	→	146
  74	→	315
  932	→	49
  1028	→	331
  903	→	1149
  24	→	33
  24	→	961
  24	→	1015
  328	→	1130
  1016	→	275
  910	→	1147
  43	→	20
  43	→	1096
  1152	→	35
  27	→	502
  27	→	830
  27	→	858
  888	→	208
  888	→	178
  888	→	271
  888	→	78
  888	→	22
  888	→	15
  888	→	37
  888	→	241
  888	→	7
  888	→	195
  888	→	79
  888	→	815
  888	→	58
  888	→	713
  888	→	938
  767	→	48
  166	→	605
  992	→	208
  996	→	242
  780	→	915
  780	→	939
  780	→	995
  780	→	1029
  849	→	347
  228	→	963
  1024	→	35
  857	→	35
  41(123)	→	124
  41(874)	→	875
  41(186)	→	187
  41(56)	→	57
  41(187)	→	188
  41(339)	→	340
  41(82)	→	83
  41(371)	→	372
  41(778)	→	779
  41(963)	→	964
  41(218)	→	219
  41(140)	→	141
  41(370)	→	371
  41(153)	→	154
  41(195)	→	196
  41(848)	→	849
  41(238)	→	239
  41(73)	→	74
  41(282)	→	283
  41(102)	→	103
  41(289)	→	290
  41(1098)	→	1099
  41(985)	→	986
  41(835)	→	836
  41(212)	→	213
  41(342)	→	343
  41(332)	→	333
  41(59)	→	60
  41(834)	→	835
  41(52)	→	53
  41(378)	→	379
  41(840)	→	841
  41(364)	→	365
  41(183)	→	184
  41(122)	→	123
  41(609)	→	610
  41(204)	→	205
  41(213)	→	214
  41(1041)	→	1042
  41(112)	→	113
  41(379)	→	380
  41(230)	→	231
  41(744)	→	745
  41(880)	→	881
  41(770)	→	771
  41(704)	→	705
  41(128)	→	129
  41(317)	→	318
  41(881)	→	882
  41(961)	→	962
  41(813)	→	814
  41(20)	→	21
  41(288)	→	289
  41(139)	→	140
  41(334)	→	335
  41(175)	→	176
  41(19)	→	20
  41(302)	→	303
  41(294)	→	295
  41(284)	→	285
  41(121)	→	122
  41(254)	→	255
  41(271)	→	272
  41(278)	→	279
  12(911)	→	912
  12(913)	→	914
  02(912)	→	913
  51(235)	→	236
  51(208)	→	209
  51(365)	→	366
  51(727)	→	728
  51(322)	→	323
  51(1124)	→	1125
  51(93)	→	94
  51(1104)	→	1105
  51(148)	→	149
  51(295)	→	296
  51(58)	→	59
  51(323)	→	324
  51(326)	→	327
  51(22)	→	23
  51(201)	→	202
  51(841)	→	842
  51(217)	→	218
  51(227)	→	228
  51(250)	→	251
  51(273)	→	274
  51(905)	→	906
  51(124)	→	125
  51(484)	→	485
  51(23)	→	24
  51(166)	→	167
  51(333)	→	334
  51(773)	→	774
  51(485)	→	486
  51(346)	→	347
  51(872)	→	873
  51(176)	→	177
  51(125)	→	126
  51(362)	→	363
  51(907)	→	908
  51(780)	→	781
  51(188)	→	189
  51(206)	→	207
  51(338)	→	339
  51(272)	→	273
  51(903)	→	904
  51(99)	→	100
  51(299)	→	300
  51(184)	→	185
  51(845)	→	846
  51(502)	→	503
  51(875)	→	876
  51(61)	→	62
  51(97)	→	98
  51(316)	→	317
  51(120)	→	121
  51(741)	→	742
  30(7)	→	7
  50(7)	→	7
  40(7)	→	7
  31(843)	→	844
  31(846)	→	847
  31(753)	→	754
  31(246)	→	247
  31(296)	→	297
  31(882)	→	883
  31(740)	→	741
  31(372)	→	373
  31(871)	→	872
  31(335)	→	336
  31(368)	→	369
  31(141)	→	142
  31(844)	→	845
  31(297)	→	298
  31(27)	→	28
  31(60)	→	61
  31(304)	→	305
  31(241)	→	242
  31(343)	→	344
  31(275)	→	276
  31(220)	→	221
  31(385)	→	386
  31(285)	→	286
  31(181)	→	182
  31(997)	→	998
  31(116)	→	117
  31(298)	→	299
  31(887)	→	888
  31(319)	→	320
  31(165)	→	166
  31(81)	→	82
  31(878)	→	879
  31(173)	→	174
  31(832)	→	833
  31(18)	→	19
  31(995)	→	996
  31(144)	→	145
  31(247)	→	248
  31(85)	→	86
  31(24)	→	25
  31(126)	→	127
  31(361)	→	362
  31(38)	→	39
  31(300)	→	301
  31(331)	→	332
  31(842)	→	843
  31(205)	→	206
  31(228)	→	229
  31(746)	→	747
  31(748)	→	749
  31(91)	→	92
  31(233)	→	234
  31(377)	→	378
  31(104)	→	105
  31(325)	→	326
  31(75)	→	76
  31(1036)	→	1037
  31(200)	→	201
  11(138)	→	139
  11(742)	→	743
  11(180)	→	181
  11(935)	→	936
  11(1155)	→	1156
  11(606)	→	607
  11(236)	→	237
  11(750)	→	751
  11(869)	→	870
  11(1100)	→	1101
  11(293)	→	294
  11(321)	→	322
  11(197)	→	198
  11(72)	→	73
  11(1153)	→	1154
  11(198)	→	199
  11(531)	→	532
  11(1039)	→	1040
  11(883)	→	884
  11(172)	→	173
  11(864)	→	865
  11(802)	→	803
  11(862)	→	863
  11(253)	→	254
  11(40)	→	41
  11(341)	→	342
  11(870)	→	871
  11(202)	→	203
  11(939)	→	940
  11(211)	→	212
  11(243)	→	244
  11(933)	→	934
  11(360)	→	361
  11(804)	→	805
  11(50)	→	51
  11(199)	→	200
  11(1151)	→	1152
  11(1025)	→	1026
  11(1159)	→	1160
  11(324)	→	325
  11(117)	→	118
  11(373)	→	374
  11(769)	→	770
  11(216)	→	217
  11(1147)	→	1148
  11(768)	→	769
  11(318)	→	319
  11(1035)	→	1036
  11(111)	→	112
  11(1157)	→	1158
  11(113)	→	114
  11(281)	→	282
  11(26)	→	27
  11(41)	→	42
  11(142)	→	143
  11(941)	→	942
  11(886)	→	887
  11(170)	→	171
  11(1149)	→	1150
  11(37)	→	38
  11(168)	→	169
  11(839)	→	840
  11(739)	→	740
  11(35)	→	36
  11(1021)	→	1022
  11(529)	→	530
  11(858)	→	859
  11(815)	→	816
  11(754)	→	755
  11(244)	→	245
  11(856)	→	857
  11(33)	→	34
  11(136)	→	137
  11(714)	→	715
  11(1017)	→	1018
  11(1102)	→	1103
  11(178)	→	179
  11(315)	→	316
  11(219)	→	220
  11(100)	→	101
  11(1023)	→	1024
  11(702)	→	703
  11(607)	→	608
  11(1038)	→	1039
  11(706)	→	707
  11(209)	→	210
  00(7)	→	7
  10(7)	→	7
  21(92)	→	93
  21(101)	→	102
  21(1015)	→	1016
  21(76)	→	77
  21(237)	→	238
  21(17)	→	18
  21(989)	→	990
  21(774)	→	775
  21(127)	→	128
  21(993)	→	994
  21(776)	→	777
  21(345)	→	346
  21(279)	→	280
  21(232)	→	233
  21(779)	→	780
  21(716)	→	717
  21(114)	→	115
  21(726)	→	727
  21(105)	→	106
  21(305)	→	306
  21(290)	→	291
  21(276)	→	277
  21(189)	→	190
  21(937)	→	938
  21(49)	→	50
  21(221)	→	222
  21(234)	→	235
  21(798)	→	799
  21(248)	→	249
  21(1037)	→	1038
  21(367)	→	368
  21(249)	→	250
  21(991)	→	992
  21(366)	→	367
  21(167)	→	168
  21(1130)	→	1131
  21(336)	→	337
  21(147)	→	148
  21(245)	→	246
  21(79)	→	80
  21(151)	→	152
  21(152)	→	153
  21(78)	→	79
  21(48)	→	49
  21(196)	→	197
  21(722)	→	723
  21(215)	→	216
  21(252)	→	253
  21(772)	→	773
  21(274)	→	275
  21(725)	→	726
  21(74)	→	75
  21(1096)	→	1097
  21(149)	→	150
  21(605)	→	606
  21(337)	→	338
  21(743)	→	744
  21(327)	→	328
  21(700)	→	701
  21(830)	→	831
  21(57)	→	58
  21(836)	→	837
  21(39)	→	40
  21(777)	→	778
  21(95)	→	96
  21(877)	→	878
  21(231)	→	232
  21(751)	→	752
  21(171)	→	172
  21(320)	→	321
  21(185)	→	186
  21(287)	→	288
  21(931)	→	932
  21(96)	→	97
  21(25)	→	26
  21(712)	→	713
  21(747)	→	748
  21(701)	→	702
  21(174)	→	175
  21(210)	→	211
  21(182)	→	183
  21(876)	→	877
  21(118)	→	119
  01(53)	→	54
  01(1040)	→	1041
  01(277)	→	278
  01(766)	→	767
  01(879)	→	880
  01(80)	→	81
  01(103)	→	104
  01(291)	→	292
  01(374)	→	375
  01(16)	→	17
  01(344)	→	345
  01(347)	→	348
  01(340)	→	341
  01(703)	→	704
  01(775)	→	776
  01(1106)	→	1107
  01(328)	→	329
  01(115)	→	116
  01(84)	→	85
  01(1027)	→	1028
  01(752)	→	753
  01(169)	→	170
  01(868)	→	869
  01(764)	→	765
  01(1029)	→	1030
  01(137)	→	138
  01(363)	→	364
  01(203)	→	204
  01(229)	→	230
  01(179)	→	180
  01(608)	→	609
  01(811)	→	812
  01(724)	→	725
  01(51)	→	52
  01(847)	→	848
  01(42)	→	43
  01(885)	→	886
  01(771)	→	772
  01(838)	→	839
  01(292)	→	293
  01(745)	→	746
  01(150)	→	151
  01(530)	→	531
  01(94)	→	95
  01(1094)	→	1095
  01(34)	→	35
  01(375)	→	376
  01(15)	→	16
  01(146)	→	147
  01(1031)	→	1032
  01(143)	→	144
  01(301)	→	302
  01(873)	→	874
  01(330)	→	331
  01(369)	→	370
  01(242)	→	243
  01(83)	→	84
  01(280)	→	281
  01(303)	→	304
  01(54)	→	55
  01(837)	→	838
  01(251)	→	252
  01(214)	→	215
  01(884)	→	885
  01(283)	→	284
  01(239)	→	240
  20(7)	→	7
  52(909)	→	910
  52(910)	→	911
  52(915)	→	916
  52(917)	→	918