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: |
|---|---|---|
| insert | An Axiom | |
| remove | An Axiom | |
| insert-contract | # x0 = # rx0, x0 ≠ [], x1 ≠ [], ((r => mkcell(rx0.last, rx1.first, a) * dls(head, prev, x0 + x1, rx0 + rx1, next, tail) * P))(H) ⊦ ⟪insert(r; H)⟫ ((dls(head, prev, x0 + a ' + x1, rx0 + r ' + rx1, next, tail) * P))(H) | A User Theorem |
| insert-simple-contract | # x0 = # rx0, x0 ≠ [], x1 ≠ [], ((r => mkcell(rx0.last, r0, a) * dls(head, prev, x0 + x1, rx0 + r0 ' + rx1, next, tail) * P))(H) ⊦ ⟪insert(r; H)⟫ ((dls(head, prev, x0 + a ' + x1, rx0 + r ' + r0 ' + rx1, next, tail) * P))(H) | A User Theorem |
| remove-contract | # x0 = # rx0, x0 ≠ [], x1 ≠ [], ((dls(head, prev, x0 + a ' + x1, rx0 + r ' + rx1, next, tail) * P))(H) ⊦ ⟪remove(r; H)⟫ ((r => mkcell(rx0.last, rx1.first, a) * dls(head, prev, x0 + x1, rx0 + rx1, next, tail) * P))(H) | A User Theorem |
| remove-insert-inverse | r ∈ rx, r ≠ head, r ≠ tail, ((dls(head, prev, x, rx, next, tail) * P))(H) ⊦ ⟪remove(r; H); insert(r; H)⟫ ((dls(head, prev, x, rx, next, tail) * P))(H) | A User Theorem |
| remove-insert-inverse-twice | r0 ≠ r1, r0 ∈ rx, r0 ≠ head, r0 ≠ tail, r1 ∈ rx, r1 ≠ head, r1 ≠ tail, ((dls(head, prev, x, rx, next, tail) * P))(H) ⊦ ⟪remove(r0; H); remove(r1; H); insert(r1; H); insert(r0; H)⟫ ((dls(head, prev, x, rx, next, tail) * P))(H) | A User Theorem |
| remove-simple-contract | r ∈ rx, r ≠ head, r ≠ tail, ((dls(head, prev, x, rx, next, tail) * P))(H) ⊦ ⟪remove(r; H)⟫ ∃ x0, rx0, x1, rx1, a. x0 ≠ [] ∧ x1 ≠ [] ∧ # x0 = # rx0 ∧ x = x0 + a ' + x1 ∧ rx = rx0 + r ' + rx1 ∧ ((r => mkcell(rx0.last, rx1.first, a) * dls(head, prev, x0 + x1, rx0 + rx1, next, tail) * P))(H) | A User Theorem |