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: |
|---|---|---|
| Extension | ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a]) | An Axiom |
| In-empty | ⊦ ¬ a ∈ ∅ | An Axiom |
| In-insert | ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st | An Axiom |
| At-same | ⊦ st[a, d][a] = d | An Axiom |
| At-other | ⊦ a ≠ b → st[b, d][a] = st[a] | An Axiom |
| Subset | ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1[a] = st2[a]) | An Axiom |
| Size-empty | ⊦ # ∅ = 0 | An Axiom |
| Size-insert | ⊦ ¬ a ∈ st → # st[a, d] = # st + 1 | An Axiom |
| Del-in | ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st | An Axiom |
| Del-at | ⊦ a ≠ b → (st -- b)[a] = st[a] | An Axiom |
| Dom | ⊦ a ∈ dom st ↔ a ∈ st | An Axiom |
| Data-in | ⊦ d ∈ st ↔ (∃ a. a ∈ st ∧ st[a] = d) | An Axiom |
| Ran | ⊦ d ∈ ran st ↔ d ∈ st | An Axiom |
| At-in-out | ⊦ b ∈ st ∧ ¬ a ∈ st → st[a, d][b] = st[b] | A User Theorem |
| At-other-num | a ≠ b ⊦ st[(* b), d][(* a)] = st[a] | A User Theorem |
| At-other-strong | a ≠ b ⊦ st[a, d][b] = st[b] | A User Theorem |
| 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-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 |
| In-data-in | a ∈ st ⊦ st[a] ∈ st | A User Theorem |
| del-empty | ⊦ ∅ -- a = ∅ | A User Theorem |
| del-exists | a ∈ st ⊦ ∃ st0. ¬ a ∈ st0 ∧ st = st0[a, st[a]] | A User Theorem |
| del-notin | ⊦ ¬ a ∈ st → st -- a = st | A User Theorem |
| del-put | ⊦ (st -- a)[a, d] = st[a, d] | A User Theorem |
| del-putsame | ⊦ a ∈ st → (st -- a)[a, st[a]] = st | A User Theorem |
| deldel | ⊦ st -- a -- a = st -- a | A User Theorem |
| delete-put-rew | ⊦ a ≠ b → (st -- b)[a, d] = st[a, d] -- b | 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 |
| empty | ⊦ # st = 0 ↔ st = ∅ | A User Theorem |
| eq-shift-put | ⊦ a ∈ st → (st[a, d] = st0 ↔ st = st0[a, st[a]] ∧ a ∈ st0 ∧ st0[a] = d) | A User Theorem |
| exin | ⊦ a ∈ st ↔ (∃ d, st0. st = st0[a, d] ∧ ¬ a ∈ st0) | A User Theorem |
| exnotempty | ⊦ st = ∅ ↔ ¬(∃ a, d, st0. st = st0[a, d] ∧ ¬ a ∈ st0) | A User Theorem |
| exputin | ⊦ ∃ st0. st0[a, d] = st[a, d] ∧ ¬ a ∈ st0 | A User Theorem |
| in-neq | ⊦ a ≠ b → (a ∈ st[b, d] ↔ a ∈ st) | A User Theorem |
| in-notemp | ⊦ a ∈ st → st ≠ ∅ | A User Theorem |
| indef | ⊦ a ∈ st ↔ st = (st -- a)[a, st[a]] | A User Theorem |
| indef-01 | ⊦ a ∈ st ↔ st = st[a, st[a]] | A User Theorem |
| inex | ⊦ a ∈ st → (∃ d, st0. st = st0[a, d] ∧ ¬ a ∈ st0) | A User Theorem |
| inj-put | ⊦ a ≠ b → (st[a, d][b, d0] = st[b, d0] ↔ a ∈ st ∧ st[a] = d) | A User Theorem |
| inj-put-01 | ⊦ ¬ a ∈ st ∧ ¬ a ∈ st0 → (st[a, d] = st0[a, d] ↔ st = st0) | A User Theorem |
| ins | ⊦ st[a] = d ∧ a ∈ st → st[a, d] = st | A User Theorem |
| ins-same | ⊦ a ∈ st → st[a, st[a]] = st | A User Theorem |
| ins-same-01 | ⊦ st[a, st[a]] = st ↔ a ∈ st | A User Theorem |
| ins3 | ⊦ st[a, d1][b, d0][a, d] = st[b, d0][a, d] | A User Theorem |
| insert | ⊦ st[a, d] -- a = st -- a | A User Theorem |
| insin | ⊦ a ∈ st[a, d] | A User Theorem |
| insins | ⊦ st[a, d0][a, d] = st[a, d] | A User Theorem |
| k-Extension | ⊦ st0 ≠ st1 ↔ ¬(∀ a. (a ∈ st0 ↔ a ∈ st1) ∧ (a ∈ st0 → st0[a] = st1[a])) | A User Theorem |
| lookupisempty | ⊦ (st -- a)[a] = (∅)[a] | A User Theorem |
| neq | ⊦ st[a, d] ≠ ∅ | A User Theorem |
| notin-emp | ⊦ st = ∅ → ¬ a ∈ st | A User Theorem |
| notmemlookup | ⊦ ¬ a ∈ st → st[a] = (∅)[a] | A User Theorem |
| put-neq | ⊦ st ≠ st0 ∧ ¬ a ∈ st ∧ ¬ a ∈ st0 → st[a, d] ≠ st0[a, d] | A User Theorem |
| put-neq-01 | ⊦ d ≠ d0 → st[a, d] ≠ st0[a, d0] | A User Theorem |
| put-same | ⊦ a = b → st[a, d][b, d0] = st[b, d0] | A User Theorem |
| rew | ⊦ a ≠ b → st[b, d0][a, d] = st[a, d][b, d0] | A User Theorem |
| sub-ref | ⊦ st ⊆ st | A User Theorem |
| sub-trans | ⊦ st ⊆ st0 ∧ st0 ⊆ st1 → st ⊆ st1 | A User Theorem |
| subset-delete | ⊦ st ⊆ st0 → (¬ st -- a ⊆ st0 ↔ false) | A User Theorem |
| subset-delete-01 | ⊦ st ⊆ st0 → st -- a ⊆ st0 | A User Theorem |
| subset-delete-02 | ⊦ st ⊆ st0 → st -- a ⊆ st0 -- a | A User Theorem |
| subset-elem-eq | ⊦ b ∈ st ∧ st ⊆ st1 → st[b] = st1[b] | A User Theorem |
| subset-elem-eq-01 | ⊦ b ∈ st ∧ st[b] ≠ st1[b] → ¬ st ⊆ st1 | A User Theorem |
| subset-elem-eq-02 | ⊦ b ∈ st ∧ st ⊆ st1 → (st[b] ≠ st1[b] ↔ false) | A User Theorem |
| subset-empty | ⊦ ∅ ⊆ st | A User Theorem |
| subset-empty-01 | ⊦ st ⊆ ∅ ↔ st = ∅ | A User Theorem |
| subset-put | ⊦ st ⊆ st[a, st[a]] | A User Theorem |
| subset-put-01 | ⊦ st[a] = d → st ⊆ st[a, d] | A User Theorem |
| subset-put-strong | ⊦ st ⊆ st0 → st[a, d] ⊆ st0[a, d] | A User Theorem |
| subset-put-strong-01 | ⊦ st ⊆ st0 → st[a, d][a0, d0] ⊆ st0[a, d][a0, d0] | A User Theorem |
| subset-put-strong-02 | ⊦ st ⊆ st0 → st[a, d][a0, d0][a1, d1] ⊆ st0[a, d][a0, d0][a1, d1] | A User Theorem |
| subset-put-strong-03 | ⊦ ¬ st[a, d] ⊆ st0[a, d] → ¬ st ⊆ st0 | A User Theorem |
| subset-put-strong-04 | ⊦ ¬ st[a, d][a0, d0] ⊆ st0[a, d][a0, d0] → ¬ st ⊆ st0 | A User Theorem |
| subset-put-strong-05 | ⊦ ¬ st[a, d][a0, d0][a1, d1] ⊆ st0[a, d][a0, d0][a1, d1] → ¬ st ⊆ st0 | A User Theorem |
| superset-elem-eq | ⊦ b ∈ st ∧ st ⊆ st1 → st1[b] = st[b] | A User Theorem |
| superset-elem-in | ⊦ b ∈ st ∧ st ⊆ st0 → b ∈ st0 | A User Theorem |
| superset-elem-in-01 | ⊦ b ∈ st ∧ ¬ b ∈ st0 → ¬ st ⊆ st0 | A User Theorem |
| sw | ⊦ a ≠ b → st[b, d] -- a = (st -- a)[b, d] | A User Theorem |
| sw-01 | ⊦ st -- a -- b = st -- b -- a | A User Theorem |