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 |
| In-store | ⊦ a × d ∈ st ↔ a ∈ st ∧ st[a] = d | 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 |
| gen-03 | elemdata freely generated by ×; | An Axiom |
| gen-04 | store generated by ∅, [ ]; | An Axiom |
| ax | ⊦ a × d = a0 × d0 ↔ a = a0 ∧ d = d0 | 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 |
| Del-at-strong | a ≠ b ⊦ (st -- b)[a] = st[a] | A User Theorem |
| Del-notin | ⊦ ¬ a ∈ st -- a | A User Theorem |
| Del-other-data | ⊦ st[a] ≠ st[b] → (a ∈ st -- b ↔ a ∈ st) | A User Theorem |
| del-exists | a ∈ st ⊦ ∃ st0. ¬ a ∈ st0 ∧ st = st0[a, st[a]] | 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 |
| empty | ⊦ # st = 0 ↔ st = ∅ | A User Theorem |
| empty-01 | ⊦ ∅ -- a = ∅ | A User Theorem |
| eq-shift-del | ⊦ ¬ a ∈ st → (st[a, d] = st0 ↔ st = st0 -- a ∧ a ∈ st0 ∧ st0[a] = d) | 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 |
| ext-rec | ⊦ st1 = st0[a, d] ↔ a ∈ st1 ∧ st1[a] = d ∧ (∀ b. a ≠ b → (b ∈ st0 ↔ b ∈ st1) ∧ (b ∈ st0 → st0[b] = st1[b])) | A User Theorem |
| in-neq | ⊦ a ≠ b → (a ∈ st[b, d] ↔ a ∈ st) | A User Theorem |
| in-pair | ⊦ a × d ∈ st ↔ ¬ ¬(a ∈ st ∧ st[a] = d) | A User Theorem |
| indef | ⊦ a ∈ st ↔ st = st[a, st[a]] | A User Theorem |
| indef-01 | ⊦ a ∈ st ↔ st = (st -- a)[a, st[a]] | A User Theorem |
| inex | ⊦ a ∈ st → (∃ d, st0. st = st0[a, d] ∧ ¬ a ∈ st0) | A User Theorem |
| inj-put | ⊦ ¬ a ∈ st ∧ ¬ a ∈ st0 → (st[a, d] = st0[a, d] ↔ st = st0) | A User Theorem |
| inj-put-01 | ⊦ a ≠ b → (st[a, d][b, d0] = st[b, d0] ↔ a ∈ st ∧ st[a] = d) | A User Theorem |
| ins | ⊦ st[a] = d ∧ a ∈ st → st[a, d] = st | A User Theorem |
| ins-same | ⊦ st[a, st[a]] = st ↔ a ∈ st | A User Theorem |
| ins-same-01 | ⊦ a ∈ st → st[a, st[a]] = st | A User Theorem |
| ins3 | ⊦ st[a, d1][b, d0][a, d] = st[b, d0][a, d] | A User Theorem |
| ins4 | ⊦ st[a, d2][b, d1][c, d0][a, d] = st[b, d1][c, 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-At-same | ⊦ a = b → st[b, d][a] = d | A User Theorem |
| k-Del-rec1 | ⊦ ¬ a ∈ st → st[a, d] -- a = st | A User Theorem |
| k-Del-rec2 | ⊦ a ≠ b ∧ ¬ a ∈ st → st[a, d] -- b = (st -- b)[a, d] | A User Theorem |
| k-Extension | ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ (a ∈ st1 → st1[a] = st2[a])) | A User Theorem |
| key-size | ∀ a. a ∈ st ↔ a ∈ st0 ⊦ # st = # st0 | A User Theorem |
| lookupisempty | ⊦ (st -- a)[a] = (∅)[a] | A User Theorem |
| neq | ⊦ st[a, d] ≠ ∅ | A User Theorem |
| notin-del-notin | ⊦ ¬ a ∈ st → st -- a = st | A User Theorem |
| notmemlookup | ⊦ ¬ a ∈ st → st[a] = (∅)[a] | A User Theorem |
| put-neq | ⊦ d ≠ d0 → st[a, d] ≠ st0[a, d0] | A User Theorem |
| put-neq-01 | ⊦ st ≠ st0 ∧ ¬ a ∈ st ∧ ¬ a ∈ st0 → st[a, d] ≠ st0[a, d] | A User Theorem |
| put-same | ⊦ a = b → st[a, d][b, d0] = st[b, d0] | A User Theorem |
| rem-eq | ⊦ st -- a ≠ st ↔ a ∈ st | A User Theorem |
| rew | ⊦ a ≠ b → st[b, d0][a, d] = st[a, d][b, d0] | A User Theorem |
| size | ⊦ a ∈ st → #(st -- a) = (# st)-1 | A User Theorem |
| size-in | ⊦ a ∈ st → # st[a, d] = # st | A User Theorem |
| size-neq | ⊦ # st[a, d] ≠ # st[a, d0] ↔ false | A User Theorem |
| size-subset | ⊦ st ⊆ st0 → # st ≤ # st0 | 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 -- a | A User Theorem |
| subset-delete-01 | ⊦ st ⊆ st0 → st -- a ⊆ st0 | A User Theorem |
| subset-delete-02 | ⊦ st ⊆ st0 → (¬ st -- a ⊆ st0 ↔ false) | 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-new | ⊦ ¬ a ∈ st → (st ⊆ st0[a, d] ↔ st ⊆ st0) | A User Theorem |
| subset-put | ⊦ st[a, d] ⊆ st0 ↔ st -- a ⊆ st0 ∧ a × d ∈ st0 | A User Theorem |
| subset-put-01 | ⊦ st ⊆ st0[a, d] ↔ st ⊆ st0 ∧ ¬ a ∈ st ∨ a × d ∈ st ∧ st -- a ⊆ st0 -- a | A User Theorem |
| subset-put-02 | ⊦ st[a, d] ⊆ st0 ↔ st -- a ⊆ st0 -- a ∧ a × d ∈ st0 | A User Theorem |
| subset-put-03 | ⊦ st[a] = d → st ⊆ st[a, d] | A User Theorem |
| subset-put-04 | ⊦ st ⊆ st[a, st[a]] | 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 |
| subset-size | ⊦ # st0 < # st → ¬ 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 |