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
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
lemma2,
|
| Security-simple | proved | all subs proved
| lemma2,
|
| Security-strong | proved | all subs proved
| eqds-sources-ipurge,
eqds-symm,
eqds-sources-ipurge-01,
run-eqd,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
eqds-refl,
lemma5,
|
| lemma2 | proved | all subs proved
| eqds-refl,
lemma5,
run-initial,
|
| run-eqd | proved | all subs proved
| eqds-refl,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
lemma5,
|
| Security-simple-without-initialstate | proved | all subs proved
| eqds-refl,
lemma5,
|
| eqds-sources-ipurge-01 | proved | all subs proved
| eqds-sources-ipurge,
|
| 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,
|
| sources-not-transitive | proved | all subs proved
| sources-in-two,
|
| eqds-sources-ipurge | proved | all subs proved
| sources-ipurge,
eqds-def,
|
| lemma3 | proved | all subs proved
| locally-respects,
sources-rec,
weakly-step-consistent,
eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
eqds-def,
|
| sources-in-two | proved | all subs proved
| sources-1,
sources-not-empty-01,
sources-base,
sources-one,
sources-not-empty,
sources-rec,
|
| ipurge-idempotent | proved | all subs proved
| sources-ipurge,
sources-rec,
ipurge-rec,
ipurge-base,
|
| sources-not-empty-01 | proved | all subs proved
| sources-not-empty,
|
| eqds-trans | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
eqds-def,
|
| weakly-step-consistent | proved | all subs proved
| eqd-reflexivity,
eqd-transitivity,
eqd-symmetry,
|
| sources-ipurge | proved | all subs proved
| sources-1,
sources-rec,
ipurge-rec,
sources-base,
ipurge-base,
|
| sources-app | proved | all subs proved
| sources-not-empty,
sources-rec,
|
| sources-in-one | proved | all subs proved
| sources-base,
sources-one,
|
| sources-interfere | proved | all subs proved
| sources-1,
sources-rec,
|
| sources-one-transitive | proved | all subs proved
| sources-base,
sources-one,
|
| sources-rec-01 | proved | all subs proved
| sources-rec,
sources-not-empty,
|
| sources-two-transitive | proved | all subs proved
| sources-1,
sources-base,
sources-one,
sources-rec,
|
| eqds-symm | proved | all subs proved
| eqd-symmetry,
eqds-def,
|
| eqds-refl | proved | all subs proved
| eqd-reflexivity,
eqds-def,
|
| sources-not-empty | proved | all subs proved
| sources-rec,
sources-base,
|
| sources-1 | proved | all subs proved
| sources-rec,
sources-base,
|
| sources-one | proved | all subs proved
| sources-rec,
sources-base,
|
| eqd-transitivity | proved | all subs proved
| eqd-symmetry,
|
| sources-not-in | proved | all subs proved
| sources-base,
|
| lemma4 | proved | all subs proved
| locally-respects,
eqds-def,
sources-rec,
|
| sources-base | axiom | | |
| run-base | axiom | | |
| run-rec | axiom | | |
| locally-respects | proved | all subs proved
| |
| run-initial | axiom | | |
| ipurge-base | axiom | | |
| ipurge-rec | axiom | | |
| sources-rec | axiom | | |
| eqds-def | axiom | | |
| eqd-symmetry | proved | all subs proved
| |
| eqd-reflexivity | proved | all subs proved
| |