[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: 71, Interactions: 38
Ordered(0,0)
empty(1,1)
ins-01(5,3)
ordered-perm-sort(6,5)
size-01(1,0)
sort-append-three(1,1)
Perm(0,0)
emptyp(2,0)
ins-02(3,2)
perm(3,2)
sort(1,0)
sperm(7,4)
appins(4,2)
eq(2,0)
insdel(1,0)
perm-01(6,5)
sort-01(1,1)
two(1,0)
combine-ordered-sublists(6,2)
in(3,2)
ole(1,0)
rec(1,1)
sort-02(3,0)
two-01(1,0)
del1(7,4)
ins(1,1)
one(1,1)
size(1,0)
sort-append(1,1)