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: |
|---|---|---|
| dls-emp | ⊦ dls(head, prev, [], rx, next, tail) = (emp ∧ ⌜head = next ∧ tail = prev ∧ rx = []⌝ ) | An Axiom |
| dls-rec | ⊦ dls(head, prev, a ' + x, rx, next, tail) = _∃(λ r. ⌜rx ≠ [] ∧ head = rx.first⌝ ∧ head => mkcell(prev, r, a) * dls(r, head, x, rx.rest, next, tail)) | An Axiom |
| dls-last | ⊦ # x = # rx → dls(head, prev, x + a ', rx + tail0 ', next, tail) = _∃(λ r. ⌜tail0 = tail⌝ ∧ tail => mkcell(r, next, a) * dls(head, prev, x, rx, tail, r)) | A User Theorem |
| dls-length | ⊦ ((dls(head, prev, x, rx, next, tail) * P))(H) → # x = # rx | A User Theorem |
| dls-one | ⊦ dls(head, prev, a ', r ', next, tail) = (⌜head = r ∧ tail = head⌝ ∧ head => mkcell(prev, next, a)) | A User Theorem |
| dls-split | # x0 = # rx0, # x1 = # rx1, x0 ≠ [], x1 ≠ [] ⊦ dls(head, prev, x0 + a ' + x1, rx0 + r ' + rx1, next, tail) = _∃(λ r0, r1. dls(head, prev, x0, rx0, r, r0) * r => mkcell(r0, r1, a) * dls(r1, r, x1, rx1, next, tail)) | A User Theorem |