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: |
|---|---|---|
| gto-def | ⊦ Gton(n)(s, s0) ↔ (∃ m. m ≤ n ∧ Gr(m)(s, s0)) | An Axiom |
| rton-def | ⊦ Rton(n)(s, s0) ↔ (∀ m. m ≤ n → Ry(m)(s, s0)) | An Axiom |
| poton-def | ⊦ Poton(n)(s) ↔ (∀ m. m ≤ n → Po(m)(s)) | An Axiom |
| prton-def | ⊦ Prton(n)(s) ↔ (∀ m. m ≤ n → Pr(m)(s)) | An Axiom |
| rg-restr1 | ⊦ ¬ RG-restr(GInit, GInv, Ry(n0 + 1), Gr(n0 + 1), Pr(n0 + 1), Po(n0 + 1), λ s. true, Rton(n0), Gton(n0), Pr(n0), Poton(n0), λ s. true) ↔ false | A User Theorem |
| rg-restr2 | ⊦ ¬ RG-restr(GInit, GInv, Ry(n0 + 1), Gr(n0 + 1), Pr(n0 + 1), Po(n0 + 1), λ s. true, Rton(n0), Gton(n0), Prton(n0), Poton(n0), λ s. true) ↔ false | A User Theorem |
| seq-sat-rg | [:Inpf, S, Outf | SEQ#(m, Inpf(m); S, Outf(m))], GInv(S), Pr(m)(S) ⊦ (Ry(m)(S', S'') ∧ (GInv(S') → GInv(S''))) -+-> (last ⊃ Po(m)(S) ∧ GInv(S);Gr(m)(S, S') ∧ ¬ blocked ∧ (GInv(S) → GInv(S'))) | A User Theorem |
| spawn-partial-corr-strng | GInit(S) ⊦ [: Inpf, S, Outf | Rton(n)(S', S''), (Gton(n)(S, S') ∧ ¬ blocked), GInv(S), SPAWN#(n; Inpf, S, Outf)] (Poton(n)(S) ∧ GInv(S)) | A User Theorem |
| spawn-sat-rg | [:Inpf, S, Outf | SPAWN#(n; Inpf, S, Outf)], GInit(S) ⊦ (Rton(n)(S', S'') ∧ (GInv(S') → GInv(S''))) -+-> (last ⊃ Poton(n)(S) ∧ GInv(S);Gton(n)(S, S') ∧ ¬ blocked ∧ (GInv(S) → GInv(S'))) | A User Theorem |
| spawn-sat-rg-strnger | [:Inpf, S, Outf | SPAWN#(n; Inpf, S, Outf)], GInv(S), Prton(n)(S) ⊦ (Rton(n)(S', S'') ∧ (GInv(S') → GInv(S''))) -+-> (last ⊃ Poton(n)(S) ∧ GInv(S);Gton(n)(S, S') ∧ ¬ blocked ∧ (GInv(S) → GInv(S'))) | A User Theorem |