[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 linked-list-seg
Status:
Proved!
Axioms: 6, User Theorems: 27 (Proved: 27, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 226, Interactions: 95
ll-lasso(0,0)
ll-trav2-init(2,0)
lls-fold-head(10,4)
lls-merge(2,1)
lls-rec(0,0)
ls-lls(12,7)
ll-trav1-def(0,0)
ll-trav2-next(15,5)
lls-fold-tail(9,2)
lls-merge-gen(8,3)
lls-split(14,7)
ls-lls-last(8,5)
ll-trav1-end(9,2)
ll-trav2-nonnull-def(0,0)
lls-fold-tail2(2,1)
lls-null(4,2)
lls-to-ls(13,4)
ls-split(8,5)
ll-trav1-init(3,1)
ll-trav2-null-def(0,0)
lls-injective(4,1)
lls-one(6,4)
lls-unfold-head(8,2)
ll-trav1-next(9,3)
lls-base(0,0)
lls-lasso-inj(7,3)
lls-prefix(2,1)
lls-unfold-head-simp(3,1)
ll-trav2-end(15,2)
lls-consecutive(7,2)
lls-lasso-inj-gen(22,14)
lls-prefix-gen(10,5)
lls-unfold-tail(14,8)