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) → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| obs-in-domain | ⊦ observe(nam, d) → contents(obs(sys, d), nam) = contents(sys, nam) | An Axiom |
| obs-other-domain | ⊦ ¬ observe(nam, d) → contents(obs(sys, d), nam) = null | An Axiom |
| RMA-2 | ⊦ eqd(sys, cdom(co), 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) → d ⇒ d0 | An Axiom |
| extensionality | ⊦ sys = sys0 ↔ (∀ nam. contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| RMA-1 | ⊦ eqd(sys, d, sys0) → obs(sys, d) = obs(sys0, d) | A User Theorem |
| eqd-is-equivalent-to-obs | ⊦ eqd(sys, d, sys0) ↔ obs(sys, d) = obs(sys0, d) | A User Theorem |