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: |
|---|---|---|
| eqd-def | ⊦ eqd(sys, d, sys0) ↔ (∀ nam. observe(nam, d) ∧ ¬ isState(nam) → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| obs-in-domain | ⊦ observe(nam, d) ∧ ¬ isState(nam) → contents(obs(sys, d), nam) = contents(sys, nam) | An Axiom |
| obs-other-domain | ⊦ ¬ (observe(nam, d) ∧ ¬ isState(nam)) → contents(obs(sys, d), nam) = null | An Axiom |
| extensionality | ⊦ sys = sys0 ↔ (∀ nam. contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| RMA-2 | ⊦ eqd(sys, cdom(co), sys0) ∧ eqS(sys, sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ alter(nam, cdom(co)) → contents(step(sys, co), nam) = contents(step(sys0, co), nam) | An Axiom |
| RMA-3 | ⊦ contents(step(sys, co), nam) ≠ contents(sys, nam) → alter(nam, cdom(co)) | An Axiom |
| alter-observe-respects-policy | ⊦ alter(nam, d) ∧ observe(nam, d0) ∧ ¬ isState(nam) → d ⇒ d0 | An Axiom |
| eqS-def | ⊦ eqS(sys, sys0) ↔ (∀ nam. isState(nam) → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| ipurged-req | ⊦ isState(nam) → contents(step(sys, ipurged(co)), nam) = contents(step(sys, co), nam) | An Axiom |
| ipurged-dom | ⊦ cdom(ipurged(co)) = cdom(co) | An Axiom |
| ipurged-not | ⊦ ¬ isState(nam) → contents(step(sys, ipurged(co)), nam) = contents(sys, nam) | An Axiom |
| ipurged-id | ⊦ ipurged(ipurged(co)) = ipurged(co) | An Axiom |
| eqs-step | ⊦ eqS(sys, sys0) → eqS(step(sys, co), step(sys0, co)) | An Axiom |
| RMA-1 | ⊦ eqd(sys, d, sys0) → obs(sys, d) = obs(sys0, d) | A Proof Obligation |