[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 FLITPSCweak-proofs
Status:
Proved!
Axioms: 5, User Theorems: 43 (Proved: 43, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 207, Interactions: 43
FLITPSCInv-thm(0,0)
rely-PSCPERSIST_FO(10,0)
rely-W3-W4(2,0)
stable-W1(2,0)
step-FLITPSCLInv(0,0)
step-R3-R4(2,0)
step-W6-W7(7,0)
definedness-PSCPERSIST_W(2,0)
rely-PSCPERSIST_W(2,0)
rely-W4-W5(2,0)
stable-W2(2,0)
step-PSCCRASH(23,9)
step-R4-ready(2,0)
step-W7-ready(2,0)
definedness-R2(2,0)
rely-R1-R2(2,0)
rely-W6-W7(2,0)
stable-W3(2,0)
step-PSCPERSIST_FO(9,0)
step-W1-W2(26,8)
step-idle-ready(2,0)
definedness-W6(2,0)
rely-R2-R3(2,0)
rely-reflexive(2,0)
stable-W4(2,0)
step-PSCPERSIST_W(2,0)
step-W2-W3(2,0)
step-ready-R1(3,2)
init-state-inv(19,9)
rely-R2-R4(2,0)
stable-FLITPSCLInv(0,0)
stable-W5(2,0)
step-R1-R2(2,0)
step-W3-W4(2,0)
step-ready-W1(3,2)
other-FLITPSCLInv(0,0)
rely-R3-R4(2,0)
stable-R1(2,0)
stable-W7(2,0)
step-R2-R3(2,0)
step-W4-W5(2,0)
step-ready-ready(2,0)
rely-FLITPSCLInv(0,0)
rely-W2-W3(2,0)
stable-R2(2,0)
stable-idle(2,0)
step-R2-R4(2,0)
step-W5-W6(39,13)