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: |
|---|---|---|
| in-write | r ≠ null, r0 ∈ H ⊦ r ∈ H[r0, o] ↔ r ∈ H | An Axiom |
| in-alloc | r0 ≠ null, ¬ r0 ∈ H ⊦ r ∈ H ++ r0 ↔ ¬ ¬ (r = r0 ∨ r ∈ H) | An Axiom |
| ext | ⊦ H0 = H1 ↔ (∀ r. (r ∈ H0 ↔ r ∈ H1) ∧ (r ∈ H0 → H0[r] = H1[r])) | An Axiom |
| sanity | ⊦ ¬ null ∈ H | An Axiom |
| in-emp | ⊦ ¬ r ∈ ∅ | An Axiom |
| at-alloc | r ∈ H, r0 ≠ null, ¬ r0 ∈ H ⊦ r ≠ r0 → (H ++ r0)[r] = H[r] | An Axiom |
| at-write | r ∈ H, r0 ∈ H ⊦ (H[r0, o][r]) = ((r = r0 ⊃ o; H[r])) | An Axiom |
| in-del | ⊦ r ∈ H -- r0 ↔ ¬ ¬ (r ≠ r0 ∧ r ∈ H) | An Axiom |
| at-del | r ∈ H ⊦ r ≠ r0 → (H -- r0)[r] = H[r] | An Axiom |
| gen | An Axiom | |
| diff-write | r ∈ H1 ⊦ H0 \ H1[r, o] = H0 \ H1 | An Axiom |
| diff-alloc | r ≠ null, ¬ r ∈ H1 ⊦ H0 \ (H1 ++ r) = (H0 -- r) \ H1 | An Axiom |
| diff-emp | ⊦ H0 \ ∅ = H0 | An Axiom |
| uni-write | r ≠ null, r ∈ H1, H0 ⊥ H1 ⊦ H0 ∪ H1[r, o] = (H0 ∪ H1)[r, o] | An Axiom |
| uni-alloc | r ≠ null, ¬ r ∈ H1, ¬ r ∈ H0, H0 ⊥ H1 ⊦ H0 ∪ (H1 ++ r) = (H0 ∪ H1) ++ r | An Axiom |
| uni-emp | ⊦ H0 ∪ ∅ = H0 | An Axiom |
| size-write | r ∈ H ⊦ # (H[r, o]) = # H | An Axiom |
| size-alloc | ¬ r ∈ H, r ≠ null ⊦ # (H ++ r) = # H + 1 | An Axiom |
| size-emp | ⊦ # ∅ = 0 | An Axiom |
| disj | ⊦ H0 ⊥ H1 ↔ (∀ r. ¬ r ∈ H0 ∨ ¬ r ∈ H1) | An Axiom |
| diffs-ins | ⊦ H0 \ (rs ++ r) = (H0 -- r) \ rs | An Axiom |
| diffs-emp | ⊦ H0 \ ∅ = H0 | An Axiom |
| subset | ⊦ H0 ⊆ H1 ↔ (∀ r. (r ∈ H0 → r ∈ H1) ∧ (r ∈ H0 → H0[r] = H1[r])) | An Axiom |
| alloc-write | r ≠ null, ¬ r ∈ H, r0 ∈ H ⊦ ((H ++ r)[r0, o0][r, o]) = (H[r0, o0] ++ r)[r, o] | A User Theorem |
| at-diffs | ⊦ r ∈ H ∧ ¬ r ∈ rs → (H \ rs)[r] = H[r] | A User Theorem |
| at-uni | r ∈ H0 ∪ H1 ⊦ H0 ⊥ H1 → (H0 ∪ H1)[r] = ((r ∈ H0 ⊃ H0[r]; H1[r])) | A User Theorem |
| del-new | ¬ r ∈ H, r ≠ null ⊦ (H ++ r) -- r = H | A User Theorem |
| del-notin | ⊦ ¬ r ∈ H → H -- r = H | A User Theorem |
| del-sw | ⊦ H -- r -- r0 = H -- r0 -- r | A User Theorem |
| del-twice | ⊦ H -- r -- r = H -- r | A User Theorem |
| del-uni | ⊦ H0 ⊥ H1 → (H0 ∪ H1) -- r = (H0 -- r) ∪ (H1 -- r) | A User Theorem |
| delswr | r ∈ H ⊦ r ∈ rs → H[r, o] \ rs = H \ rs | A User Theorem |
| diff-at | r ∈ H0, ¬ r ∈ H1 ⊦ (H0 \ H1)[r] = H0[r] | A User Theorem |
| diff-in | ⊦ r ∈ H0 \ H1 ↔ ¬ ¬ (r ∈ H0 ∧ ¬ r ∈ H1) | A User Theorem |
| diffs-sw | ⊦ (H -- r) \ rs = (H \ rs) -- r | A User Theorem |
| diffs-twice | ⊦ (H \ rs) \ rs = H \ rs | A User Theorem |
| disj-alloc | r0 ≠ null, ¬ r0 ∈ H0, ¬ r0 ∈ H1 ⊦ H0 ⊥ H1 → H0 ⊥ H1 ++ r0 | A User Theorem |
| disj-com | ⊦ H0 ⊥ H1 ↔ H1 ⊥ H0 | A User Theorem |
| disj-com-rw | ⊦ H0 ⊥ H1 → (¬ H1 ⊥ H0 ↔ false) | A User Theorem |
| disj-diff | ⊦ ¬ H ⊥ H0 \ H ↔ false | A User Theorem |
| disj-distr-uni | ⊦ H1 ⊥ H → (H0 ⊥ H1 ∪ H ↔ H0 ⊥ H1 ∧ H0 ⊥ H) | A User Theorem |
| disj-distr-uni-com | ⊦ H1 ⊥ H2 → (H1 ∪ H2 ⊥ H0 ↔ H0 ⊥ H1 ∧ H0 ⊥ H2) | A User Theorem |
| disj-emp-l | ⊦ ∅ ⊥ H | A User Theorem |
| disj-emp-r | ⊦ H ⊥ ∅ | A User Theorem |
| disj-l | ⊦ r ∈ H0 ∧ H0 ⊥ H1 → (r ∈ H1 ↔ false) | A User Theorem |
| disj-r | ⊦ r ∈ H1 ∧ H0 ⊥ H1 → (r ∈ H0 ↔ false) | A User Theorem |
| disj-swap | ⊦ H0 ⊥ H1 → H1 ⊥ H0 | A User Theorem |
| disj-write | r ≠ null, ¬ r ∈ H1 ⊦ H0 ⊥ (H1 ++ r)[r, o] ↔ H0 ⊥ H1 ∧ ¬ r ∈ H0 | A User Theorem |
| emp-subset | ⊦ ∅ ⊆ H | A User Theorem |
| exin | ⊦ r ≠ null → (r ∈ H ↔ (∃ H0, o. H = (H0 ++ r)[r, o] ∧ ¬ r ∈ H0)) | A User Theorem |
| exin-uni | ⊦ r ≠ null → (r ∈ H ↔ (∃ H0, o. H = H0 ∪ (∅ ++ r)[r, o] ∧ ¬ r ∈ H0)) | A User Theorem |
| in-diffs | ⊦ r ∈ H \ rs ↔ ¬ ¬ (r ∈ H ∧ ¬ r ∈ rs) | A User Theorem |
| in-uni | ⊦ H0 ⊥ H1 → (r ∈ H0 ∪ H1 ↔ ¬ ¬ (r ∈ H0 ∨ r ∈ H1)) | A User Theorem |
| in-write-strong | r0 ∈ H ⊦ r ∈ H[r0, o] ↔ r ∈ H | A User Theorem |
| nonnull | ⊦ r ∈ H → r ≠ null | A User Theorem |
| overwrite | r ∈ H ⊦ (H[r, o0][r, o1]) = H[r, o1] | A User Theorem |
| size-uni | ⊦ H0 ⊥ H1 → # (H0 ∪ H1) = # H0 + # H1 | A User Theorem |
| subset-at | ⊦ H0 ⊆ H1 ∧ r ∈ H0 → H1[r] = H0[r] | A User Theorem |
| subset-emp | ⊦ H ⊆ ∅ ↔ H = ∅ | A User Theorem |
| subset-in | ⊦ H0 ⊆ H1 ∧ r ∈ H0 → (¬ r ∈ H1 ↔ false) | A User Theorem |
| subset-uni | ⊦ H0 ⊆ H1 ↔ (∃ H. H0 ∪ H = H1 ∧ H ⊥ H0) | A User Theorem |
| sw-alloc-put | ¬ r0 ∈ H, r0 ≠ null, r1 ∈ H ⊦ r0 ≠ r1 → ((H ++ r0)[r0, o0][r1, o1]) = (H[r1, o1] ++ r0)[r0, o0] | A User Theorem |
| sw-del-add | r ≠ null ∧ ¬ r ∈ H ⊦ r0 ≠ r → ((H -- r0) ++ r)[r, o] = (H ++ r)[r, o] -- r0 | A User Theorem |
| sw-del-add-01 | r ≠ null ∧ ¬ r ∈ H ⊦ r0 ∈ H1 ∧ ¬ r ∈ H1 → ((H -- r0) ++ r)[r, o] = (H ++ r)[r, o] -- r0 | A User Theorem |
| sw-del-add-new | ¬ r ∈ H, r ≠ null ⊦ ¬ r ∈ rs → (H ++ r)[r, o] \ rs = ((H \ rs) ++ r)[r, o] | A User Theorem |
| sw-delswr | r ∈ H ⊦ ¬ r ∈ rs → H[r, o] \ rs = (H \ rs)[r, o] | A User Theorem |
| sw-delwr | r ∈ H ⊦ r ≠ r0 → H[r, o] -- r0 = (H -- r0)[r, o] | A User Theorem |
| sw-put | r0 ∈ H, r1 ∈ H ⊦ r0 ≠ r1 → (H[r0, o0][r1, o1]) = (H[r1, o1][r0, o0]) | A User Theorem |
| uni-ass | ⊦ H0 ⊥ H1 ∧ H1 ⊥ H ∧ H ⊥ H0 → (H0 ∪ H1) ∪ H = H0 ∪ H1 ∪ H | A User Theorem |
| uni-com | ⊦ H0 ⊥ H1 → H1 ∪ H0 = H0 ∪ H1 | A User Theorem |
| uni-emp-l | ⊦ ∅ ∪ H = H | A User Theorem |
| uni-emp-r | ⊦ H ∪ ∅ = H | A User Theorem |
| uni-inj | ⊦ H ⊥ H0 ∧ H ⊥ H1 → (H ∪ H0 = H ∪ H1 ↔ H0 = H1) | A User Theorem |
| write-again | r ∈ H ⊦ H[r] = o → H[r, o] = H | A User Theorem |
| write-del | r ∈ H ⊦ H[r, o] -- r = H -- r | A User Theorem |
| write-left | ⊦ r ∈ H0 ∧ H0 ⊥ H1 → (H0 ∪ H1)[r, o] = H0[r, o] ∪ H1 | A User Theorem |
| write-right | ⊦ r ∈ H1 ∧ H0 ⊥ H1 → (H0 ∪ H1)[r, o] = H0 ∪ H1[r, o] | A User Theorem |
| write-twice | r ∈ H ⊦ (H[r, o][r, o]) = H[r, o] | A User Theorem |