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: |
|---|---|---|
| Uniform-store | Pstore(∅), ∀ st, a, d. Pstore(st) → Pstore(insert(a, d, st)) ⊦ ∀ st. Pstore(st) | A Proof Obligation |
| Extension | ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ lookup(a, st1) = lookup(a, st2)) | A Proof Obligation |
| In-insert | ⊦ a ∈ insert(b, d, st) ↔ a = b ∨ a ∈ st | A Proof Obligation |
| At-same | ⊦ lookup(a, insert(a, d, st)) = d | A Proof Obligation |
| At-other | ⊦ a ≠ b → lookup(a, insert(b, d, st)) = lookup(a, st) | A Proof Obligation |
| In-store | ⊦ a × d ∈ st ↔ a ∈ st ∧ lookup(a, st) = d | A Proof Obligation |
| Subset | ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ lookup(a, st1) = lookup(a, st2)) | A Proof Obligation |
| Size-insert | ⊦ ¬ a ∈ st → # insert(a, d, st) = # st + 1 | A Proof Obligation |
| Del-at | ⊦ a ≠ b → lookup(a, st -- b) = lookup(a, st) | A Proof Obligation |