Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/65081)

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(☐), 3(☐), 4(☐), 5(☐)}

1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1 Bounds

• final states:

  {1}

• transitions:

  272	→	1
  272	→	400
  272	→	450
  339	→	643
  364	→	277
  221	→	387
  221	→	451
  280	→	1
  280	→	196
  280	→	495
  591	→	661
  591	→	667
  846	→	404
  25	→	987
  25	→	993
  733	→	971
  733	→	985
  32	→	4
  263	→	873
  263	→	933
  750	→	222
  271	→	705
  271	→	797
  338	→	1
  338	→	16
  338	→	956
  80	→	1
  80	→	296
  80	→	220
  80	→	254
  80	→	256
  80	→	211
  80	→	744
  98	→	37
  229	→	757
  229	→	883
  229	→	939
  874	→	509
  742	→	172
  97	→	637
  97	→	645
  734	→	26
  734	→	358
  571	→	863
  886	→	509
  96	→	947
  956	→	92
  706	→	100
  436	→	400
  122	→	100
  668	→	620
  878	→	509
  638	→	4
  676	→	92
  18	→	4
  978	→	221
  50	→	34
  988	→	509
  652	→	4
  218	→	177
  218	→	847
  772	→	357
  617	→	953
  980	→	309
  646	→	620
  108	→	1
  108	→	139
  108	→	4
  108	→	26
  914	→	900
  5	→	899
  147	→	737
  147	→	871
  37	→	65
  37	→	71
  37	→	73
  37	→	79
  37	→	81
  592	→	37
  34	→	209
  34	→	509
  65	→	875
  65	→	935
  319	→	715
  319	→	805
  618	→	307
  130	→	100
  130	→	771
  130	→	807
  107	→	751
  107	→	885
  107	→	941
  942	→	140
  938	→	140
  246	→	220
  1	→	3
  1	→	15
  1	→	17
  1	→	23
  1	→	25
  1	→	31
  1	→	33
  1	→	47
  1	→	49
  1	→	55
  1	→	57
  1	→	63
  1	→	99
  1	→	121
  1	→	123
  1	→	129
  1	→	131
  1	→	137
  1	→	169
  1	→	179
  1	→	185
  1	→	187
  1	→	193
  1	→	195
  1	→	219
  1	→	245
  1	→	247
  1	→	253
  1	→	255
  1	→	261
  1	→	399
  1	→	433
  1	→	435
  1	→	441
  1	→	443
  1	→	449
  654	→	4
  936	→	140
  71	→	635
  716	→	100
  940	→	140
  524	→	37
  884	→	509
  73	→	707
  73	→	799
  26	→	4
  26	→	449
  26	→	441
  26	→	433
  26	→	261
  26	→	253
  26	→	245
  26	→	195
  26	→	187
  26	→	179
  26	→	137
  26	→	129
  26	→	121
  26	→	63
  26	→	55
  26	→	47
  26	→	31
  26	→	23
  26	→	15
  26	→	3
  26	→	17
  26	→	25
  26	→	33
  26	→	49
  26	→	57
  26	→	99
  26	→	123
  26	→	131
  26	→	169
  26	→	185
  26	→	193
  26	→	219
  26	→	247
  26	→	255
  26	→	399
  26	→	435
  26	→	443
  26	→	1
  38	→	1
  38	→	509
  38	→	209
  38	→	34
  38	→	56
  38	→	58
  38	→	988
  269	→	629
  662	→	4
  783	→	319
  58	→	34
  36	→	616
  36	→	619
  170	→	494
  760	→	298
  994	→	140
  248	→	220
  177	→	653
  177	→	851
  186	→	170
  72	→	1
  72	→	100
  72	→	35
  72	→	130
  72	→	401
  72	→	132
  72	→	728
  72	→	994
  912	→	591
  141	→	931
  138	→	100
  178	→	1
  178	→	573
  178	→	100
  178	→	138
  178	→	130
  178	→	401
  178	→	728
  178	→	982
  178	→	142
  844	→	401
  346	→	1
  346	→	355
  346	→	400
  346	→	434
  346	→	93
  171	→	449
  171	→	441
  171	→	433
  171	→	261
  171	→	253
  171	→	245
  171	→	195
  171	→	187
  171	→	179
  171	→	137
  171	→	129
  171	→	121
  171	→	63
  171	→	55
  171	→	47
  171	→	31
  171	→	23
  171	→	15
  171	→	3
  171	→	17
  171	→	25
  171	→	33
  171	→	49
  171	→	57
  171	→	99
  171	→	123
  171	→	131
  171	→	169
  171	→	185
  171	→	193
  171	→	219
  171	→	247
  171	→	255
  171	→	399
  171	→	435
  171	→	443
  171	→	1
  6	→	675
  6	→	761
  337	→	877
  337	→	937
  220	→	296
  345	→	713
  345	→	803
  986	→	509
  982	→	309
  308	→	1
  308	→	139
  308	→	6
  308	→	92
  308	→	4
  124	→	100
  230	→	6
  230	→	263
  230	→	269
  230	→	271
  230	→	277
  230	→	279
  764	→	309
  270	→	1
  270	→	138
  270	→	982
  264	→	1
  264	→	32
  264	→	962
  82	→	1
  82	→	170
  82	→	510
  82	→	188
  82	→	558
  82	→	194
  82	→	297
  180	→	170
  872	→	509
  686	→	945
  954	→	92
  4	→	92
  4	→	139
  804	→	220
  463	→	801
  463	→	843
  876	→	509
  400	→	743
  850	→	451
  188	→	170
  802	→	220
  508	→	1
  508	→	355
  508	→	400
  508	→	434
  508	→	93
  66	→	1
  66	→	311
  66	→	24
  66	→	26
  16	→	4
  93	→	355
  93	→	845
  972	→	140
  348	→	1
  348	→	296
  348	→	220
  348	→	246
  348	→	211
  348	→	254
  348	→	744
  63	→	961
  63	→	981
  306	→	677
  800	→	220
  623	→	5
  738	→	140
  684	→	92
  636	→	4
  450	→	400
  708	→	100
  100	→	309
  100	→	573
  100	→	671
  672	→	36
  7	→	1
  7	→	48
  7	→	5
  7	→	64
  7	→	511
  758	→	221
  934	→	140
  678	→	92
  444	→	400
  444	→	749
  444	→	857
  806	→	220
  962	→	92
  64	→	34
  64	→	449
  64	→	441
  64	→	433
  64	→	261
  64	→	253
  64	→	245
  64	→	195
  64	→	187
  64	→	179
  64	→	137
  64	→	129
  64	→	121
  64	→	63
  64	→	55
  64	→	47
  64	→	31
  64	→	23
  64	→	15
  64	→	3
  64	→	17
  64	→	25
  64	→	33
  64	→	49
  64	→	57
  64	→	99
  64	→	123
  64	→	131
  64	→	169
  64	→	185
  64	→	193
  64	→	219
  64	→	247
  64	→	255
  64	→	399
  64	→	435
  64	→	443
  64	→	1
  630	→	4
  752	→	221
  434	→	400
  310	→	557
  310	→	727
  948	→	573
  278	→	1
  278	→	262
  278	→	171
  278	→	246
  256	→	220
  572	→	1
  572	→	296
  572	→	220
  48	→	34
  48	→	1
  414	→	1
  414	→	509
  414	→	34
  414	→	64
  47	→	955
  47	→	979
  946	→	574
  714	→	100
  398	→	1
  398	→	196
  398	→	495
  870	→	509
  254	→	220
  464	→	347
  148	→	1
  148	→	26
  148	→	358
  762	→	309
  413	→	683
  413	→	763
  858	→	452
  320	→	337
  320	→	339
  320	→	345
  320	→	347
  320	→	353
  693	→	25
  693	→	977
  340	→	1
  340	→	122
  340	→	140
  340	→	980
  523	→	651
  523	→	659
  523	→	849
  132	→	100
  744	→	211
  74	→	1
  74	→	210
  74	→	400
  74	→	442
  74	→	451
  74	→	444
  74	→	387
  74	→	221
  848	→	451
  932	→	558
  24	→	4
  852	→	451
  660	→	620
  354	→	1
  354	→	494
  354	→	170
  354	→	180
  507	→	685
  507	→	773
  194	→	170
  194	→	759
  442	→	400
  321	→	1
  321	→	48
  321	→	5
  798	→	220
  56	→	34
  864	→	495
  644	→	4
  262	→	220
  262	→	741
  819	→	63
  196	→	170
  196	→	449
  196	→	441
  196	→	433
  196	→	261
  196	→	253
  196	→	245
  196	→	195
  196	→	187
  196	→	179
  196	→	137
  196	→	129
  196	→	121
  196	→	63
  196	→	55
  196	→	47
  196	→	31
  196	→	23
  196	→	15
  196	→	3
  196	→	17
  196	→	25
  196	→	33
  196	→	49
  196	→	57
  196	→	99
  196	→	123
  196	→	131
  196	→	169
  196	→	185
  196	→	193
  196	→	219
  196	→	247
  196	→	255
  196	→	399
  196	→	435
  196	→	443
  196	→	1
  307	→	869
  307	→	913
  130(1)	→	1
  031(174)	→	175
  031(393)	→	394
  031(55)	→	56
  031(877)	→	878
  031(320)	→	321
  031(306)	→	307
  031(781)	→	782
  551(195)	→	196
  551(397)	→	398
  551(570)	→	571
  551(494)	→	495
  551(863)	→	864
  551(590)	→	591
  141(146)	→	147
  141(25)	→	26
  141(357)	→	358
  141(520)	→	521
  141(651)	→	652
  141(229)	→	230
  141(107)	→	108
  141(459)	→	460
  141(732)	→	733
  141(518)	→	519
  141(653)	→	654
  230(1)	→	1
  140(1)	→	1
  400(1)	→	1
  311(780)	→	781
  311(460)	→	461
  311(402)	→	403
  311(776)	→	777
  311(271)	→	272
  311(433)	→	434
  311(502)	→	503
  311(102)	→	103
  311(688)	→	689
  311(92)	→	93
  311(521)	→	522
  311(808)	→	809
  311(392)	→	393
  311(388)	→	389
  051(513)	→	514
  051(63)	→	64
  051(413)	→	414
  051(454)	→	455
  051(510)	→	511
  431(210)	→	211
  431(522)	→	523
  431(347)	→	348
  431(253)	→	254
  431(461)	→	462
  431(803)	→	804
  431(176)	→	177
  431(743)	→	744
  431(801)	→	802
  131(809)	→	810
  131(501)	→	502
  131(337)	→	338
  131(845)	→	846
  131(310)	→	311
  131(643)	→	644
  131(775)	→	776
  131(677)	→	678
  131(387)	→	388
  131(637)	→	638
  131(23)	→	24
  131(403)	→	404
  401(219)	→	220
  401(813)	→	814
  401(588)	→	589
  401(517)	→	518
  401(407)	→	408
  401(773)	→	774
  401(511)	→	512
  511(453)	→	454
  511(358)	→	359
  511(579)	→	580
  511(279)	→	280
  511(179)	→	180
  020(1)	→	1
  251(94)	→	95
  251(568)	→	569
  251(137)	→	138
  251(495)	→	496
  251(763)	→	764
  251(317)	→	318
  251(690)	→	691
  251(104)	→	105
  251(715)	→	716
  251(591)	→	592
  251(981)	→	982
  111(733)	→	734
  111(263)	→	264
  111(629)	→	630
  111(363)	→	364
  111(953)	→	954
  111(15)	→	16
  111(903)	→	904
  111(515)	→	516
  111(147)	→	148
  111(955)	→	956
  111(559)	→	560
  111(904)	→	905
  111(560)	→	561
  111(675)	→	676
  310(1)	→	1
  321(435)	→	436
  321(96)	→	97
  321(900)	→	901
  321(73)	→	74
  321(223)	→	224
  321(309)	→	310
  321(500)	→	501
  321(140)	→	141
  321(225)	→	226
  200(1)	→	1
  150(1)	→	1
  521(185)	→	186
  521(100)	→	101
  521(686)	→	687
  521(313)	→	314
  521(81)	→	82
  521(907)	→	908
  521(390)	→	391
  521(778)	→	779
  521(569)	→	570
  521(563)	→	564
  521(318)	→	319
  132(645)	→	646
  541(818)	→	819
  541(193)	→	194
  541(512)	→	513
  541(412)	→	413
  541(577)	→	578
  541(296)	→	297
  541(316)	→	317
  541(589)	→	590
  550(1)	→	1
  330(1)	→	1
  001(455)	→	456
  001(869)	→	870
  001(33)	→	34
  211(121)	→	122
  211(979)	→	980
  211(269)	→	270
  211(761)	→	762
  211(971)	→	972
  211(933)	→	934
  211(139)	→	140
  211(498)	→	499
  211(565)	→	566
  211(737)	→	738
  211(705)	→	706
  211(909)	→	910
  540(1)	→	1
  530(1)	→	1
  030(1)	→	1
  531(815)	→	816
  531(299)	→	300
  531(353)	→	354
  531(396)	→	397
  531(931)	→	932
  531(901)	→	902
  531(93)	→	94
  531(585)	→	586
  531(451)	→	452
  531(227)	→	228
  531(187)	→	188
  531(689)	→	690
  531(409)	→	410
  531(103)	→	104
  531(557)	→	558
  531(857)	→	858
  411(905)	→	906
  411(731)	→	732
  411(311)	→	312
  411(277)	→	278
  411(797)	→	798
  411(304)	→	305
  411(315)	→	316
  411(458)	→	459
  411(145)	→	146
  411(519)	→	520
  411(245)	→	246
  411(561)	→	562
  101(405)	→	406
  101(616)	→	617
  101(5)	→	6
  101(514)	→	515
  101(307)	→	308
  101(730)	→	731
  101(811)	→	812
  101(144)	→	145
  101(3)	→	4
  021(37)	→	38
  021(49)	→	50
  021(215)	→	216
  021(506)	→	507
  021(566)	→	567
  021(910)	→	911
  021(671)	→	672
  021(35)	→	36
  021(875)	→	876
  420(1)	→	1
  240(1)	→	1
  041(883)	→	884
  041(987)	→	988
  041(143)	→	144
  041(57)	→	58
  041(729)	→	730
  041(885)	→	886
  421(771)	→	772
  421(79)	→	80
  421(691)	→	692
  421(728)	→	729
  421(105)	→	106
  421(356)	→	357
  421(576)	→	577
  421(217)	→	218
  421(142)	→	143
  421(172)	→	173
  421(247)	→	248
  421(799)	→	800
  421(574)	→	575
  410(1)	→	1
  000(1)	→	1
  142(659)	→	660
  301(175)	→	176
  301(507)	→	508
  301(209)	→	210
  301(399)	→	400
  300(1)	→	1
  050(1)	→	1
  152(667)	→	668
  320(1)	→	1
  351(319)	→	320
  351(395)	→	396
  351(297)	→	298
  351(759)	→	760
  351(359)	→	360
  351(583)	→	584
  351(449)	→	450
  441(106)	→	107
  441(411)	→	412
  441(817)	→	818
  441(255)	→	256
  441(692)	→	693
  040(1)	→	1
  151(314)	→	315
  151(558)	→	559
  151(578)	→	579
  151(457)	→	458
  151(687)	→	688
  151(661)	→	662
  151(101)	→	102
  151(586)	→	587
  151(908)	→	909
  151(31)	→	32
  151(902)	→	903
  151(564)	→	565
  151(961)	→	962
  151(391)	→	392
  151(452)	→	453
  151(580)	→	581
  151(779)	→	780
  151(683)	→	684
  510(1)	→	1
  341(977)	→	978
  341(408)	→	409
  341(462)	→	463
  341(814)	→	815
  341(443)	→	444
  341(220)	→	221
  341(301)	→	302
  341(305)	→	306
  341(751)	→	752
  341(847)	→	848
  341(757)	→	758
  341(851)	→	852
  341(774)	→	775
  341(173)	→	174
  341(849)	→	850
  450(1)	→	1
  110(1)	→	1
  430(1)	→	1
  250(1)	→	1
  520(1)	→	1
  210(1)	→	1
  350(1)	→	1
  220(1)	→	1
  241(211)	→	212
  241(575)	→	576
  241(171)	→	172
  241(939)	→	940
  241(131)	→	132
  241(741)	→	742
  241(312)	→	313
  241(562)	→	563
  241(177)	→	178
  241(993)	→	994
  241(906)	→	907
  241(941)	→	942
  241(523)	→	524
  121(635)	→	636
  121(17)	→	18
  121(497)	→	498
  121(65)	→	66
  121(401)	→	402
  121(807)	→	808
  121(303)	→	304
  121(362)	→	363
  440(1)	→	1
  451(300)	→	301
  451(816)	→	817
  451(228)	→	229
  451(805)	→	806
  451(571)	→	572
  451(261)	→	262
  451(170)	→	171
  451(410)	→	411
  012(620)	→	621
  012(622)	→	623
  500(1)	→	1
  231(713)	→	714
  231(777)	→	778
  231(129)	→	130
  231(504)	→	505
  231(389)	→	390
  231(400)	→	401
  231(355)	→	356
  231(222)	→	223
  231(843)	→	844
  231(302)	→	303
  231(97)	→	98
  231(339)	→	340
  231(360)	→	361
  231(141)	→	142
  231(727)	→	728
  231(224)	→	225
  231(937)	→	938
  201(899)	→	900
  201(99)	→	100
  201(913)	→	914
  201(36)	→	37
  201(34)	→	35
  201(216)	→	217
  201(685)	→	686
  221(213)	→	214
  221(505)	→	506
  221(496)	→	497
  221(95)	→	96
  221(123)	→	124
  221(361)	→	362
  221(707)	→	708
  221(573)	→	574
  221(947)	→	948
  221(935)	→	936
  221(945)	→	946
  221(212)	→	213
  221(71)	→	72
  221(214)	→	215
  221(499)	→	500
  102(619)	→	620
  102(621)	→	622
  010(1)	→	1
  100(1)	→	1
  340(1)	→	1
  011(581)	→	582
  011(47)	→	48
  011(871)	→	872
  011(404)	→	405
  011(812)	→	813
  011(587)	→	588
  011(6)	→	7
  011(617)	→	618
  011(985)	→	986
  011(873)	→	874
  011(810)	→	811
  011(406)	→	407
  011(4)	→	5
  011(516)	→	517
  501(169)	→	170
  501(394)	→	395
  501(456)	→	457
  501(567)	→	568
  501(782)	→	783
  501(509)	→	510
  501(582)	→	583
  501(911)	→	912
  120(1)	→	1
  331(226)	→	227
  331(345)	→	346
  331(749)	→	750
  331(503)	→	504
  331(584)	→	585
  331(298)	→	299
  331(221)	→	222
  331(441)	→	442
  331(463)	→	464