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: |
|---|---|---|
| obs-in-domain | ⊦ usedName(nam) ∧ cdom(nam) ⇒ d → contents(obs(sys, d), nam) = contents(sys, nam) | An Axiom |
| obs-other-domain | ⊦ ¬ (usedName(nam) ∧ cdom(nam) ⇒ d) → contents(obs(sys, d), nam) = null | An Axiom |
| eqd-def | ⊦ eqd(sys, d, sys0) ↔ (∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| extensionality | ⊦ sys = sys0 ↔ (∀ nam. contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| RMA-2 | ⊦ eqd(sys, cdom(co), sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ alter(nam, cdom(co)) ∧ usedName(nam) → contents(step(sys, co), nam) = contents(step(sys0, co), nam) | An Axiom |
| RMA-3 | ⊦ usedName(nam) ∧ contents(step(sys, co), nam) ≠ contents(sys, nam) → alter(nam, cdom(co)) | An Axiom |
| alter-observe-respects-policy | ⊦ usedName(nam) ∧ alter(nam, d) ∧ observe(nam, d0) → d ⇒ d0 | An Axiom |
| usedName-def | ⊦ (∃ d. alter(nam, d) ∨ observe(nam, d)) → usedName(nam) | An Axiom |
| observe-all-names | ⊦ cdom(nam) ⇒ d ∧ usedName(nam) → observe(nam, d) | An Axiom |
| no-write-down | ⊦ alter(nam, d) → d ⇒ cdom(nam) | An Axiom |
| no-read-up | ⊦ observe(nam, d) → cdom(nam) ⇒ d | An Axiom |
| RMA-1 | ⊦ eqd(sys, d, sys0) → obs(sys, d) = obs(sys0, d) | A User Theorem |
| obs-is-eqd | ⊦ obs(sys, d) = obs(sys0, d) ↔ eqd(sys, d, sys0) | A User Theorem |