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