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 |
| eqlbs-def | ⊦ eqlbs(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqlb(sys, d, sys0)) | An Axiom |
| eqlb-def | ⊦ eqlb(sys, d, sys0) ↔ (∀ nam. cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam)) | An Axiom |
| 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 |
| obs-implies-lbnif-observe | obs(sys, d) = obs(sys0, d) ⊦ ∀ nam. cdom(nam) ⇒ d ∧ observe(nam, d) → contents(sys, nam) = contents(sys0, nam) | A Proof Obligation |
| LanguageBasedNIF-run | eqlbs(sys, sources(cl, d), sys0) ⊦ eqlb(run(sys, cl), d, run(sys0, cl)) | A Proof Obligation |
| LanguageBasedNIF-run-observe | eqds(sys, sources(cl, d), sys0) ⊦ eqd(run(sys, cl), d, run(sys0, cl)) | A Proof Obligation |
| eqlb-equiv-eqd | ⊦ eqlb(sys, d, sys0) ↔ eqd(sys, d, sys0) | A User Theorem |
| eqlbs-equiv-eqds | ⊦ eqlbs(sys, ds, sys0) ↔ eqds(sys, ds, sys0) | A User Theorem |
| no-write-down-follows | ∀ d. d ⇒ d ⊦ ¬ d ⇒ cdom(nam) → ¬ alter(nam, d) | A User Theorem |