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: |
|---|---|---|
| run-base | ⊦ run(sys, []) = sys | An Axiom |
| run-rec | ⊦ run(sys, co + cl) = run(exec(sys, co) .1, cl) | An Axiom |
| execl | ⊦ execl(cl) = run(initialstate, cl) | An Axiom |
| test | ⊦ test(cl, co) = exec(execl(cl), co) .2 | An Axiom |
| sources-base | ⊦ sources(sys, [], d) = ∅ ++ d | An Axiom |
| sources-rec | ⊦ sources(sys, co + cl, d) = (((∃ d0. d0 ∈ sources(exec(sys, co) .1, cl, d) ∧ cdom(sys, co) ⇒ d0) ⊃ sources(exec(sys, co) .1, cl, d) ++ cdom(sys, co) ; sources(exec(sys, co) .1, cl, d) ) ) | An Axiom |
| purge-base | ⊦ purge(sys, [], d) = [] | An Axiom |
| purge-rec | ⊦ purge(sys, co + cl, d) = ((cdom(sys, co) ∈ sources(sys, co + cl, d) ⊃ co + purge(exec(sys, co) .1, cl, d); purge(sys, cl, d))) | An Axiom |
| step | ⊦ step(sys, co) = exec(sys, co) .1 | An Axiom |
| eqds-def | ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0)) | An Axiom |
| eqds-refl | ⊦ eqds(sys, ds, sys) | 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 |
| inv-run | ⊦ inv(run(initialstate, cl)) | A User Theorem |
| inv-run-gen | ⊦ inv(sys) → inv(run(sys, cl)) | A User Theorem |
| lemma2 | ⊦ eqd(execl(cl), d, execl(purge(initialstate, cl, d))) | A User Theorem |
| lemma3 | ⊦ inv(sys) ∧ inv(sys0) ∧ eqds(sys, sources(sys, co + cl, d), sys0) → eqds(exec(sys, co) .1, sources(exec(sys, co) .1, cl, d), exec(sys0, co) .1) | A User Theorem |
| lemma4 | inv(sys) ∧ ¬ cdom(sys, co) ∈ sources(sys, co + cl, d) ⊦ eqds(sys, sources(exec(sys, co) .1, cl, d), exec(sys, co) .1) | A User Theorem |
| lemma5 | inv(sys) ∧ inv(sys0) ∧ eqds(sys, sources(sys, cl, d), sys0) ⊦ eqd(run(sys, cl), d, run(sys0, purge(sys0, cl, d))) | A User Theorem |
| purge-rec-lem | ⊦ purge(sys, co ' + cl, d) = ((cdom(sys, co) ∈ sources(sys, co + cl, d) ⊃ co + purge(exec(sys, co) .1, cl, d); purge(sys, cl, d))) | A User Theorem |
| run-rec-lem | ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl) | A User Theorem |
| secure | ⊦ execl(cl) = sys → test(cl, co) = test(purge(initialstate, cl, cdom(sys, co)), co) | A User Theorem |
| sources-1 | ⊦ d ∈ sources(sys, cl, d) | A User Theorem |
| sources-equal | inv(sys) ∧ inv(sys0) ∧ eqds(sys, sources(sys, cl, d), sys0) ⊦ sources(sys, cl, d) = sources(sys0, cl, d) | A User Theorem |
| sources-rec-lem | ⊦ sources(sys, co ' + cl, d) = (((∃ d0. d0 ∈ sources(exec(sys, co) .1, cl, d) ∧ cdom(sys, co) ⇒ d0) ⊃ sources(exec(sys, co) .1, cl, d) ++ cdom(sys, co) ; sources(exec(sys, co) .1, cl, d) ) ) | A User Theorem |