[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 PLIB-proofs
Status:
Proved!
Axioms: 5, User Theorems: 18 (Proved: 18, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 81, Interactions: 20
PLIBInv-thm(0,0)
rely-PLIBLInv(0,0)
stable-PLIBLInv(0,0)
step-idle-ready(2,0)
step-ready-ready(2,0)
definedness-APersist(2,0)
rely-TSync(2,0)
stable-resWrite(2,0)
step-invRead-resRead(6,2)
step-resRead-ready(2,0)
init-state-inv(13,5)
rely-invRead-resRead(2,0)
step-ACrash(8,1)
step-invWrite-resWrite(2,0)
step-resWrite-ready(2,0)
other-PLIBLInv(0,0)
rely-invWrite-resWrite(2,0)
step-APersist(16,9)
step-ready-invRead(2,0)
rely-APersist(12,3)
rely-reflexive(2,0)
step-PLIBLInv(0,0)
step-ready-invWrite(2,0)