A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| other-PLIBLInv | axiom | | init-state-inv,
step-ready-ready,
step-ready-invWrite,
step-ready-invRead,
step-idle-ready,
step-invWrite-resWrite,
step-resWrite-ready,
step-invRead-resRead,
step-resRead-ready,
step-ACrash,
step-APersist,
rely-reflexive,
rely-invWrite-resWrite,
rely-invRead-resRead,
rely-APersist,
stable-resWrite,
definedness-APersist,
|
| stable-PLIBLInv | axiom | | init-state-inv,
step-ready-ready,
step-ready-invWrite,
step-ready-invRead,
step-idle-ready,
step-invWrite-resWrite,
step-resWrite-ready,
step-invRead-resRead,
step-resRead-ready,
step-ACrash,
step-APersist,
rely-reflexive,
rely-invWrite-resWrite,
rely-invRead-resRead,
rely-APersist,
stable-resWrite,
definedness-APersist,
|
| PLIBInv-thm | axiom | | init-state-inv,
step-ready-ready,
step-ready-invWrite,
step-ready-invRead,
step-idle-ready,
step-invWrite-resWrite,
step-resWrite-ready,
step-invRead-resRead,
step-resRead-ready,
step-ACrash,
step-APersist,
rely-reflexive,
rely-invWrite-resWrite,
rely-invRead-resRead,
rely-APersist,
stable-resWrite,
definedness-APersist,
|
| rely-PLIBLInv | axiom | | init-state-inv,
step-ready-ready,
step-ready-invWrite,
step-ready-invRead,
step-idle-ready,
step-invWrite-resWrite,
step-resWrite-ready,
step-invRead-resRead,
step-resRead-ready,
step-ACrash,
step-APersist,
rely-reflexive,
rely-invWrite-resWrite,
rely-invRead-resRead,
rely-APersist,
stable-resWrite,
definedness-APersist,
|
| step-PLIBLInv | axiom | | init-state-inv,
step-ready-ready,
step-ready-invWrite,
step-ready-invRead,
step-idle-ready,
step-invWrite-resWrite,
step-resWrite-ready,
step-invRead-resRead,
step-resRead-ready,
step-ACrash,
step-APersist,
rely-reflexive,
rely-invWrite-resWrite,
rely-invRead-resRead,
rely-APersist,
stable-resWrite,
definedness-APersist,
|
| definedness-APersist | proved | all subs proved
| |
| stable-resWrite | proved | all subs proved
| |
| rely-APersist | proved | all subs proved
| |
| rely-invRead-resRead | proved | all subs proved
| |
| rely-invWrite-resWrite | proved | all subs proved
| |
| rely-reflexive | proved | all subs proved
| |
| step-APersist | proved | all subs proved
| |
| step-ACrash | proved | all subs proved
| |
| step-resRead-ready | proved | all subs proved
| |
| step-invRead-resRead | proved | all subs proved
| |
| step-resWrite-ready | proved | all subs proved
| |
| step-invWrite-resWrite | proved | all subs proved
| |
| step-idle-ready | proved | all subs proved
| |
| step-ready-invRead | proved | all subs proved
| |
| step-ready-invWrite | proved | all subs proved
| |
| step-ready-ready | proved | all subs proved
| |
| init-state-inv | proved | all subs proved
| |