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: |
|---|
| stable-FLITPSCLInv | axiom | | init-state-inv,
step-ready-W1,
step-ready-R1,
step-ready-ready,
step-W1-W2,
step-W2-W3,
step-W3-W4,
step-W4-W5,
step-W5-W6,
step-W6-W7,
step-W7-ready,
step-R1-R2,
step-R2-R3,
step-R2-R4,
step-R3-R4,
step-R4-ready,
step-idle-ready,
step-PSCPERSIST_W,
step-PSCPERSIST_FO,
step-PSCCRASH,
rely-reflexive,
rely-W2-W3,
rely-W3-W4,
rely-W4-W5,
rely-W6-W7,
rely-R1-R2,
rely-R2-R3,
rely-R2-R4,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
stable-R1,
stable-R2,
stable-W1,
stable-W2,
stable-W3,
stable-W4,
stable-W5,
stable-W7,
stable-idle,
definedness-W6,
definedness-R2,
definedness-PSCPERSIST_W,
|
| step-FLITPSCLInv | axiom | | init-state-inv,
step-ready-W1,
step-ready-R1,
step-ready-ready,
step-W1-W2,
step-W2-W3,
step-W3-W4,
step-W4-W5,
step-W5-W6,
step-W6-W7,
step-W7-ready,
step-R1-R2,
step-R2-R3,
step-R2-R4,
step-R3-R4,
step-R4-ready,
step-idle-ready,
step-PSCPERSIST_W,
step-PSCPERSIST_FO,
step-PSCCRASH,
rely-reflexive,
rely-W2-W3,
rely-W3-W4,
rely-W4-W5,
rely-W6-W7,
rely-R1-R2,
rely-R2-R3,
rely-R2-R4,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
stable-R1,
stable-R2,
stable-W1,
stable-W2,
stable-W3,
stable-W4,
stable-W5,
stable-W7,
stable-idle,
definedness-W6,
definedness-R2,
definedness-PSCPERSIST_W,
|
| other-FLITPSCLInv | axiom | | init-state-inv,
step-ready-W1,
step-ready-R1,
step-ready-ready,
step-W1-W2,
step-W2-W3,
step-W3-W4,
step-W4-W5,
step-W5-W6,
step-W6-W7,
step-W7-ready,
step-R1-R2,
step-R2-R3,
step-R2-R4,
step-R3-R4,
step-R4-ready,
step-idle-ready,
step-PSCPERSIST_W,
step-PSCPERSIST_FO,
step-PSCCRASH,
rely-reflexive,
rely-W2-W3,
rely-W3-W4,
rely-W4-W5,
rely-W6-W7,
rely-R1-R2,
rely-R2-R3,
rely-R2-R4,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
stable-R1,
stable-R2,
stable-W1,
stable-W2,
stable-W3,
stable-W4,
stable-W5,
stable-W7,
stable-idle,
definedness-W6,
definedness-R2,
definedness-PSCPERSIST_W,
|
| FLITPSCInv-thm | axiom | | init-state-inv,
step-ready-W1,
step-ready-R1,
step-ready-ready,
step-W1-W2,
step-W2-W3,
step-W3-W4,
step-W4-W5,
step-W5-W6,
step-W6-W7,
step-W7-ready,
step-R1-R2,
step-R2-R3,
step-R2-R4,
step-R3-R4,
step-R4-ready,
step-idle-ready,
step-PSCPERSIST_W,
step-PSCPERSIST_FO,
step-PSCCRASH,
rely-reflexive,
rely-W2-W3,
rely-W3-W4,
rely-W4-W5,
rely-W6-W7,
rely-R1-R2,
rely-R2-R3,
rely-R2-R4,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
stable-R1,
stable-R2,
stable-W1,
stable-W2,
stable-W3,
stable-W4,
stable-W5,
stable-W7,
stable-idle,
definedness-W6,
definedness-R2,
definedness-PSCPERSIST_W,
|
| rely-FLITPSCLInv | axiom | | init-state-inv,
step-ready-W1,
step-ready-R1,
step-ready-ready,
step-W1-W2,
step-W2-W3,
step-W3-W4,
step-W4-W5,
step-W5-W6,
step-W6-W7,
step-W7-ready,
step-R1-R2,
step-R2-R3,
step-R2-R4,
step-R3-R4,
step-R4-ready,
step-idle-ready,
step-PSCPERSIST_W,
step-PSCPERSIST_FO,
step-PSCCRASH,
rely-reflexive,
rely-W2-W3,
rely-W3-W4,
rely-W4-W5,
rely-W6-W7,
rely-R1-R2,
rely-R2-R3,
rely-R2-R4,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
stable-R1,
stable-R2,
stable-W1,
stable-W2,
stable-W3,
stable-W4,
stable-W5,
stable-W7,
stable-idle,
definedness-W6,
definedness-R2,
definedness-PSCPERSIST_W,
|
| definedness-PSCPERSIST_W | proved | all subs proved
| |
| definedness-R2 | proved | all subs proved
| |
| definedness-W6 | proved | all subs proved
| |
| stable-idle | proved | all subs proved
| |
| stable-W7 | proved | all subs proved
| |
| stable-W5 | proved | all subs proved
| |
| stable-W4 | proved | all subs proved
| |
| stable-W3 | proved | all subs proved
| |
| stable-W2 | proved | all subs proved
| |
| stable-W1 | proved | all subs proved
| |
| stable-R2 | proved | all subs proved
| |
| stable-R1 | proved | all subs proved
| |
| rely-PSCPERSIST_FO | proved | all subs proved
| |
| rely-PSCPERSIST_W | proved | all subs proved
| |
| rely-R3-R4 | proved | all subs proved
| |
| rely-R2-R4 | proved | all subs proved
| |
| rely-R2-R3 | proved | all subs proved
| |
| rely-R1-R2 | proved | all subs proved
| |
| rely-W6-W7 | proved | all subs proved
| |
| rely-W4-W5 | proved | all subs proved
| |
| rely-W3-W4 | proved | all subs proved
| |
| rely-W2-W3 | proved | all subs proved
| |
| rely-reflexive | proved | all subs proved
| |
| step-PSCCRASH | proved | all subs proved
| |
| step-PSCPERSIST_FO | proved | all subs proved
| |
| step-PSCPERSIST_W | proved | all subs proved
| |
| step-idle-ready | proved | all subs proved
| |
| step-R4-ready | proved | all subs proved
| |
| step-R3-R4 | proved | all subs proved
| |
| step-R2-R4 | proved | all subs proved
| |
| step-R2-R3 | proved | all subs proved
| |
| step-R1-R2 | proved | all subs proved
| |
| step-W7-ready | proved | all subs proved
| |
| step-W6-W7 | proved | all subs proved
| |
| step-W5-W6 | proved | all subs proved
| |
| step-W4-W5 | proved | all subs proved
| |
| step-W3-W4 | proved | all subs proved
| |
| step-W2-W3 | proved | all subs proved
| |
| step-W1-W2 | proved | all subs proved
| |
| step-ready-ready | proved | all subs proved
| |
| step-ready-R1 | proved | all subs proved
| |
| step-ready-W1 | proved | all subs proved
| |
| init-state-inv | proved | all subs proved
| |