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-simple | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
lemma2,
|
| Security | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
lemma2,
|
| lemma2 | proved | all subs proved
| eqs-reflexivity,
eqds-refl,
lemma5-2,
run-initial,
|
| lemma5-2 | proved | all subs proved
| locally-respects2,
locally-respects,
eqs-ipurged,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
sources-1,
lemma3-2,
ipurge-rec,
run-rec,
sources-rec,
eqds-def,
ipurge-base,
run-base,
sources-base,
|
| lemma3-2 | proved | all subs proved
| locally-respects,
sources-1,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
weakly-step-consistent2,
sources-rec,
eqds-def,
|
| ipurge-idempotent | proved | all subs proved
| sources-ipurge,
sources-rec,
ipurge-rec,
ipurge-base,
|
| sources-ipurge | proved | all subs proved
| sources-rec,
ipurge-rec,
sources-base,
ipurge-base,
|
| eqds-refl | proved | all subs proved
| eqd-reflexivity,
eqds-def,
|
| weakly-step-consistent2 | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
|
| sources-1 | proved | all subs proved
| sources-rec,
sources-base,
|
| lemma4 | proved | all subs proved
| locally-respects,
eqds-def,
sources-rec,
|
| eqs-step | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
|
| eqds-trans | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
eqds-def,
|
| eqds-symm | proved | all subs proved
| eqd-symmetry,
eqds-def,
|
| sources-base | axiom | | |
| run-base | axiom | | |
| run-rec | axiom | | |
| eqs-ipurged | proved | all subs proved
| |
| locally-respects2 | proved | all subs proved
| |
| locally-respects | proved | all subs proved
| |
| run-initial | axiom | | |
| eqs-reflexivity | proved | all subs proved
| |
| ipurge-base | axiom | | |
| ipurge-rec | axiom | | |
| sources-rec | axiom | | |
| eqds-def | axiom | | |
| eqd-symmetry | proved | all subs proved
| |
| eqd-transitivity | proved | all subs proved
| |
| eqd-reflexivity | proved | all subs proved
| |