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: |
|---|
| abs-theorem | axiom | | abs-init,
step-absstep-ready-W1-invFLITPSCWRITE-same,
step-absstep-ready-W1-invFLITPSCWRITE-other,
step-absstep-W1-W2-tau-same,
step-absstep-W2-W3-tau-same,
step-absstep-W2-W3-tau-other,
step-absstep-W3-W4-doWritePSC-same,
step-absstep-W3-W4-doWritePSC-other,
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
step-absstep-W5-W6-tau-same,
step-absstep-W6-W7-tau-same,
step-absstep-W6-W7-tau-other,
step-absstep-W7-ready-retFLITPSCWRITE-same,
step-absstep-W7-ready-retFLITPSCWRITE-other,
step-absstep-ready-R1-invFLITPSCREAD-same,
step-absstep-ready-R1-invFLITPSCREAD-other,
step-absstep-R1-R2-doReadPSC-same,
step-absstep-R1-R2-doReadPSC-other,
step-absstep-R2-R3-tau-same,
step-absstep-R2-R3-tau-other,
step-absstep-R2-R4-tau-same,
step-absstep-R2-R4-tau-other,
step-absstep-R3-R4-tau-same,
step-absstep-R3-R4-tau-other,
step-absstep-R4-ready-retFLITPSCREAD-same,
step-absstep-R4-ready-retFLITPSCREAD-other,
step-absstep-idle-ready-callPSCRUN-same,
step-absstep-idle-ready-callPSCRUN-other,
step-absstep-ready-ready-callPSCCOMPLETE-same,
step-absstep-ready-ready-callPSCCOMPLETE-other,
step-absstep-PSCPERSIST_W-globalPSCPERSIST_W,
step-absstep-PSCPERSIST_FO-tau,
step-absstep-PSCCRASH-globalPSCCRASH,
|
| step-absstep-PSCCRASH-globalPSCCRASH | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PSCPERSIST_FO-tau | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PSCPERSIST_W-globalPSCPERSIST_W | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| abs-init | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-ready-ready-callPSCCOMPLETE-other | proved | all subs proved
| |
| step-absstep-ready-ready-callPSCCOMPLETE-same | proved | all subs proved
| |
| step-absstep-idle-ready-callPSCRUN-other | proved | all subs proved
| |
| step-absstep-idle-ready-callPSCRUN-same | proved | all subs proved
| |
| step-absstep-R4-ready-retFLITPSCREAD-other | proved | all subs proved
| |
| step-absstep-R4-ready-retFLITPSCREAD-same | proved | all subs proved
| |
| step-absstep-R3-R4-tau-other | proved | all subs proved
| |
| step-absstep-R3-R4-tau-same | proved | all subs proved
| |
| step-absstep-R2-R4-tau-other | proved | all subs proved
| |
| step-absstep-R2-R4-tau-same | proved | all subs proved
| |
| step-absstep-R2-R3-tau-other | proved | all subs proved
| |
| step-absstep-R2-R3-tau-same | proved | all subs proved
| |
| step-absstep-R1-R2-doReadPSC-other | proved | all subs proved
| |
| step-absstep-R1-R2-doReadPSC-same | proved | all subs proved
| |
| step-absstep-ready-R1-invFLITPSCREAD-other | proved | all subs proved
| |
| step-absstep-ready-R1-invFLITPSCREAD-same | proved | all subs proved
| |
| step-absstep-W7-ready-retFLITPSCWRITE-other | proved | all subs proved
| |
| step-absstep-W7-ready-retFLITPSCWRITE-same | proved | all subs proved
| |
| step-absstep-W6-W7-tau-other | proved | all subs proved
| |
| step-absstep-W6-W7-tau-same | proved | all subs proved
| |
| step-absstep-W5-W6-tau-same | proved | all subs proved
| |
| step-absstep-W4-W5-tau-other | proved | all subs proved
| |
| step-absstep-W4-W5-tau-same | proved | all subs proved
| |
| step-absstep-W3-W4-doWritePSC-other | proved | all subs proved
| |
| step-absstep-W3-W4-doWritePSC-same | proved | all subs proved
| |
| step-absstep-W2-W3-tau-other | proved | all subs proved
| |
| step-absstep-W2-W3-tau-same | proved | all subs proved
| |
| step-absstep-W1-W2-tau-same | proved | all subs proved
| |
| step-absstep-ready-W1-invFLITPSCWRITE-other | proved | all subs proved
| |
| step-absstep-ready-W1-invFLITPSCWRITE-same | proved | all subs proved
| |
| abs-def | axiom | | |
| gabs-def | axiom | | |
| labs-def | axiom | | |