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-invFLITWRITE-same,
step-absstep-ready-W1-invFLITWRITE-other,
step-absstep-W1-W2-tau-same,
step-absstep-W1-W2-tau-other,
step-absstep-W2-W3-ctrInc-same,
step-absstep-W2-W3-ctrInc-other,
step-absstep-W3-W4-tau-same,
step-absstep-W3-W4-tau-other,
step-absstep-W4-W5-tau-same,
step-absstep-W4-W5-tau-other,
step-absstep-W5-W6-tau-same,
step-absstep-W5-W6-tau-other,
step-absstep-W6-W7-ctrDec-same,
step-absstep-W6-W7-ctrDec-other,
step-absstep-W7-ready-retFLITWRITE-same,
step-absstep-W7-ready-retFLITWRITE-other,
step-absstep-ready-R1-invFLITREAD-same,
step-absstep-ready-R1-invFLITREAD-other,
step-absstep-R1-R2-doRead-same,
step-absstep-R1-R2-doRead-other,
step-absstep-R2-R3-ctrRead-same,
step-absstep-R2-R3-ctrRead-other,
step-absstep-R2-R4-ctrRead-same,
step-absstep-R2-R4-ctrRead-other,
step-absstep-R3-R4-pwb-same,
step-absstep-R3-R4-pwb-other,
step-absstep-R4-ready-retFLITREAD-same,
step-absstep-R4-ready-retFLITREAD-other,
step-absstep-idle-ready-callRUN-same,
step-absstep-idle-ready-callRUN-other,
step-absstep-ready-ready-callFLITCOMPLETE-same,
step-absstep-ready-ready-callFLITCOMPLETE-other,
step-absstep-PROP_W-doWrite,
step-absstep-PROP_FO-doWriteFO,
step-absstep-PROP_FO-tau,
step-absstep-PROP_SF-propSF,
step-absstep-PERSIST_W-globalPERSIST_W,
step-absstep-PERSIST_FO-globalPERSIST_FO,
step-absstep-CRASH-globalCRASH,
|
| step-absstep-CRASH-globalCRASH | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PERSIST_FO-globalPERSIST_FO | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PERSIST_W-globalPERSIST_W | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PROP_SF-propSF | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PROP_FO-tau | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PROP_FO-doWriteFO | proved | all subs proved
| labs-def,
gabs-def,
abs-def,
|
| step-absstep-PROP_W-doWrite | 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-callFLITCOMPLETE-other | proved | all subs proved
| |
| step-absstep-ready-ready-callFLITCOMPLETE-same | proved | all subs proved
| |
| step-absstep-idle-ready-callRUN-other | proved | all subs proved
| |
| step-absstep-idle-ready-callRUN-same | proved | all subs proved
| |
| step-absstep-R4-ready-retFLITREAD-other | proved | all subs proved
| |
| step-absstep-R4-ready-retFLITREAD-same | proved | all subs proved
| |
| step-absstep-R3-R4-pwb-other | proved | all subs proved
| |
| step-absstep-R3-R4-pwb-same | proved | all subs proved
| |
| step-absstep-R2-R4-ctrRead-other | proved | all subs proved
| |
| step-absstep-R2-R4-ctrRead-same | proved | all subs proved
| |
| step-absstep-R2-R3-ctrRead-other | proved | all subs proved
| |
| step-absstep-R2-R3-ctrRead-same | proved | all subs proved
| |
| step-absstep-R1-R2-doRead-other | proved | all subs proved
| |
| step-absstep-R1-R2-doRead-same | proved | all subs proved
| |
| step-absstep-ready-R1-invFLITREAD-other | proved | all subs proved
| |
| step-absstep-ready-R1-invFLITREAD-same | proved | all subs proved
| |
| step-absstep-W7-ready-retFLITWRITE-other | proved | all subs proved
| |
| step-absstep-W7-ready-retFLITWRITE-same | proved | all subs proved
| |
| step-absstep-W6-W7-ctrDec-other | proved | all subs proved
| |
| step-absstep-W6-W7-ctrDec-same | proved | all subs proved
| |
| step-absstep-W5-W6-tau-other | 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-tau-other | proved | all subs proved
| |
| step-absstep-W3-W4-tau-same | proved | all subs proved
| |
| step-absstep-W2-W3-ctrInc-other | proved | all subs proved
| |
| step-absstep-W2-W3-ctrInc-same | proved | all subs proved
| |
| step-absstep-W1-W2-tau-other | proved | all subs proved
| |
| step-absstep-W1-W2-tau-same | proved | all subs proved
| |
| step-absstep-ready-W1-invFLITWRITE-other | proved | all subs proved
| |
| step-absstep-ready-W1-invFLITWRITE-same | proved | all subs proved
| |
| abs-def | axiom | | |
| gabs-def | axiom | | |
| labs-def | axiom | | |