[Imprint]
[Data Privacy Statement]
[E-Mail]
Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem base summary for Specification olist
Status:
Proved!
Axioms: 11, User Theorems: 60 (Proved: 60, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 475, Interactions: 130
app(9,2)
del1-01-01(3,1)
in-04(6,0)
ins-rec(3,0)
insperm-03(5,2)
ls-o(0,0)
ole-last-01(3,1)
ordered-postfix(17,8)
rest(3,0)
app-01(5,0)
del1-01-02(17,4)
ins-e(0,0)
ins-y(0,0)
k-le-r(5,0)
ls-r(0,0)
ole-rec(5,0)
ordered-prefix(17,4)
rest-01(3,0)
app-02(5,2)
del1-02(8,2)
ins-less-first(5,0)
ins-y-01(2,1)
k-ls-r(4,0)
merge-empty(0,0)
ole-two(2,1)
ordered-shorter-sublist(6,3)
same(2,0)
cons(3,0)
empty(5,0)
ins-less-last(7,1)
ins-yes(3,0)
le-e(0,0)
merge-rec(0,0)
ols-rec(5,0)
orderedle-all(29,10)
sort-possible(5,3)
cons-02(3,0)
eq(21,4)
ins-n(0,0)
ins2(3,1)
le-o(0,0)
ole(2,0)
one-02(2,1)
orderedle-ls(2,0)
sw(18,3)
cons-03(3,0)
eqdef(7,2)
ins-one(3,1)
insperm(2,1)
le-r(0,0)
ole-01(16,4)
ordered-append(13,3)
orderedls-all(31,11)
szle1-orderedle(2,1)
del1(15,5)
ex(11,4)
ins-one-01(3,1)
insperm-01(9,5)
len(6,0)
ole-in(5,1)
ordered-ex-divide-lels(19,8)
orderedls-ls(5,1)
szle1-orderedls(2,1)
del1-01(17,6)
in-01-02(7,2)
ins-one-02(3,1)
insperm-02(8,2)
ls-e(0,0)
ole-last(23,5)
ordered-ex-divide-lsle(15,7)
perm-ins(7,4)