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
| eqds-refl,
Security-strong,
run-initial,
|
| Security-strong | proved | all subs proved
| eqds-sources-ipurge,
run-eqd,
Security-simple-without-initialstate,
|
| LanguageBasedNIF-run | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
run-eqd,
|
| LanguageBasedNIF-run-observe | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
run-eqd,
|
| Security-simple | proved | all subs proved
| Security-simple-without-initialstate,
run-initial,
|
| Security-simple-without-initialstate | proved | all subs proved
| eqds-refl,
lemma5,
|
| run-eqd | proved | all subs proved
| eqds-refl,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
lemma5,
|
| eqds-sources-ipurge | proved | all subs proved
| eqds-sources-ipurge-01,
|
| lemma2 | proved | all subs proved
| eqds-refl,
lemma5,
run-initial,
|
| eqds-sources-ipurge-01 | proved | all subs proved
| sources-ipurge,
eqds-def,
|
| lemma5 | proved | all subs proved
| locally-respects,
eqds-symm,
eqds-trans,
sources-rec,
ipurge-rec,
lemma3,
run-rec,
eqds-def,
ipurge-base,
run-base,
sources-base,
|
| ipurge-idempotent | proved | all subs proved
| sources-1,
sources-ipurge,
sources-rec,
ipurge-rec,
ipurge-base,
|
| lemma3 | proved | all subs proved
| locally-respects,
sources-rec,
weakly-step-consistent,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
eqds-def,
|
| sources-ipurge | proved | all subs proved
| sources-1,
ipurge-rec,
sources-rec,
sources-base,
ipurge-base,
|
| LanguageBasedNIF-follows | proved | all subs proved
| eqd-implies-LanguageBasedNIF,
|
| eqd-implies-LanguageBasedNIF | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
|
| weakly-step-consistent | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
|
| eqds-symm | proved | all subs proved
| eqd-symmetry,
eqds-def,
|
| eqds-trans | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
eqds-def,
|
| eqds-refl | proved | all subs proved
| eqd-reflexivity,
eqds-def,
|
| sources-1 | proved | all subs proved
| sources-rec,
sources-base,
|
| lemma4 | proved | all subs proved
| locally-respects,
eqds-def,
sources-rec,
|
| LanguageBasedNIF-weaker | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
|
| sources-base | axiom | | |
| run-base | axiom | | |
| run-rec | axiom | | |
| locally-respects | 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
| |
| run-initial | axiom | | |