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: |
|---|
| secure | proved | all subs proved
| lemma2,
inv-run,
test,
execl,
|
| lemma2 | proved | all subs proved
| eqds-refl,
lemma5,
execl,
|
| lemma5 | proved | all subs proved
| sources-rec-lem,
sources-equal,
eqds-trans,
lemma3,
purge-rec-lem,
run-rec-lem,
eqds-def,
purge-base,
run-base,
sources-base,
|
| sources-equal | proved | all subs proved
| eqds-def,
sources-rec-lem,
lemma3,
sources-base,
|
| inv-run | proved | all subs proved
| inv-run-gen,
|
| lemma3 | proved | all subs proved
| sources-rec-lem,
eqds-def,
|
| inv-run-gen | proved | all subs proved
| run-rec-lem,
run-base,
|
| lemma4 | proved | all subs proved
| sources-rec-lem,
eqds-def,
|
| sources-1 | proved | all subs proved
| sources-rec-lem,
sources-base,
|
| eqds-refl | proved | all subs proved
| eqds-def,
|
| eqds-trans | proved | all subs proved
| eqds-def,
|
| purge-rec-lem | proved | all subs proved
| purge-rec,
|
| run-rec-lem | proved | all subs proved
| run-rec,
|
| sources-rec-lem | proved | all subs proved
| sources-rec,
|
| eqds-symm | proved | all subs proved
| eqds-def,
|
| sources-rec | axiom | | |
| test | axiom | | |
| run-rec | axiom | | |
| purge-rec | axiom | | |
| sources-base | axiom | | |
| purge-base | axiom | | |
| execl | axiom | | |
| run-base | axiom | | |
| eqds-def | axiom | | |