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: |
|---|---|---|
| proc2-rg-totalcorr | Pre2(s, S), Inv(S) ⊦ ⟨:S | R2(S', S''), (G2(S, S') ∧ (Runs2(S) → ¬ blocked)), Inv(S), Proc2(; S)⟩ Post2(s, S) | An Axiom |
| proc1-rg-totalcorr | Pre1(s, S), Inv(S) ⊦ ⟨:S | R1(S', S''), (G1(S, S') ∧ (Runs1(S) → ¬ blocked)), Inv(S), Proc1(; S)⟩ Post1(s, S) | An Axiom |
| post2-runs1 | ⊦ Post2(s, s0) → (¬ Runs1(s0) ↔ false) | An Axiom |
| post1-runs2 | ⊦ Post1(s, s0) → (¬ Runs2(s0) ↔ false) | An Axiom |
| inv-runs | ⊦ Inv(s) → Runs1(s) ∨ Runs2(s) | An Axiom |
| r2-trans | ⊦ R2(s, s0) ∧ R2(s0, s1) → (¬ R2(s, s1) ↔ false) | An Axiom |
| r1-trans | ⊦ R1(s, s0) ∧ R1(s0, s1) → (¬ R1(s, s1) ↔ false) | An Axiom |
| r2-refl | ⊦ R2(s, s) | An Axiom |
| r1-refl | ⊦ R1(s, s) | An Axiom |
| g2-r1 | ⊦ G2(s, s0) → (¬ R1(s, s0) ↔ false) | An Axiom |
| g1-r2 | ⊦ G1(s, s0) → (¬ R2(s, s0) ↔ false) | An Axiom |
| post2-stable-r2 | ⊦ Post2(s, s0) ∧ R2(s0, s1) → (¬ Post2(s, s1) ↔ false) | An Axiom |
| post1-stable-r1 | ⊦ Post1(s, s0) ∧ R1(s0, s1) → (¬ Post1(s, s1) ↔ false) | An Axiom |
| pre2-stable-r2 | ⊦ Pre2(s, s0) ∧ R2(s0, s1) → (¬ Pre2(s, s1) ↔ false) | An Axiom |
| pre1-stable-r1 | ⊦ Pre1(s, s0) ∧ R1(s0, s1) → (¬ Pre1(s, s1) ↔ false) | An Axiom |
| init-pre-inv | ⊦ Init(s) → Pre1(s, s) ∧ Pre2(s, s) ∧ Inv(s) | An Axiom |
| init-ex | ⊦ ∃ s. Init(s) | An Axiom |
| RG2-Sound+DF | [:S | [PL Pre1(s, S) ∧ Inv(S) → (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ] ∥ [PL Pre2(s, S) ∧ Inv(S) → (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(s, S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ] ], Init(S), s = S ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S) ∧ Post2(s, 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, S) ∧ Inv(S) → (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL Pre2(s, S) ∧ Inv(S) → (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(s, S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked)) ∧ (□ (R2(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ], s = S, Init(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S) ∧ Post2(s, 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-Strong-Total-Corr | Init(S), S = s ⊦ ⟨:S | (R1(S', S'') ∧ R2(S', S'')), ((G1(S, S') ∨ G2(S, S')) ∧ ¬ blocked), Inv(S), Proc1(; S) ∥ Proc2(; S)⟩ (Post1(s, S) ∧ Post2(s, S) ∧ Inv(S)) | A User Theorem |
| po1-g-r-stable | ⊦ Post1(s, s0) ∧ G2(s0, s1) ∧ R1(s1, s2) → Post1(s, s2) | A User Theorem |
| po2-g-r-stable | ⊦ Post2(s, s0) ∧ G1(s0, s1) ∧ R2(s1, s2) → Post2(s, s2) | A User Theorem |
| pre1-g-r-stable | ⊦ Pre1(s, s0) ∧ G2(s0, s1) ∧ R1(s1, s2) → Pre1(s, s2) | A User Theorem |
| pre2-g-r-stable | ⊦ Pre2(s, s0) ∧ G1(s0, s1) ∧ R2(s1, s2) → Pre2(s, s2) | A User Theorem |
| r1-g2-r1 | ⊦ R1(s, s0) ∧ G2(s0, s1) → R1(s, s1) | A User Theorem |
| r2-g1-r2 | ⊦ R2(s, s0) ∧ G1(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(s1, S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], Inv(S), R1(s0, S), ¬ R1(s0, s) ∨ ¬ Inv(s) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s1, S) ∧ Post2(s1, 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(s1, S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), Inv(S), R1(s0, S), ¬ R1(s0, s) ∨ ¬ Inv(s) ⊦ ◇ last | A User Theorem |
| rg-blocked2-not-r2 | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s1, S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL S = s] ], Inv(S), R2(s0, S), ¬ R2(s0, s) ∨ ¬ Inv(s) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s1, S) ∧ Post2(s1, 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(s1, 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''))), Inv(S), R2(s0, S), ¬ R2(s0, s) ∨ ¬ Inv(s) ⊦ ◇ last | A User Theorem |
| rg2-lem1-term-strnger | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, 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, 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''))), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-lem2-term-strnger | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, 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, 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''))), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre1 | [:S | [PL ¬ Pre1(s, S) ∨ ¬ Inv(S)] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(s, S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], Inv(S), Pre1(s, S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S) ∧ Post2(s, S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-not-pre1-term-strnger | [:S | [PL ¬ Pre1(s, S) ∨ ¬ Inv(S)] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(s, 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''))), Pre1(s, S), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-not-pre2 | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL ¬ Pre2(s, S) ∨ ¬ Inv(S)] ], Inv(S), Pre2(s, S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S) ∧ Post2(s, S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |
| rg2-not-pre2-term-strnger | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked)) ∧ (□ (R1(S', S'') ∧ Inv(S) ∧ Inv(S')) → ◇ last) ] ∥ [PL ¬ Pre2(s, S) ∨ ¬ Inv(S)] ], □ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))), Pre2(s, S), Inv(S) ⊦ ◇ last | A User Theorem |
| rg2-sound-main | [:S | [PL (R1(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S);G1(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs1(S) → ¬ blocked))] ∥ [PL (R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post2(s, S);G2(S, S') ∧ (Inv(S) → Inv(S')) ∧ (Inv(S) ∧ Runs2(S) → ¬ blocked))] ], Inv(S) ⊦ (R1(S', S'') ∧ R2(S', S'') ∧ (Inv(S') → Inv(S''))) -+-> (last ⊃ Post1(s, S) ∧ Post2(s, S) ∧ Inv(S);(G1(S, S') ∨ G2(S, S')) ∧ (Inv(S) → Inv(S')) ∧ ¬ blocked) | A User Theorem |