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: |
|---|---|---|
| no-read-up | ⊦ observe(nam, d) → cdom(nam) ⇒ d | An Axiom |
| no-write-down | ⊦ alter(nam, d) → d ⇒ cdom(nam) | An Axiom |
| observe-all-names | ⊦ cdom(nam) ⇒ d → observe(nam, d) | An Axiom |
| eqlb-def | ⊦ eqlb(sys, d, sys0) ↔ (∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| obs-implies-lbnif-weaker | obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. cdom(nam) ⇒ d ∧ observe(nam, d) → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| eqd-implies-lbnif | eqd(sys, d, sys0) ⊦ ∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| obs-implies-lbnif | obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| LanguageBasedNIF-run | ∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam) ⊦ ∀ nam. cdom(nam) ⇒ d → contents(run(sys, cl), nam) = contents(run(sys0, cl), nam) | A Proof Obligation |
| LanguageBasedNIF-observe-run | eqd(sys, d, sys0) ⊦ ∀ nam. observe(nam, d) → contents(run(sys, cl), nam) = contents(run(sys0, cl), nam) | A Proof Obligation |
| eqlb-run | ⊦ eqlb(sys, d, sys0) → eqlb(run(sys, cl), d, run(sys0, cl)) | A User Theorem |