[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: 5, User Theorems: 15 (Proved: 15, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 125, Interactions: 42
ll-trav1-def(0,0)
ll-trav2-end(15,2)
ll-trav2-null-def(0,0)
lls-fold-tail(9,2)
lls-to-ls(11,4)
ll-trav1-end(9,2)
ll-trav2-init(2,0)
lls-base(0,0)
lls-null(4,2)
lls-unfold-head(8,2)
ll-trav1-init(3,1)
ll-trav2-next(15,5)
lls-consecutive(7,2)
lls-one(6,4)
lls-unfold-head-simp(3,1)
ll-trav1-next(9,3)
ll-trav2-nonnull-def(0,0)
lls-fold-head(10,4)
lls-rec(0,0)
lls-unfold-tail(14,8)