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(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ↔ (∀ s, s0. (G1(s, s0) → R2(s, s0)) ∧ (G2(s, s0) → R1(s, s0)) ∧ (Pre1(s) ∧ R1(s, s0) → Pre1(s0)) ∧ (Pre2(s) ∧ R2(s, s0) → Pre2(s0)) ∧ (Post1(s) ∧ R1(s, s0) → Post1(s0)) ∧ (Post2(s) ∧ R2(s, s0) → Post2(s0))) ∧ (∀ s, s0, s1. (R1(s, s0) ∧ R1(s0, s1) → R1(s, s1)) ∧ (R2(s, s0) ∧ R2(s0, s1) → R2(s, s1))) ∧ (∀ s. (∃ s. Init(s)) ∧ (Init(s) → Pre1(s) ∧ Pre2(s) ∧ Inv(s)) ∧ R1(s, s) ∧ R2(s, s) ∧ (Inv(s) → Runs1(s) ∨ Runs2(s)) ∧ (Post1(s) → Runs2(s)) ∧ (Post2(s) → Runs1(s))) | An Axiom |
| RG2-Sound+DF | [:S | [PL Pre1(S) ∧ Inv(S) → (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL Pre2(S) ∧ Inv(S) → (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Init(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| RG2-Sound+DF+Term | [:S | [PL Pre1(S) ∧ Inv(S) → (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL Pre2(S) ∧ Inv(S) → (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Init(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) ∧ (□ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) → ◇ last) | A User Theorem |
| RG2-Sound+DF+Term-unfair | [:S | [PL Pre1(S) ∧ Inv(S) → (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥nf [PL Pre2(S) ∧ Inv(S) → (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Init(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) ∧ (□ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) → ◇ last) | A User Theorem |
| RG2-Sound+DF-unfair | [:S | [PL Pre1(S) ∧ Inv(S) → (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥nf [PL Pre2(S) ∧ Inv(S) → (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Init(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| g1-r2 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ G1(s, s0) → R2(s, s0) | A User Theorem |
| g2-r1 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ G2(s, s0) → R1(s, s0) | A User Theorem |
| not-pre1-term-unfair | □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), [:S | [PL ¬ Pre1(S) ∨ ¬ Inv(S)] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Pre1(S), Inv(S) ⊦ ◇ last | A User Theorem |
| not-pre2-term-unfair | □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥nf [PL ¬ Pre2(S) ∨ ¬ Inv(S)] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Pre2(S), Inv(S) ⊦ ◇ last | A User Theorem |
| post1-r1 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R1(s, s0) ∧ Post1(s) → Post1(s0) | A User Theorem |
| post1-runs2 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ Post1(s) → Runs2(s) | A User Theorem |
| post2-r1 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R2(s, s0) ∧ Post2(s) → Post2(s0) | A User Theorem |
| post2-runs1 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ Post2(s) → Runs1(s) | A User Theorem |
| pre1-r1 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R1(s, s0) ∧ Pre1(s) → Pre1(s0) | A User Theorem |
| pre2-r2 | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R2(s, s0) ∧ Pre2(s) → Pre2(s0) | A User Theorem |
| r-g-r | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R1(s, s0) ∧ G2(s0, s1) ∧ R1(s1, s2) → R1(s, s2) | A User Theorem |
| r1-trans | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R1(s, s0) ∧ R1(s0, s1) → R1(s, s1) | A User Theorem |
| r2-trans | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ R2(s, s0) ∧ R2(s0, s1) → R2(s, s1) | A User Theorem |
| rg-blocked1-not-r1 | [:S | [PL S = s] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))]], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R1(s0, S), ¬ R1(s0, s) ∨ ¬ Inv(s) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg-blocked1-not-r1-term | [:S | [PL S = s] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))]], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R1(s0, S), ¬ R1(s0, s) ∨ ¬ Inv(s) ⊦ ◇ last | A User Theorem |
| rg-blocked1-not-r1-term-unfair | [:S | [PL S = s] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R1(s0, S), ¬ R1(s0, s) ∨ ¬ Inv(s) ⊦ ◇ last | A User Theorem |
| rg-blocked1-not-r1-unfair | [:S | [PL S = s] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R1(s0, S), ¬ R1(s0, s) ∨ ¬ Inv(s) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg-blocked2-not-r2 | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL S = s]], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R2(s0, S), ¬ R2(s0, s) ∨ ¬ Inv(s) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg-blocked2-not-r2-term | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL S = s]], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R2(s0, S), ¬ R2(s0, s) ∨ ¬ Inv(s) ⊦ ◇ last | A User Theorem |
| rg-blocked2-not-r2-term-unfair | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥nf [PL S = s] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R2(s0, S), ¬ R2(s0, s) ∨ ¬ Inv(s) ⊦ ◇ last | A User Theorem |
| rg-blocked2-not-r2-unfair | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥nf [PL S = s] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), R2(s0, S), ¬ R2(s0, s) ∨ ¬ Inv(s) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-lem1-term | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ ◇ (¬ R1(S', S'') ∨ ¬ Inv(S) ∨ ¬ Inv(S')) ] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), □ ((G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-lem1-term-strnger | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ ◇ (¬ R1(S', S'') ∨ ¬ Inv(S) ∨ ¬ Inv(S')) ] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-lem1-term-strnger-term-unfair | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ ◇ (¬ R1(S', S'') ∨ ¬ Inv(S) ∨ ¬ Inv(S')) ] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-lem2-term | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ ◇ (¬ R2(S', S'') ∨ ¬ Inv(S) ∨ ¬ Inv(S')) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), □ ((G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-lem2-term-strnger | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ ◇ (¬ R2(S', S'') ∨ ¬ Inv(S) ∨ ¬ Inv(S')) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-lem2-term-strnger-term-unfair | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ ◇ last] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre1 | [:S | [PL ¬ Pre1(S) ∨ ¬ Inv(S)] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), Pre1(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-not-pre1-term | [:S | [PL ¬ Pre1(S) ∨ ¬ Inv(S)] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ ((G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked), □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Pre1(S), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre1-term-strnger | [:S | [PL ¬ Pre1(S) ∨ ¬ Inv(S)] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Pre1(S), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre1-unfair | [:S | [PL ¬ Pre1(S) ∨ ¬ Inv(S)] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), Pre1(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-not-pre2 | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL ¬ Pre2(S) ∨ ¬ Inv(S)] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), Pre2(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-not-pre2-term | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL ¬ Pre2(S) ∨ ¬ Inv(S)] ], □ ((G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked), □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Pre2(S), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre2-term-strnger | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL ¬ Pre2(S) ∨ ¬ Inv(S)] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Pre2(S), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre2-unfair | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥nf [PL ¬ Pre2(S) ∨ ¬ Inv(S)] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S), Pre2(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-sound-main | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-sound-main-term-unfair | □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-sound-main-unfair | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥nf [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2), Inv(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(S) ∧ Post2(S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| runs | ⊦ RG-restr(Init, Inv, R1, G1, Pre1, Post1, Runs1, R2, G2, Pre2, Post2, Runs2) ∧ Inv(s) ∧ ¬ Runs2(s) → Runs1(s) | A User Theorem |