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: |
|---|---|---|
| dom-equal | ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, cdom(sys, co), sys0) → cdom(sys, co) = cdom(sys0, co) | An Axiom |
| dom-equiv | ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) → (cdom(sys, co) ⇒ d ↔ cdom(sys0, co) ⇒ d) | An Axiom |
| inv-exec | ⊦ inv(sys) → inv(exec(sys, co) .1) | An Axiom |
| inv-init | ⊦ inv(initialstate) | An Axiom |
| eqd-refl | ⊦ eqd(sys, d, sys) | An Axiom |
| eqd-symm | ⊦ eqd(sys, d, sys0) → eqd(sys0, d, sys) | An Axiom |
| eqd-trans | ⊦ eqd(sys, d, sys0) ∧ eqd(sys0, d, sys1) → eqd(sys, d, sys1) | An Axiom |
| locally-respects | ⊦ inv(sys) ∧ ¬ cdom(sys, co) ⇒ d0 → eqd(sys, d0, exec(sys, co) .1) | An Axiom |
| output-cons | ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, cdom(sys, co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2 | An Axiom |
| weakly-step-consistent | ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) ∧ eqd(sys, cdom(sys, co), sys0) → eqd(exec(sys, co) .1, d, exec(sys0, co) .1) | An Axiom |
| eqd-symm-lem | ⊦ eqd(sys, d, sys0) → (¬ eqd(sys0, d, sys) ↔ false) | A User Theorem |
| eqd-trans-lem | ⊦ eqd(sys, d, sys0) ∧ eqd(sys0, d, sys1) → (¬ eqd(sys, d, sys1) ↔ false) | A User Theorem |
| inv-exec-lem | ⊦ inv(sys) → (¬ inv(exec(sys, co) .1) ↔ false) | A User Theorem |