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: |
|---|---|---|
| osc-def | ⊦ osc(view, trans, eqstate) ↔ (∀ s1, s11, s22. ∀ ev. view(ev) ≠ C ∧ reachable(trans, s1) ∧ reachable(trans, s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1) → (∃ s2. ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(trans, s1, tr, s2) ∧ eqstate(s22, s2))) | An Axiom |
| lrf-def | ⊦ lrf(view, trans, eqstate) ↔ (∀ s, s0. ∀ ev. view(ev) = C → (reachable(trans, s) ∧ trans(s, ev, s0) → eqstate(s0, s))) | An Axiom |
| xlrf-def | ⊦ xlrf(mkxview(view, eqrel), trans, eqstate) ↔ (∀ s, s0, s1. ∀ ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ reachable(trans, s) ∧ trans(s, ev, s0) ∧ eqstate(s, s1) ∧ reachable(trans, s1) → (∃ s2. trans(s1, ev0, s2) ∧ eqstate(s0, s2))) | An Axiom |
| xosc-def | ⊦ xosc(mkxview(view, eqrel), trans, eqstate) ↔ (∀ s1, s11, s22. ∀ ev. view(ev) ≠ C ∧ reachable(trans, s1) ∧ reachable(trans, s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1) → (∃ s2. ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(trans, s1, tr, s2) ∧ eqstate(s22, s2))) | An Axiom |
| isEqRel-def | ⊦ isEqRel(eqstate) ↔ (∀ s. eqstate(s, s)) ∧ (∀ s, s0. eqstate(s, s0) → eqstate(s0, s)) ∧ (∀ s, s0, s1. eqstate(s, s0) ∧ eqstate(s0, s1) → eqstate(s, s1)) | An Axiom |
| isEqRel-reflexive | ⊦ ¬ eqstate(s, s) → ¬ isEqRel(eqstate) | A User Theorem |
| isEqRel-symmetric | ⊦ ¬ eqstate(s, s0) ∧ eqstate(s0, s) → ¬ isEqRel(eqstate) | A User Theorem |
| isEqRel-transitive | ⊦ ¬ eqstate(s2, s0) ∧ eqstate(s1, s0) ∧ eqstate(s2, s1) → ¬ isEqRel(eqstate) | A User Theorem |
| lemma-5-4-2 | osc(view, trans, eqstate) ⊦ ∀ s1, s11. ∀ tr. proj(tr, Cview(view)) = [] ∧ reachable(trans, s1) ∧ reachable(trans, s11) → ( enabled(trans, s11, tr) ∧ eqstate(s11, s1) → (∃ tr0. proj(tr0, Cview(view)) = [] ∧ proj(tr0, Vview(view)) = proj(tr, Vview(view)) ∧ enabled(trans, s1, tr0))) | A User Theorem |
| lrf-intro | ⊦ ¬ (∀ s, s0. ∀ ev. view(ev) = C → (reachable(trans, s) ∧ trans(s, ev, s0) → eqstate(s0, s))) → ¬ lrf(view, trans, eqstate) | A User Theorem |
| osc-help | osc(view, trans, eqstate), view(ev) ≠ C, reachable(trans, s1), reachable(trans, s11), trans(s11, ev, s2), eqstate(s11, s1) ⊦ ∃ s22, tr1. proj(tr1, Cview(view)) = [] ∧ proj(tr1, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(trans, s1, tr1, s22) ∧ eqstate(s2, s22) | A User Theorem |
| osc-intro | ⊦ ¬ (∀ s1, s11, s22. ∀ ev. view(ev) ≠ C ∧ reachable(trans, s1) ∧ reachable(trans, s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1) → (∃ s2. ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(trans, s1, tr, s2) ∧ eqstate(s22, s2))) → ¬ osc(view, trans, eqstate) | A User Theorem |
| unwind-BSD-theorem | ⊦ lrf(view, trans, eqstate) ∧ osc(view, trans, eqstate) → BSP_BSD(view, trans) | A User Theorem |
| unwind-BSRA-theorem | ⊦ xlrf(xview, trans, eqstate) ∧ xosc(xview, trans, eqstate) ∧ validx(xview) ∧ (∀ s. eqstate(s, s)) → BSP_BSRA(xview, trans) | A User Theorem |
| unwind-SD-theorem | ⊦ view0 = N2Vview(view) ∧ lrf(view0, trans, eqstate) ∧ osc(view0, trans, eqstate) → BSP_SD(view, trans) | A User Theorem |
| xlrf-intro | ⊦ ¬ (∀ s, s0, s1. ∀ ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ reachable(trans, s) ∧ trans(s, ev, s0) ∧ eqstate(s, s1) ∧ reachable(trans, s1) → (∃ s2. trans(s1, ev0, s2) ∧ eqstate(s0, s2))) → ¬ xlrf(mkxview(view, eqrel), trans, eqstate) | A User Theorem |
| xlrf-property | xlrf(mkxview(view, eqrel), trans, eqstate), xosc(mkxview(view, eqrel), trans, eqstate), ∀ ev1. view(ev1) = C → eqrel(ev1, ev1) ⊦ ∀ s1, s11, s2. ∀ tr. reachable(trans, s1) ∧ reachable(trans, s11) ∧ trans∃(trans, s1, tr, s2) ∧ eqstate(s1, s11) → (∃ tr0, s22. proj(tr0, VCview(view)) = proj(tr, VCview(view)) ∧ trans∃(trans, s11, tr0, s22) ∧ eqstate(s2, s22)) | A User Theorem |
| xosc-is-osc | ⊦ xosc(mkxview(view, eqrel), trans, eqstate) ↔ osc(view, trans, eqstate) | A User Theorem |