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: |
|---|
| Security | proved | all subs proved
| RMA-1,
lemma2,
test,
|
| lemma2 | proved | all subs proved
| eqds-refl,
lemma5,
execl,
|
| lemma5 | proved | all subs proved
| sources-rec,
locally-respects,
eqds-symm,
eqds-trans,
ipurge-rec,
lemma3,
run-rec,
eqds-def,
ipurge-base,
run-base,
sources-base,
|
| lemma3 | proved | all subs proved
| eqd-symmetry,
eqd-transitivity,
locally-respects,
sources-rec,
weakly-step-consistent,
eqds-def,
|
| eqds-trans | proved | all subs proved
| eqd-transitivity,
eqds-def,
|
| eqds-symm | proved | all subs proved
| eqd-symmetry,
eqds-def,
|
| eqds-refl | proved | all subs proved
| eqd-reflexivity,
eqds-def,
|
| lemma4 | proved | all subs proved
| locally-respects,
eqds-def,
sources-rec,
|
| eqd-reflexivity | proved | all subs proved
| eqd-def,
|
| eqd-symmetry | proved | all subs proved
| eqd-def,
|
| eqd-transitivity | proved | all subs proved
| eqd-def,
|
| weakly-step-consistent | proved | all subs proved
| RMA-3,
RMA-2,
eqd-def,
|
| locally-respects | proved | all subs proved
| alter-observe-respects-policy,
RMA-3,
eqd-def,
|
| sources-1 | proved | all subs proved
| sources-rec,
sources-base,
|
| RMA-2 | axiom | | |
| RMA-3 | axiom | | |
| alter-observe-respects-policy | axiom | | |
| sources-base | axiom | | |
| run-base | axiom | | |
| ipurge-base | axiom | | |
| run-rec | axiom | | |
| ipurge-rec | axiom | | |
| sources-rec | axiom | | |
| execl | axiom | | |
| eqds-def | axiom | | |
| eqd-def | axiom | | |
| test | axiom | | |
| RMA-1 | axiom | | |