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: |
|---|---|---|
| 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 |
| empty-oplus | ⊦ ∅ ⊕ st = st | A User Theorem |
| in-dom-inter | ⊦ a ∈ st → (a ∈ dom st ∩ s ↔ a ∈ s) | A User Theorem |
| oplus-empty | ⊦ st ⊕ ∅ = st | A User Theorem |
| oplus-shift-put-l | ⊦ st0[a, d] ⊕ st1 = (st0 ⊕ st1)[a, d] | 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 |