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: |
|---|---|---|
| COP-sat-rely-guar | Idle(n, CS), Inv(CS) ⊦ [: CS, Outp | (Rely(n, CS', CS'') ∧ (Idle(n, CS') ↔ Idle(n, CS''))) , (Guar(n, CS, CS') ∧ (∀ m. m ≠ n → (Idle(m, CS) ↔ Idle(m, CS')))) , Inv(CS) , COP(n, Inp; CS, Outp) ] (Idle(n, CS) ∧ Inv(CS)) | An Axiom |
| init-ex | ⊦ ∃ cs. Init(cs) | An Axiom |
| init-idle | ⊦ Init(cs) → (∀ n. Idle(n, cs)) | An Axiom |
| init-inv | ⊦ Init(cs) → (¬ Inv(cs) ↔ false) | An Axiom |
| g-r | ⊦ m ≠ n ∧ Guar(m, cs1, cs2) ∧ Inv(cs1) ∧ Inv(cs2) → (¬ Rely(n, cs1, cs2) ↔ false) | An Axiom |
| g-refl | ⊦ Inv(cs) → (¬ Guar(m, cs, cs) ↔ false) | An Axiom |
| r-trans | ⊦ Rely(m, cs1, cs2) ∧ Rely(m, cs2, cs3) ∧ Inv(cs1) → Rely(m, cs1, cs3) | An Axiom |