[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 persistence-io-inv
Status:
Proved!
Axioms: 8, User Theorems: 29 (Proved: 29, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 161, Interactions: 55
disk-layout(0,0)
disk-layout-log-above-main(3,1)
disk-layout-orphans-below-main(2,0)
lebs-range-eq(19,8)
lebs-write-last(3,1)
mapped-full-write-above(1,0)
sb-orph(0,0)
disk-layout-1-unfold(1,0)
disk-layout-log-neq-orphans(2,0)
disk-layout-same-size(2,0)
lebs-rec(0,0)
mapped-full(0,0)
mapped-full-write-below(1,0)
disk-layout-2-unfold(1,0)
disk-layout-log-not-0(2,0)
disk-layout-size-vol-orphans(4,2)
lebs-size(11,3)
mapped-full-aligndown-vol(7,3)
mapped-full-zero(1,0)
disk-layout-avol-le-5(3,0)
disk-layout-lpt-below-main(3,1)
lebs-base(0,0)
lebs-size-mappedfull(14,7)
mapped-full-idexpt-below(13,6)
persistence-io-inv(0,0)
disk-layout-avol-neq-0(2,0)
disk-layout-main-not-below-lpt(2,0)
lebs-crash(17,8)
lebs-write-above(7,2)
mapped-full-last(11,4)
sb-log(0,0)
disk-layout-avol-neq-1(3,0)
disk-layout-not1-unfold(2,0)
lebs-idexpt-below(9,4)
lebs-write-below(6,2)
mapped-full-range-eq(9,3)
sb-lpt(0,0)