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: |
|---|---|---|
| eqstate-reflexive | ⊦ ∀ s. eqstate(s, s) | An Axiom |
| validx-def | ⊦ validx ↔ (∀ ev. view(ev) = C → eqrel(ev, ev)) ∧ (∀ ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) → eqrel(ev0, ev)) ∧ (∀ ev, ev0, ev1. view(ev) = C ∧ view(ev0) = C ∧ view(ev1) = C ∧ eqrel(ev, ev0) ∧ eqrel(ev0, ev1) → eqrel(ev, ev1)) ∧ (∀ ev, ev0. view(ev) = C ∧ eqrel(ev, ev0) → view(ev0) = C) ∧ (∀ ev, ev0. view(ev0) = C ∧ eqrel(ev, ev0) → view(ev) = C) | An Axiom |
| xosc-def | ⊦ xosc ↔ (∀ 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 |
| xlrf-def | ⊦ xlrf ↔ (∀ 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))) | An Axiom |