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: |
|---|---|---|
| CSEQ-def | An Axiom | |
| CSPAWN-def | An Axiom | |
| CGuarto-def | ⊦ CGuarto(m, act, cs, act0, cs0) ↔ (∃ m0. m0 ≤ m ∧ CGuar(m0, act, cs, act0, cs0)) | An Axiom |
| CRrelyto-def | ⊦ CRelyto(m, act, cs, act0, cs0) ↔ (∀ m0. m0 ≤ m → CRely(m0, act, cs, act0, cs0)) | An Axiom |
| CInitto-def | ⊦ CInitto(m, act1, cs1) ↔ (∀ m0. m0 ≤ m → CInit(m0, act1, cs1)) | An Axiom |
| CInit-def | ⊦ CInit(m, act1, cs1) ↔ Idle(m, cs1) ∧ ¬ act1(m) | An Axiom |
| CRely-def | ⊦ CRely(m, act1, cs1, act2, cs2) ↔ Rely(m, cs1, cs2) ∧ (Idle(m, cs1) ↔ Idle(m, cs2)) ∧ (act2(m) ↔ act1(m)) | An Axiom |
| CGuar-def | ⊦ CGuar(m, act, cs, act0, cs0) ↔ Guar(m, cs, cs0) ∧ ((¬ act(m) → Idle(m, cs)) → ¬ act0(m) → Idle(m, cs0)) ∧ (∀ m0. m0 ≠ m → (act0(m0) ↔ act(m0)) ∧ (Idle(m0, cs) ↔ Idle(m0, cs0))) | An Axiom |
| CInv-def | ⊦ CInv(m, act, cs) ↔ Inv(cs) ∧ (∀ m0. m < m0 → Idle(m0, cs) ∧ ¬ act(m0)) | An Axiom |