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: |
|---|---|---|
| inv-exec | ⊦ inv(sys) → inv(exec(sys, co) .1) | 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 |
| output-consistent | ⊦ wf(co) ∧ inv(sys) ∧ inv(sys0) ∧ eqd(sys, cdom(co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2 | An Axiom |
| locally-respects | ⊦ wf(co) ∧ inv(sys) ∧ ¬ cdom(co) ⇒ d0 → eqd(sys, d0, exec(sys, co) .1) | An Axiom |
| step-consistent | ⊦ wf(co) ∧ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) → eqd(exec(sys, co) .1, d, exec(sys0, co) .1) | An Axiom |