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: |
|---|
| fw-trans | proved | all subs proved
| fw-trans-aux,
forwardsim-def,
|
| weakbwsim-implies-bwsiminv | proved | all subs proved
| weakbwsim-implies-bwsiminv-aux,
backwardsiminv-def,
weakbackwardsim-def,
|
| weakbwsim-implies-bwsiminv-aux | proved | all subs proved
| weak-lemma_3-15,
proofobls-weakbackwardsim,
proofobls-backwardsiminv,
|
| fw-trans-aux | proved | all subs proved
| fw-frag,
proofobls-forwardsim,
|
| bwsim-bwsiminv | proved | all subs proved
| bwsim-bwsiminv-aux,
backwardsiminv-def,
backwardsim-def,
|
| bwsiminv-implies-weakbwsim | proved | all subs proved
| bwsiminv-implies-weakbwsim-aux,
weakbackwardsim-def,
backwardsiminv-def,
|
| weak-lemma_3-15 | proved | all subs proved
| proofobls-weakbackwardsim,
|
| fw-frag | proved | all subs proved
| proofobls-forwardsim,
|
| bwsiminv-implies-weakbwsim-aux | proved | all subs proved
| proofobls-backwardsiminv,
proofobls-weakbackwardsim,
|
| bwsim-bwsiminv-aux | proved | all subs proved
| proofobls-backwardsiminv,
proofobls-backwardsim,
|
| lemma_3-15 | proved | all subs proved
| proofobls-backwardsiminv,
|
| forwardsim-def | axiom | | |
| proofobls-forwardsim | axiom | | |
| proofobls-weakbackwardsim | axiom | | |
| weakbackwardsim-def | axiom | | |
| proofobls-backwardsim | axiom | | |
| proofobls-backwardsiminv | axiom | | |
| backwardsim-def | axiom | | |
| backwardsiminv-def | axiom | | |