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 ↔ (∀ 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))) | An Axiom |
| lrf-def | ⊦ lrf ↔ (∀ s, s0. ∀ ev. view(ev) = C → (reachable(s) ∧ trans(s, ev, s0) → eqstate(s0, s))) | An Axiom |