[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-sort
Status:
Proved!
Axioms: 2, User Theorems: 27 (Proved: 27, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 98, Interactions: 38
Ordered(0,0)
empty(2,1)
ins-01(6,3)
ordered-perm-sort(7,5)
size-01(2,0)
sort-append-three(2,1)
Perm(0,0)
emptyp(3,0)
ins-02(4,2)
perm(4,2)
sort(2,0)
sperm(8,4)
appins(5,2)
eq(3,0)
insdel(2,0)
perm-01(7,5)
sort-01(2,1)
two(2,0)
combine-ordered-sublists(7,2)
in(4,2)
ole(2,0)
rec(2,1)
sort-02(4,0)
two-01(2,0)
del1(8,4)
ins(2,1)
one(2,1)
size(2,0)
sort-append(2,1)