[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 eraseblock
Status:
Proved!
Axioms: 12, User Theorems: 30 (Proved: 30, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 84, Interactions: 47
emptyleb-at(0,0)
isempty(0,0)
lebsize-eq-2page-size-pebsize(1,0)
page-size(0,0)
peb-vs-leb-size-ext(1,0)
pebsize-le-page-size(2,1)
pebsize-simp-ls(2,1)
emptyleb-size(0,0)
leb-size(0,0)
lebsize-ls-2page-size-pebsize(1,0)
peb-size(0,0)
pebsize(0,0)
pebsize-ls-2page-size-n(4,3)
pebsize-simp-ls-rev(2,1)
emptypage-at(0,0)
leb-size-rewrite(1,1)
lebsize-neq-zero(3,2)
peb-size-ge2(1,0)
pebsize-le-2page-size(2,1)
pebsize-ls-lebsize(4,2)
pebsize-simp-neq(2,1)
emptypage-size(0,0)
lebsize(0,0)
lebsize-page-size-is-aligned(3,2)
peb-size-not0(1,0)
pebsize-le-2page-size-lebsize(1,0)
pebsize-minus-2eb-page-size(5,3)
subarray-emptypeb-eq-emptyleb(9,5)
emptypeb-at(0,0)
lebsize-2page-size-le(5,3)
lebsize-pebsize(2,2)
peb-size-rewrite(2,1)
pebsize-le-2page-size-n(4,3)
pebsize-minus-eb-page-size(5,3)
subarray-emptypeb-eq-emptypage(3,2)
emptypeb-size(0,0)
lebsize-add-eq-0(2,1)
lebsize-simp-ls(2,1)
peb-vs-leb-size(1,0)
pebsize-le-minus-eb-page-size(5,3)
pebsize-page-size-is-aligned(3,2)
subarray-emptypeb-eq-emptypage1(5,3)