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_BSD-def | ⊦ BSP_BSD ↔ (∀ tr, tr0, ev. view(ev) = C ∧ (tr0 + (ev + tr)) ∈TR ∧ proj(tr, Cview(view)) = [] → (∃ tr1. (tr0 + tr1) ∈TR ∧ proj(tr1, Vview(view)) = proj(tr, Vview(view)) ∧ proj(tr1, Cview(view)) = [])) | An Axiom |
| BSD-unwind-theorem | ⊦ lrf ∧ osc → BSP_BSD | A User Theorem |
| lemma-5-4-2 | osc ⊦ ∀ s1, s11. ∀ tr. proj(tr, Cview(view)) = [] ∧ reachable(s1) ∧ reachable(s11) → (enabled(s11, tr) ∧ eqstate(s11, s1) → (∃ tr0. proj(tr0, Cview(view)) = [] ∧ proj(tr0, Vview(view)) = proj(tr, Vview(view)) ∧ enabled(s1, tr0))) | A User Theorem |
| osc-help | osc, view(ev) ≠ C, reachable(s1), reachable(s11), trans(s11, ev, s2), eqstate(s11, s1) ⊦ ∃ s22, tr1. proj(tr1, Cview(view)) = [] ∧ proj(tr1, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(s1, tr1, s22) ∧ eqstate(s2, s22) | A User Theorem |