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: |
|---|---|---|
| ls-base | ⊦ ls(r, []) = (emp ∧ ⌜r = null⌝ ) | An Axiom |
| ls-rec | ⊦ ls(r, a ' + x) = _∃ λ r0. r => a × r0 * ls(r0, x) | An Axiom |
| lst-def | ⊦ lst(r) = ((r = null ⊃ ls(r, []); _∃ λ x. ls(r, x))) | An Axiom |
| ex-lst | ⊦ (_∃ xv)(mk(rs, cf)) ↔ (∃ x. xv(x)(mk(rs, cf))) | An Axiom |
| ex-lst-shift | ⊦ (o[_∃ xv] * R)[rs, cf, af] ↔ (∃ x. (o[xv(x)] * R)[rs, cf, af]) | A User Theorem |
| ls-fold1 | ⊦ (r => a × r0 * ls(r0, x) * P)(H) → (¬ (ls(r, a ' + x) * P)(H) ↔ false) | A User Theorem |
| ls-null | ⊦ ls(null, x) = (emp ∧ ⌜x = []⌝ ) | A User Theorem |
| ls-one | ⊦ ls(r, a ') = r => a × null | A User Theorem |
| ls-push | ⊦ (o[ls(r, x)] * true)[rs, cf, af(r ; o)] ∧ (o0[r => a × r0] * true)[rs, cf, af] ∧ o ≠ o0 ∧ (o[ls(r0, x0)] * true)[rs, cf, af] → (x ≠ a ' + x0 ↔ false) | A User Theorem |
| ls-unfold1 | r ≠ null ⊦ H[r] = ce → (¬ ¬ (ls(r, x) * P)(H) ↔ (∃ a, y, r0. (r => a × r0 * ls(r0, y) * P)(H) ∧ x = a ' + y)) | A User Theorem |
| ls-unfold2 | ⊦ ¬ ¬ (ls(r, a ' + x) * P)(H) ↔ (∃ r0. (r => a × r0 * ls(r0, x) * P)(H)) | A User Theorem |
| ls-unique | ⊦ (o[ls(r, x)] * R)[rs, cf, af] ∧ (o[ls(r, x0)] * R)[rs, cf, af] → (x ≠ x0 ↔ false) | A User Theorem |
| ls-unique-strng | ⊦ (o[ls(r, x)] * R)[rs, cf, af] ∧ (o[ls(r, x0)] * R0)[rs, cf, af] → (x ≠ x0 ↔ false) | A User Theorem |
| lst-in-hp | ⊦ (o[lst(r)] * R)[rs, cf, af] ∧ r ≠ null → (¬ r ∈ rs ↔ false) | A User Theorem |
| lst-null | ⊦ o[lst(null)][∅, cf, af] | A User Theorem |
| lst-rec | ⊦ r ≠ null → lst(r) = _∃ λ x. ls(r, x) | A User Theorem |
| owner-ls1 | ⊦ af(r) ≠ o ∧ r ≠ null → ((o[ls(r, x)] * R)[rs, cf, af] ↔ false) | A User Theorem |
| owner-lst1 | ⊦ af(r) ≠ o ∧ r ≠ null → ((o[lst(r)] * R)[rs, cf, af] ↔ false) | A User Theorem |
| precise-ls | ⊦ precise(ls(r, x)) | A User Theorem |