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 |
| 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-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 |
| precise-ls | ⊦ precise(ls(r, x)) | A User Theorem |