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: |
|---|---|---|
| seq-sat-rg-total-lem | GInv(S), Pr(m)(S), [:S, Outf | SEQ#(m, Inpf(m); S, Outf(m))] ⊦ (□ (Ry(m)(S', S'') ∧ GInv(S) ∧ GInv(S')) → ◇ last) ∧ (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-rg-total-correct-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+df+term | [:Inpf, S, Outf | SPAWN#(n; Inpf, S, Outf)], GInit(S) ⊦ (□ (Rton(n)(S', S'') ∧ (GInv(S') → GInv(S''))) → ◇ last) ∧ (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 |