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: |
|---|---|---|
| sel-01 | ⊦ remove(key).key = key | An Axiom |
| inj-01 | ⊦ remove(key) = remove(key0) ↔ key = key0 | An Axiom |
| case | ⊦ mod = contains(mod.key) ∨ mod = lookup(mod.key) ∨ mod = store(mod.key, mod.adr) ∨ mod = remove(mod.key) | An Axiom |
| gen | modification freely generated by contains, lookup, store, remove; | An Axiom |
| inj-04 | ⊦ lookup(key) = lookup(key0) ↔ key = key0 | An Axiom |
| sel-05 | ⊦ lookup(key).key = key | An Axiom |
| disj-07 | ⊦ lookup(key) ≠ remove(key0) | An Axiom |
| elim-01 | ⊦ mod.lookup? → (key = mod.key ↔ mod = lookup(key)) | An Axiom |
| elim-04 | ⊦ mod.remove? → (key = mod.key ↔ mod = remove(key)) | An Axiom |
| ex-01 | ⊦ mod.lookup? ↔ (∃ key. mod = lookup(key)) | An Axiom |
| ex-04 | ⊦ mod.remove? ↔ (∃ key. mod = remove(key)) | An Axiom |
| test-01 | ⊦ lookup(key).lookup? | An Axiom |
| test-04 | ⊦ ¬ remove(key).lookup? | An Axiom |
| test-09 | ⊦ ¬ lookup(key).store? | An Axiom |
| test-12 | ⊦ ¬ remove(key).store? | An Axiom |
| test-13 | ⊦ ¬ lookup(key).remove? | An Axiom |
| test-16 | ⊦ remove(key).remove? | An Axiom |
| elim-03 | ⊦ mod.contains? → (key = mod.key ↔ mod = contains(key)) | An Axiom |
| ex-03 | ⊦ mod.contains? ↔ (∃ key. mod = contains(key)) | An Axiom |
| inj-02 | ⊦ contains(key) = contains(key0) ↔ key = key0 | An Axiom |
| test-03 | ⊦ contains(key).contains? | An Axiom |
| test-07 | ⊦ ¬ lookup(key).contains? | An Axiom |
| test-21 | ⊦ ¬ remove(key).contains? | An Axiom |
| test-22 | ⊦ ¬ contains(key).lookup? | An Axiom |
| test-24 | ⊦ ¬ contains(key).store? | An Axiom |
| test-25 | ⊦ ¬ contains(key).remove? | An Axiom |
| sel-02 | ⊦ contains(key).key = key | An Axiom |
| disj-04 | ⊦ contains(key) ≠ remove(key0) | An Axiom |
| disj-10 | ⊦ contains(key) ≠ lookup(key0) | An Axiom |
| elim-02 | ⊦ mod.store? → (key = mod.key ∧ adr = mod.adr ↔ mod = store(key, adr)) | An Axiom |
| ex-02 | ⊦ mod.store? ↔ (∃ key, adr. mod = store(key, adr)) | An Axiom |
| inj-03 | ⊦ store(key, adr) = store(key0, adr0) ↔ key = key0 ∧ adr = adr0 | An Axiom |
| test-02 | ⊦ ¬ store(key, adr).contains? | An Axiom |
| test-05 | ⊦ ¬ store(key, adr).lookup? | An Axiom |
| test-06 | ⊦ store(key, adr).store? | An Axiom |
| test-08 | ⊦ ¬ store(key, adr).remove? | An Axiom |
| sel-03 | ⊦ store(key, adr).key = key | An Axiom |
| sel-04 | ⊦ store(key, adr).adr = adr | An Axiom |
| disj-02 | ⊦ store(key, adr) ≠ remove(key0) | An Axiom |
| disj-05 | ⊦ lookup(key) ≠ store(key0, adr) | An Axiom |
| disj-08 | ⊦ contains(key) ≠ store(key0, adr) | An Axiom |