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: |
|---|---|---|
| input-output-disjoint | ⊦ ¬ (isInput(ev) ∧ isOutput(ev)) | An Axiom |
| projection-empty | ⊦ proj([], inevs) = [] | An Axiom |
| projection-remove | ⊦ ¬ inevs(ev) → proj(ev ' + tr, inevs) = proj(tr, inevs) | An Axiom |
| projection-keep | ⊦ inevs(ev) → proj(ev ' + tr, inevs) = ev ' + proj(tr, inevs) | An Axiom |
| Vview-def | ⊦ Vview(view) = (λ ev. view(ev) = V) | An Axiom |
| Nview-def | ⊦ Nview(view) = (λ ev. view(ev) = N) | An Axiom |
| Cview-def | ⊦ Cview(view) = (λ ev. view(ev) = C) | An Axiom |
| isTransition-def | ⊦ isTransition(trans) ↔ (∀ s, s0, s1, ev. trans(s, ev, s0) ∧ trans(s, ev, s1) → s0 = s1) | An Axiom |
| transex-rec | ⊦ trans∃(trans, s, ev ' + tr, s0) ↔ (∃ s1. trans(s, ev, s1) ∧ trans∃(trans, s1, tr, s0)) | An Axiom |
| transex-empty | ⊦ trans∃(trans, s, [], s0) ↔ s = s0 | An Axiom |
| reachable-def | ⊦ reachable(trans, s) ↔ (∃ tr. trans∃(trans, S0, tr, s)) | An Axiom |
| VCview-def | ⊦ VCview(view) = (λ ev. view(ev) = V ∨ view(ev) = C) | An Axiom |
| VNview-def | ⊦ VNview(view) = (λ ev. view(ev) = V ∨ view(ev) = N) | An Axiom |
| enabled-def | ⊦ enabled(trans, s, tr) ↔ (∃ s0. trans∃(trans, s, tr, s0)) | An Axiom |
| in-trace-def | ⊦ tr ∈TR trans ↔ enabled(trans, S0, tr) | An Axiom |
| validx-def | ⊦ validx(mkxview(view, eqrel)) ↔ (∀ 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 |
| N2Vview-def | ⊦ N2Vview(view) = (λ ev. view(ev) = C ⊃ C ; V) | An Axiom |
| Cview | ⊦ Cview(view)(ev) ↔ view(ev) = C | A User Theorem |
| N2Vview-C | ⊦ N2Vview(view)(ev) = C ↔ view(ev) = C | A User Theorem |
| N2Vview-Cview | ⊦ Cview(N2Vview(view)) = Cview(view) | A User Theorem |
| N2Vview-Vview | ⊦ Vview(N2Vview(view))(ev) ↔ view(ev) = V ∨ view(ev) = N | A User Theorem |
| VCview | ⊦ VCview(view)(ev) ↔ view(ev) = V ∨ view(ev) = C | A User Theorem |
| Vview | ⊦ Vview(view)(ev) ↔ view(ev) = V | A User Theorem |
| enabled-empty | ⊦ enabled(trans, s, []) | A User Theorem |
| enabled-transex | ⊦ ¬ enabled(trans, s, tr) → ¬ trans∃(trans, s, tr, s0) | A User Theorem |
| lastoc-C-event | ⊦ view(ev) = C ∧ ev ∈ tr → (∃ tr0, ev0, tr1. tr = tr0 + (ev0 + tr1) ∧ view(ev0) = C ∧ proj(tr1, Cview(view)) = []) | A User Theorem |
| lastoc-C-event-01 | ⊦ proj(tr, Cview(view)) ≠ [] → (∃ tr0, ev, tr1. tr = tr0 + (ev + tr1) ∧ view(ev) = C ∧ proj(tr1, Cview(view)) = []) | A User Theorem |
| prefix-closed | ⊦ tr ∈TR trans ∧ tr0 ⊑ tr → tr0 ∈TR trans | A User Theorem |
| projection-C-empty | ⊦ proj(tr, Cview(view)) = [] ↔ (∀ ev. ev ∈ tr → view(ev) ≠ C) | A User Theorem |
| projection-N2V-unchanged | ⊦ proj(tr, Cview(view)) = [] → proj(tr, Vview(N2Vview(view))) = tr | A User Theorem |
| projection-VC-C | ⊦ proj(tr, Cview(view)) = [] → proj(tr, VCview(view)) = proj(tr, Vview(view)) | A User Theorem |
| projection-VC-C-01 | ⊦ proj(tr, Cview(view)) ≠ [] → proj(tr, VCview(view)) ≠ proj(tr0, Vview(view)) | A User Theorem |
| projection-VN-unchanged | ⊦ (∀ ev. ev ∈ tr → view(ev) = V ∨ view(ev) = N) → proj(tr, VNview(view)) = tr | A User Theorem |
| projection-VN-unchanged-01 | ⊦ proj(tr, Cview(view)) = [] → proj(tr, VNview(view)) = tr | A User Theorem |
| projection-append | ⊦ proj(tr + tr0, inevs) = proj(tr, inevs) + proj(tr0, inevs) | A User Theorem |
| projection-in | ⊦ view(ev) = C → ¬ ev ∈ proj(tr, Vview(view)) | A User Theorem |
| projection-in-01 | ⊦ view(ev) = C ∧ ev ∈ tr → ev ∈ proj(tr, VCview(view)) | A User Theorem |
| projection-last-if | ⊦ proj(tr + ev ', inevs) = ((inevs(ev) ⊃ proj(tr, inevs) + ev; proj(tr, inevs))) | A User Theorem |
| projection-one | ⊦ view(ev) = C → proj(ev ', VNview(view)) = [] | A User Theorem |
| projection-one-01 | ⊦ view(ev) = C → proj(ev ', VCview(view)) = ev ' | A User Theorem |
| projection-one-empty | ⊦ proj(ev ', Cview(view)) = [] ↔ view(ev) ≠ C | A User Theorem |
| projection-one-empty-01 | ⊦ proj(ev ', Vview(view)) = [] ↔ view(ev) ≠ V | A User Theorem |
| projection-one-empty-02 | ⊦ proj(ev ', Nview(view)) = [] ↔ view(ev) ≠ N | A User Theorem |
| projection-one-if | ⊦ proj(ev ', inevs) = ((inevs(ev) ⊃ ev '; [])) | A User Theorem |
| projection-one-keep | ⊦ inevs(ev) → proj(ev ', inevs) = ev ' | A User Theorem |
| projection-one-remove | ⊦ ¬ inevs(ev) → proj(ev ', inevs) = [] | A User Theorem |
| reachable-trans | ⊦ reachable(trans, s) ∧ trans(s, ev, s2) → (¬ reachable(trans, s2) ↔ false) | A User Theorem |
| reachable-transex | ⊦ reachable(trans, s) ∧ trans∃(trans, s, tr, s2) → (¬ reachable(trans, s2) ↔ false) | A User Theorem |
| reachable-transex-01 | ⊦ ¬ reachable(trans, s) → ¬ trans∃(trans, S0, tr, s) | A User Theorem |
| transex-append | ⊦ trans∃(trans, s, tr + tr0, s0) ↔ (∃ s1. trans∃(trans, s, tr, s1) ∧ trans∃(trans, s1, tr0, s0)) | A User Theorem |
| transex-empty-01 | ⊦ trans∃(trans, s, [], s) | A User Theorem |
| transex-enabled-intrans | ⊦ trans∃(trans, S0, tr, s0) ∧ enabled(trans, s0, tr1) → (¬ tr + tr1 ∈TR trans ↔ false) | A User Theorem |
| transex-one | ⊦ trans∃(trans, s1, ev ', s2) ↔ trans(s1, ev, s2) | A User Theorem |
| view-C-VN | ⊦ ¬ Cview(view)(ev) → VNview(view)(ev) | A User Theorem |