This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| eqds-def | ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0)) | An Axiom |
| run-base | ⊦ run(sys, []) = sys | An Axiom |
| run-rec | ⊦ run(sys, co ' + cl) = run(step(sys, co), cl) | An Axiom |
| run-initial | ⊦ run(cl) = run(initialstate, cl) | An Axiom |
| sources-base | ⊦ sources([], d) = ∅ ++ d | An Axiom |
| sources-rec | ⊦ sources(co ' + cl, d) = (((∃ d0. d0 ∈ sources(cl, d) ∧ cdom(co) ⇒ d0) ⊃ sources(cl, d) ++ cdom(co); sources(cl, d))) | An Axiom |
| ipurge-base | ⊦ ipurge([], d) = [] | An Axiom |
| ipurge-rec | ⊦ ipurge(co ' + cl, d) = ((cdom(co) ∈ sources(co + cl, d) ⊃ co + ipurge(cl, d); ipurge(cl, d))) | An Axiom |
| Security | ⊦ ipurge(cl, d) = ipurge(cl0, d) → obs(run(cl), d) = obs(run(cl0), d) | A Proof Obligation |
| Security-simple | ⊦ obs(run(cl), d) = obs(run(ipurge(cl, d)), d) | A Proof Obligation |
| Security-simple-without-initialstate | ⊦ obs(run(sys, cl), d) = obs(run(sys, ipurge(cl, d)), d) | A Proof Obligation |
| Security-strong | ⊦ ipurge(cl, d) = ipurge(cl0, d) ∧ eqds(sys, sources(cl, d), sys0) → obs(run(sys, cl), d) = obs(run(sys0, cl0), d) | A Proof Obligation |
| eqd-reflexivity | ⊦ eqd(sys, d, sys) | A User Theorem |
| eqd-symmetry | ⊦ eqd(sys, d, sys0) → eqd(sys0, d, sys) | A User Theorem |
| eqd-transitivity | ⊦ eqd(sys, d, sys0) ∧ eqd(sys0, d, sys1) → eqd(sys, d, sys1) | A User Theorem |
| eqds-refl | ⊦ eqds(sys, ds, sys) | A User Theorem |
| eqds-sources-ipurge | ⊦ eqds(sys, sources(cl, d), sys0) ↔ eqds(sys, sources(ipurge(cl, d), d), sys0) | A User Theorem |
| eqds-sources-ipurge-01 | ⊦ eqds(sys, sources(ipurge(cl, d), d), sys0) ↔ eqds(sys, sources(cl, d), sys0) | A User Theorem |
| eqds-symm | ⊦ eqds(sys, ds, sys0) → eqds(sys0, ds, sys) | A User Theorem |
| eqds-trans | ⊦ eqds(sys, ds, sys0) ∧ eqds(sys0, ds, sys1) → eqds(sys, ds, sys1) | A User Theorem |
| ipurge-idempotent | ⊦ ipurge(ipurge(cl, d), d) = ipurge(cl, d) | A User Theorem |
| lemma2 | ⊦ eqd(run(cl), d, run(ipurge(cl, d))) | A User Theorem |
| lemma3 | ⊦ eqds(sys, sources(co + cl, d), sys0) → eqds(step(sys, co), sources(cl, d), step(sys0, co)) | A User Theorem |
| lemma4 | ¬ cdom(co) ∈ sources(co ' + cl, d) ⊦ eqds(sys, sources(cl, d), step(sys, co)) | A User Theorem |
| lemma5 | eqds(sys, sources(cl, d), sys0) ⊦ eqd(run(sys, cl), d, run(sys0, ipurge(cl, d))) | A User Theorem |
| locally-respects | ⊦ ¬ cdom(co) ⇒ d0 → eqd(sys, d0, step(sys, co)) | A User Theorem |
| run-eqd | ⊦ eqds(sys, sources(cl, d), sys0) → eqd(run(sys, cl), d, run(sys0, cl)) | A User Theorem |
| sources-1 | ⊦ d ∈ sources(cl, d) | A User Theorem |
| sources-app | ⊦ sources(cl0, d) = sources(cl1, d) → sources(cl + cl0, d) = sources(cl + cl1, d) | A User Theorem |
| sources-in-one | ⊦ d0 ∈ sources(co ', d) ↔ d0 = d ∨ d0 = cdom(co) ∧ d0 ⇒ d | A User Theorem |
| sources-in-two | ⊦ d0 ∈ sources(co ' + co0 ', d) ↔ d0 = d ∨ d0 = cdom(co0) ∧ d0 ⇒ d ∨ d0 = cdom(co) ∧ d0 ⇒ d ∨ d0 = cdom(co) ∧ d0 ⇒ cdom(co0) ∧ cdom(co0) ⇒ d | A User Theorem |
| sources-interfere | ⊦ cdom(co) ⇒ d ∧ co ∈ cl → cdom(co) ∈ sources(cl, d) | A User Theorem |
| sources-ipurge | ⊦ d0 ∈ sources(ipurge(cl, d), d) ↔ d0 ∈ sources(cl, d) | A User Theorem |
| sources-not-empty | ⊦ sources(cl, d) ≠ ∅ | A User Theorem |
| sources-not-empty-01 | ⊦ # sources(cl, d) ≠ 0 | A User Theorem |
| sources-not-in | d0 ⇒ d, d0 ≠ d, cl = [] ⊦ ¬ (d0 ⇒ d → d0 ∈ sources(cl, d)) | A User Theorem |
| sources-not-transitive | d1 = cdom(co0), d0 = cdom(co), cdom(co0) ⇒ cdom(co), cdom(co) ⇒ d, ¬ cdom(co0) ⇒ d, cdom(co0) ≠ cdom(co), cdom(co0) ≠ d ⊦ ¬ (d1 ∈ sources(co ' + co0 ', d0) ∧ d0 ∈ sources(co ' + co0 ', d) → d1 ∈ sources(co ' + co0 ', d)) | A User Theorem |
| sources-one | ⊦ sources(co ', d) = (((∃ d0. d0 ∈ sources([], d) ∧ cdom(co) ⇒ d0) ⊃ sources([], d) ++ cdom(co); sources([], d))) | A User Theorem |
| sources-one-transitive | ⊦ d1 ∈ sources(co ', d0) ∧ d0 ∈ sources(co ', d) → d1 ∈ sources(co ', d) | A User Theorem |
| sources-rec-01 | ⊦ cl ≠ [] → sources(cl, d) = (((∃ d0. d0 ∈ sources(cl .rest, d) ∧ cdom(cl .first) ⇒ d0) ⊃ sources(cl .rest, d) ++ cdom(cl .first); sources(cl .rest, d))) | A User Theorem |
| sources-two-transitive | ⊦ d1 ∈ sources(co ' + co ', d0) ∧ d0 ∈ sources(co ' + co ', d) → d1 ∈ sources(co ' + co ', d) | A User Theorem |
| weakly-step-consistent | ⊦ eqd(sys, d, sys0) ∧ eqd(sys, cdom(co), sys0) → eqd(step(sys, co), d, step(sys0, co)) | A User Theorem |