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: |
|---|---|---|
| init-ex | ⊦ ∃ s. GInit(s) | An Axiom |
| init-inv-pr | ⊦ GInit(s) → GInv(s) ∧ (∀ m. Pr(m)(s)) | An Axiom |
| g-refl | ⊦ Gr(m)(s, s) | An Axiom |
| g-r | ⊦ Gr(m)(s, s0) → (∀ n. n ≠ m → Ry(n)(s, s0)) | An Axiom |
| seq-sat-rg | GInv(S), Pr(m)(S) ⊦ [: S, Out | Ry(m)(S', S''), (Gr(m)(S, S') ∧ ¬ blocked), GInv(S), SEQ#(m, Inp; S, Out)] Po(m)(S) | An Axiom |
| rely-po | ⊦ Ry(m)(s, s0) ∧ Po(m)(s) → Po(m)(s0) | An Axiom |
| rely-pr | ⊦ Ry(m)(s, s0) ∧ Pr(m)(s) → Pr(m)(s0) | An Axiom |
| r-trans | ⊦ Ry(m)(s, s0) ∧ Ry(m)(s0, s1) → Ry(m)(s, s1) | An Axiom |