[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 list-prefixn
Status:
Proved!
Axioms: 3, User Theorems: 49 (Proved: 49, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 229, Interactions: 43
dropn(0,0)
in-prefixn-pos-smaller0(7,2)
isprefix-eq-size-app-eq(9,3)
prefixn(0,0)
prefixn-eq-append(4,1)
prefixn-le-eq(3,0)
prefixn-prefixn(19,1)
prefixn-split-sublist(10,4)
dropn-0(1,0)
in-prefixn-samepos(3,0)
isprefix-eq-size-app-eq1(3,1)
prefixn-0(1,0)
prefixn-eq-empty(4,2)
prefixn-le-size(1,0)
prefixn-prepend-one(2,0)
slice(0,0)
dropn-empty(1,0)
isprefix-add-prefixn-size(14,5)
isprefix-prefixn(3,0)
prefixn-append-left(1,0)
prefixn-eq-prefixn-app(22,5)
prefixn-len-le-n(2,0)
prefixn-shift-right(5,1)
slice-range0(1,0)
dropn-first(9,0)
isprefix-app-prefixn-isprefix(4,0)
prefix-append-one-sizeeq(4,2)
prefixn-append-prefix(2,1)
prefixn-full(1,0)
prefixn-len-n(1,0)
prefixn-single-1(1,0)
in-prefixn-at-smaller(3,0)
isprefix-app-size-ls(3,1)
prefix-prefixn-exact(3,1)
prefixn-append-slice(9,0)
prefixn-full-eq(2,1)
prefixn-neq-empty-plusone(2,0)
prefixn-size-eq(3,0)
in-prefixn-in-shorter-prefix(9,1)
isprefix-app-size-ls1(5,2)
prefix-prefixn-not-shorter(3,1)
prefixn-butlast(7,2)
prefixn-fulln(1,0)
prefixn-nodups(3,0)
prefixn-size-prefixn(6,0)
in-prefixn-pos-smaller(7,2)
isprefix-append-size(5,2)
prefix-prefixn-same(2,0)
prefixn-empty(1,0)
prefixn-in(3,0)
prefixn-notin(3,0)
prefixn-split-dropn(11,2)