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: |
|---|---|---|
| RG-restr-def | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ↔ ¬ ¬ ( (∀ s, s0. (Pre1(pm, s) ∧ R1(pm, s, s0) → Pre1(pm, s0)) ∧ (R1(pm, s, s0) ∧ I(pm, s) → I(pm, s0)) ∧ (R2(pm, s, s0) ∧ I(pm, s) → I(pm, s0)) ∧ (Pre2(pm, s) ∧ R2(pm, s, s0) → Pre2(pm, s0)) ∧ (G1(pm, s, s0) ∧ I(pm, s) → R2(pm, s, s0)) ∧ (G2(pm, s, s0) ∧ I(pm, s) → R1(pm, s, s0))) ∧ (∀ s, s0, s1. (Pre1(pm, s) ∧ Post1(pm, s, s0) ∧ I(pm, s0) ∧ R1(pm, s0, s1) → Post1(pm, s, s1)) ∧ (Pre2(pm, s) ∧ Post2(pm, s, s0) ∧ I(pm, s0) ∧ R2(pm, s0, s1) → Post2(pm, s, s1)) ∧ (R1(pm, s, s0) ∧ R1(pm, s0, s1) ∧ I(pm, s) → R1(pm, s, s1)) ∧ (R2(pm, s, s0) ∧ R2(pm, s0, s1) ∧ I(pm, s) → R2(pm, s, s1))) ∧ (∀ s. (I(pm, s) → R1(pm, s, s) ∧ R2(pm, s, s)) ∧ (Pre1(pm, s) → I(pm, s)) ∧ (Pre2(pm, s) → I(pm, s)))) | An Axiom |
| RG-restr-sym | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) → (¬ RG-restr(pm, R2, G2, Pre2, Post2, I, R1, G1, Pre1, Post1) ↔ false) | A User Theorem |
| RG2-Sound | [:S | [PL Pre1(pm, S) → R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL Pre2(pm, S) → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, S), Pre2(pm, S), S = s ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |
| RG2-Sound+Term | [:S | [PL Pre1(pm, S) → R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∧ (□ R1(pm, S', S'') → ◇ last)] ∥ [PL Pre2(pm, S) → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, S), Pre2(pm, S), S = s ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) ∧ (□ (R1(pm, S', S'') ∧ R2(pm, S', S'')) → ◇ last) | A User Theorem |
| RG2-Sound+Term-unfair | [:S | [PL Pre1(pm, S) → R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∧ (□ R1(pm, S', S'') → ◇ last)] ∥nf [PL Pre2(pm, S) → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, S), Pre2(pm, S), S = s ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) ∧ (□ (R1(pm, S', S'') ∧ R2(pm, S', S'')) → ◇ last) | A User Theorem |
| RG2-Sound-unfair | [:S | [PL Pre1(pm, S) → R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf [PL Pre2(pm, S) → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, S), Pre2(pm, S), S = s ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |
| fair-always-left-rely | RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL ◇ ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ⊦ | A User Theorem |
| fair-always-right-rely | RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL ◇ ¬ R2(pm, S', S'') ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ] ⊦ | A User Theorem |
| fair-never-violates-left-rely | RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre2(pm, s1), I(pm, s0), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL S = s] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s1, S);G2(pm, S, S'))]], ¬ R1(pm, s0, s), R1(pm, s0, S) ⊦ | A User Theorem |
| fair-never-violates-right-rely | RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s1), I(pm, s0), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s1, S);G1(pm, S, S'))] ∥ [PL S = s]], ¬ R2(pm, s0, s), R2(pm, s0, S) ⊦ | A User Theorem |
| fair-sustains-implies-always | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S) ⊦ [:S | [PL □ (R1(pm, S', S'') ∧ (last ⊃ Post1(pm, s, S);G1(pm, S, S')))] ∥ [PL □ (R2(pm, S', S'') ∧ (last ⊃ Post2(pm, s, S);G2(pm, S, S')))]] | A User Theorem |
| g1-r2 | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ G1(pm, s, s0) ∧ I(pm, s) → R2(pm, s, s0) | A User Theorem |
| g2-r1 | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ G2(pm, s, s0) ∧ I(pm, s) → R1(pm, s, s0) | A User Theorem |
| i-r1-i | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s, s0) ∧ I(pm, s) → I(pm, s0) | A User Theorem |
| i-r2-i | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R2(pm, s, s0) ∧ I(pm, s) → I(pm, s0) | A User Theorem |
| not-pre1-term-unfair | □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL ¬ Pre1(pm, S)] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, S), Pre2(pm, s) ⊦ ◇ last | A User Theorem |
| not-pre2-term-unfair | □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∧ (□ R1(pm, S', S'') → ◇ last)] ∥nf [PL ¬ Pre2(pm, S)]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre2(pm, S), Pre1(pm, s) ⊦ ◇ last | A User Theorem |
| post1-r1 | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s0, s1) ∧ Post1(pm, s, s0) ∧ Pre1(pm, s) ∧ I(pm, s0) → Post1(pm, s, s1) | A User Theorem |
| post2-r2 | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R2(pm, s0, s1) ∧ Post2(pm, s, s0) ∧ Pre2(pm, s) ∧ I(pm, s0) → Post2(pm, s, s1) | A User Theorem |
| pre1-i | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ Pre1(pm, s) → I(pm, s) | A User Theorem |
| pre1-r1 | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s, s0) ∧ Pre1(pm, s) → Pre1(pm, s0) | A User Theorem |
| pre2-i | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ Pre2(pm, s) → I(pm, s) | A User Theorem |
| pre2-r2 | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R2(pm, s, s0) ∧ Pre2(pm, s) → Pre2(pm, s0) | A User Theorem |
| r-g-r | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s, s0) ∧ G2(pm, s0, s1) ∧ R1(pm, s1, s2) ∧ I(pm, s) → R1(pm, s, s2) | A User Theorem |
| r1-refl | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ ¬ R1(pm, s, s) ∧ I(pm, s) → false | A User Theorem |
| r1-trans | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s, s0) ∧ R1(pm, s0, s1) ∧ I(pm, s) → R1(pm, s, s1) | A User Theorem |
| r2-refl | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ ¬ R2(pm, s, s) ∧ I(pm, s) → false | A User Theorem |
| r2-trans | ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R2(pm, s, s0) ∧ R2(pm, s0, s1) ∧ I(pm, s) → R2(pm, s, s1) | A User Theorem |
| rg-blocked1-not-r1-term-unfair | [:S | [PL S = s] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s1, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), R1(pm, s0, S), ¬ R1(pm, s0, s), Pre2(pm, s1), I(pm, s0) ⊦ ◇ last | A User Theorem |
| rg-blocked1-not-r1-unfair | [:S | [PL S = s] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s1, S);G2(pm, S, S'))]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), R1(pm, s0, S), ¬ R1(pm, s0, s), I(pm, s0), Pre1(pm, s1), Pre2(pm, s1) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s1, S) ∧ Post2(pm, s1, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |
| rg-blocked2-not-r2-term-unfair | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s1, S);G1(pm, S, S')) ∧ (□ R1(pm, S', S'') → ◇ last)] ∥nf [PL S = s]], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), R2(pm, s0, S), ¬ R2(pm, s0, s), Pre1(pm, s1), I(pm, s0) ⊦ ◇ last | A User Theorem |
| rg-blocked2-not-r2-unfair | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s1, S);G1(pm, S, S'))] ∥nf [PL S = s]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), R2(pm, s0, S), ¬ R2(pm, s0, s), I(pm, s0), Pre1(pm, s1), Pre2(pm, s1) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s1, S) ∧ Post2(pm, s1, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |
| rg2-lem1-term-unfair | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∧ ◇ ¬ R1(pm, S', S'')] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S) ⊦ ◇ last | A User Theorem |
| rg2-lem2-term-unfair | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∧ ◇ last] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ], □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre1-unfair | [:S | [PL ¬ Pre1(pm, S)] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, S), Pre2(pm, s) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |
| rg2-not-pre2-unfair | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf [PL ¬ Pre2(pm, S)]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre2(pm, S), Pre1(pm, s) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |
| rg2-sound+term-unfair-main | □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S')) ∧ (□ R1(pm, S', S'') → ◇ last)] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S) ⊦ ◇ last | A User Theorem |
| rg2-sound-main-unfair | [:S | [PL R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]], RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, S) ⊦ (R1(pm, S', S'') ∧ R2(pm, S', S'')) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) | A User Theorem |