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 |
| test | ⊦ test(sys, cl, co) = exec(run(sys, cl), co) .2 | An Axiom |
| step | ⊦ step(sys, co) = exec(sys, co) .1 | An Axiom |
| output | ⊦ outputt(sys, co) = exec(sys, co) .2 | An Axiom |
| run-base | ⊦ run(sys, []) = sys | An Axiom |
| run-rec | ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl) | An Axiom |
| purge-base | ⊦ purge([], d) = [] | An Axiom |
| purge-rec | ⊦ purge(co ' + cl, d) = ((cdom(co) ⇒ d ⊃ co + purge(cl, d); purge(cl, d))) | An Axiom |
| wf-def | ⊦ wf(cl) ↔ (∀ co. co ∈ cl → wf(co)) | An Axiom |
| Security | ⊦ wf(co) ∧ wf(cl) ∧ inv(sys) → test(sys, cl, co) = test(sys, purge(cl, cdom(co)), co) | A User Theorem |
| inv-run-gen | ⊦ wf(cl) ∧ inv(sys) → inv(run(sys, cl)) | A User Theorem |
| lemma1 | ⊦ wf(cl) ∧ inv(sys) → eqd(run(sys, cl), d, run(sys, purge(cl, d))) | A User Theorem |
| lemma1-gen | ⊦ wf(cl) ∧ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) → eqd(run(sys, cl), d, run(sys0, purge(cl, d))) | A User Theorem |
| wf-purge | ⊦ wf(cl) → wf(purge(cl, cdom(co))) | A User Theorem |
| wf-rec | ⊦ wf(co ' + cl) ↔ ¬ ¬ (wf(co) ∧ wf(cl)) | A User Theorem |