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: |
|---|---|---|
| BSP_BSRA-def | ⊦ BSP_BSRA ↔ (∀ tr, tr0, ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ (tr0 + (ev + tr)) ∈TR → (∃ tr1. (tr0 + (ev0 + tr1)) ∈TR ∧ proj(tr, VCview(view)) = proj(tr1, VCview(view)))) | An Axiom |
| unwind-BSRA-theorem | ⊦ xlrf ∧ xosc ∧ validx ∧ (∀ s. eqstate(s, s)) → BSP_BSRA | A User Theorem |
| xlrf-intro | ⊦ ¬ (∀ s, s0, s1. ∀ ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ reachable(s) ∧ trans(s, ev, s0) ∧ eqstate(s, s1) ∧ reachable(s1) → (∃ s2. trans(s1, ev0, s2) ∧ eqstate(s0, s2))) → ¬ xlrf | A User Theorem |
| xlrf-property | xlrf, xosc, ∀ ev1. view(ev1) = C → eqrel(ev1, ev1) ⊦ ∀ s1, s11, s2. ∀ tr. reachable(s1) ∧ reachable(s11) ∧ trans∃(s1, tr, s2) ∧ eqstate(s1, s11) → (∃ tr0, s22. proj(tr0, VCview(view)) = proj(tr, VCview(view)) ∧ trans∃(s11, tr0, s22) ∧ eqstate(s2, s22)) | A User Theorem |
| xosc-intro | ⊦ ¬ (∀ s1, s11, s22. ∀ ev. view(ev) ≠ C ∧ reachable(s1) ∧ reachable(s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1) → (∃ s2. ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(s1, tr, s2) ∧ eqstate(s22, s2))) → ¬ xosc | A User Theorem |