This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| Dom | ⊦ a ∈ dom st ↔ a ∈ st | An Axiom |
| Diff-base | ⊦ st \ ∅ = st | An Axiom |
| Diff-rec | ⊦ st \ (s ++ a) = (st \ s) -- a | An Axiom |
| Data-in | ⊦ d ∈ st ↔ (∃ a. a ∈ st ∧ st[a] = d) | An Axiom |
| restrict | ⊦ st | s = st \ (dom st \ s) | An Axiom |
| oplus-l-at-right | ⊦ ¬ a ∈ st0 ∧ a ∈ st1 → (st0 ⊕ st1)[a] = st1[a] | An Axiom |
| oplus-l-at-left | ⊦ a ∈ st0 → (st0 ⊕ st1)[a] = st0[a] | An Axiom |
| oplus-l-in | ⊦ a ∈ st0 ⊕ st1 ↔ a ∈ st0 ∨ a ∈ st1 | An Axiom |
| Data-in-del | ⊦ ¬ d0 ∈ st → ¬ d0 ∈ st -- a | A User Theorem |
| Data-in-delput | ⊦ ¬ d0 ∈ st ∧ d0 ≠ d1 → ¬ d0 ∈ st[b, d1] -- a | A User Theorem |
| Data-in-delput-2 | ⊦ ¬ d0 ∈ st ∧ d0 ≠ d1 ∧ d0 ≠ d2 → ¬ d0 ∈ st[b, d1][c, d2] -- a | A User Theorem |
| Data-in-other | ⊦ ¬ a ∈ st → (d0 ∈ st[a, d1] ↔ d0 ∈ st ∨ d0 = d1) | A User Theorem |
| Data-in-putdel | ⊦ ¬ d0 ∈ st ∧ d0 ≠ d1 → ¬ d0 ∈ (st -- a)[b, d1] | A User Theorem |
| Data-in-putdelput | ⊦ ¬ d0 ∈ st ∧ d0 ≠ d1 ∧ d0 ≠ d2 → ¬ d0 ∈ (st[b, d1] -- a)[c, d2] | A User Theorem |
| Data-in-puteq | ⊦ d0 = d1 → d0 ∈ st[a, d1] | A User Theorem |
| Data-in-putsame | ⊦ d ∈ st[a, d] | A User Theorem |
| Data-notin-other | ⊦ d0 ≠ d1 ∧ ¬ d0 ∈ st → ¬ d0 ∈ st[a, d1] | A User Theorem |
| Data-notin-other-2 | ⊦ d0 ≠ d1 ∧ d0 ≠ d2 ∧ ¬ d0 ∈ st → ¬ d0 ∈ st[a, d1][b, d2] | A User Theorem |
| Data-notin-other-3 | ⊦ d ≠ d0 ∧ d0 ≠ d1 ∧ d0 ≠ d2 ∧ ¬ d0 ∈ st → ¬ d0 ∈ st[a, d1][b, d2][c, d] | A User Theorem |
| Diff-Diff-com | ⊦ (st \ s) \ s0 = (st \ s0) \ s | A User Theorem |
| Diff-del-rw | ⊦ (st -- a) \ s = (st \ s) -- a | A User Theorem |
| Diff-empty | ⊦ ∅ \ s = ∅ | A User Theorem |
| Diff-ext | ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s | A User Theorem |
| Diff-get | ⊦ ¬ a ∈ s → (st \ s)[a] = st[a] | A User Theorem |
| Diff-mems-get | ⊦ a ∈ s → (st \ s)[a] = (∅)[a] | A User Theorem |
| Diff-mod | ⊦ st[a, d] \ (s ++ a) = st \ (s ++ a) | A User Theorem |
| Diff-rec-rev | ⊦ st \ (s ++ a) = (st -- a) \ s | A User Theorem |
| In-data-in | a ∈ st ⊦ st[a] ∈ st | A User Theorem |
| diff-add-notin | ⊦ ¬ a ∈ st → st \ (s ++ a) = st \ s | A User Theorem |
| diff-add-rem | ⊦ a ∈ st → (st \ (s ++ a)) -- a = st \ (s ++ a) | A User Theorem |
| diff-get-add | ⊦ a ≠ b ∧ ¬ b ∈ s → (st \ (s ++ a))[b] = st[b] | A User Theorem |
| dom-add-in | ⊦ a ∈ st → dom st ++ a = dom st | A User Theorem |
| dom-del | ⊦ dom(st -- a) = dom st -- a | A User Theorem |
| dom-emp | ⊦ dom ∅ = ∅ | A User Theorem |
| dom-ins | ⊦ dom st[a, d] = dom st ++ a | A User Theorem |
| dom-isemp | ⊦ dom st = ∅ ↔ st = ∅ | A User Theorem |
| dom-rem | ⊦ dom(st \ s) = dom st \ s | A User Theorem |
| dom-restrict | ⊦ s ⊆ dom st → dom(st | s) = s | A User Theorem |
| dom-union-l | ⊦ dom(st0 ⊕ st1) = dom st0 ∪ dom st1 | A User Theorem |
| in-dom-inter | ⊦ a ∈ st → (a ∈ dom st ∩ s ↔ a ∈ s) | A User Theorem |
| rem-write | ⊦ ¬ a ∈ s → st[a, d] \ s = (st \ s)[a, d] | A User Theorem |
| rem-write-cases | ⊦ st[a, d] \ s = (a ∈ s ⊃ st \ s;(st \ s)[a, d]) | A User Theorem |
| rem-write-other | ⊦ a ∈ s → st[a, d] \ s = st \ s | A User Theorem |
| restrict-at | ⊦ a ∈ st ∧ a ∈ s → (st | s)[a] = st[a] | A User Theorem |
| restrict-empty | ⊦ st | ∅ = ∅ | A User Theorem |
| restrict-in | ⊦ a ∈ st | s ↔ a ∈ st ∧ a ∈ s | A User Theorem |
| restrict-intersect-empty | ⊦ dom st ∩ s = ∅ → st \ s = st | A User Theorem |
| restrict-intersect-empty-write-add | ⊦ dom st ∩ s = ∅ → st[a, d] \ (s -- a) = st[a, d] | A User Theorem |