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_SR-def | ⊦ BSP_SR(view, trans) ↔ (∀ tr. tr ∈TR trans → proj(tr, VNview(view)) ∈TR trans) | An Axiom |
| BSP_D-def | ⊦ BSP_D(view, trans) ↔ (∀ tr, tr0, ev. view(ev) = C ∧ tr0 + (ev + tr) ∈TR trans ∧ proj(tr, Cview(view)) = [] → (∃ tr1, tr2. tr2 + tr1 ∈TR trans ∧ proj(tr1, Vview(view)) = proj(tr, Vview(view)) ∧ proj(tr1, Cview(view)) = [] ∧ proj(tr2, VCview(view)) = proj(tr0, VCview(view)))) | An Axiom |
| BSP_BSD-def | ⊦ BSP_BSD(view, trans) ↔ (∀ tr, tr0, ev. view(ev) = C ∧ tr0 + (ev + tr) ∈TR trans ∧ proj(tr, Cview(view)) = [] → (∃ tr1. tr0 + tr1 ∈TR trans ∧ proj(tr1, Vview(view)) = proj(tr, Vview(view)) ∧ proj(tr1, Cview(view)) = [])) | An Axiom |
| BSP_SD-def | ⊦ BSP_SD(view, trans) ↔ (∀ tr, tr0, ev. view(ev) = C ∧ tr0 + (ev + tr) ∈TR trans ∧ proj(tr, Cview(view)) = [] → tr0 + tr ∈TR trans) | An Axiom |
| BSP_RA-def | ⊦ BSP_RA(mkxview(view, eqrel), trans) ↔ (∀ tr, tr0, ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ tr0 + (ev + tr) ∈TR trans → (∃ tr1, tr2. tr2 + (ev0 + tr1) ∈TR trans ∧ proj(tr0, VCview(view)) = proj(tr2, VCview(view)) ∧ proj(tr, VCview(view)) = proj(tr1, VCview(view)))) | An Axiom |
| BSP_BSRA-def | ⊦ BSP_BSRA(mkxview(view, eqrel), trans) ↔ (∀ tr, tr0, ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ tr0 + (ev + tr) ∈TR trans → (∃ tr1. tr0 + (ev0 + tr1) ∈TR trans ∧ proj(tr, VCview(view)) = proj(tr1, VCview(view)))) | An Axiom |
| BSD-implies-D | ⊦ BSP_BSD(view, trans) → BSP_D(view, trans) | A User Theorem |
| BSRA-implies-RA | ⊦ BSP_BSRA(mkxview(view, eqrel), trans) → BSP_RA(mkxview(view, eqrel), trans) | A User Theorem |
| SD-equiv-BSD-N2V | ⊦ BSP_BSD(N2Vview(view), trans) ↔ BSP_SD(view, trans) | A User Theorem |
| SD-implies-BSD | ⊦ BSP_SD(view, trans) → BSP_BSD(view, trans) | A User Theorem |
| SD-implies-SR | ⊦ BSP_SD(view, trans) → BSP_SR(view, trans) | A User Theorem |