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: |
|---|---|---|
| lls-rec | ⊦ lls(r, r1, a ' + x) = _∃ λ r0. r => a × r0 * lls(r0, r1, x) | An Axiom |
| lls-base | ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ ) | An Axiom |
| ll-trav1-def | ⊦ (ll-trav(r0, r1, x) * P)(H) ↔ (∃ x0, x1. x = x0 + x1 ∧ (lls(r0, r1, x0) * lls(r1, null, x1) * P)(H)) | An Axiom |
| ll-trav2-nonnull-def | ⊦ r1 ≠ null → ((ll-trav(r0, r1, r2, x) * P)(H) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ (lls(r0, r1, x0) * r1 => a × r2 * lls(r2, null, x1) * P)(H))) | An Axiom |
| ll-trav2-null-def | ⊦ (ll-trav(r0, null, r2, x) * P)(H) ↔ r2 = r0 ∧ (lls(r0, null, x) * P)(H) | An Axiom |
| ll-trav1-end | r1 ≠ null ⊦ H[r1] = a × null → (¬ ¬ (ll-trav(r0, r1, x) * P)(H) ↔ x ≠ [] ∧ (∃ y. x = y + a ∧ (lls(r0, r1, y) * r1 => a × null * P)(H))) | A User Theorem |
| ll-trav1-init | ⊦ (lls(r0, null, x) * P)(H) → (¬ (ll-trav(r0, r0, x) * P)(H) ↔ false) | A User Theorem |
| ll-trav1-next | r1 ≠ null ⊦ (ll-trav(r0, r1, x) * P)(H) ∧ H[r1] = a × r → (¬ (ll-trav(r0, r, x) * P)(H) ↔ false) | A User Theorem |
| ll-trav2-end | r2 ≠ null ⊦ H[r2] = a × null → ( ¬ ¬ (ll-trav(r0, r1, r2, x) * P)(H) ↔ x ≠ [] ∧ (r1 = null ⊃ (r0 = r2 ∧ (lls(r0, null, x) * P)(H)); (∃ y, b. x = y + (b + a) ∧ (lls(r0, r1, y) * r1 => b × r2 * r2 => a × null * P)(H)))) | A User Theorem |
| ll-trav2-init | ⊦ (lls(r0, null, x) * P)(H) → (¬ (ll-trav(r0, null, r0, x) * P)(H) ↔ false) | A User Theorem |
| ll-trav2-next | r2 ≠ null ⊦ (ll-trav(r0, r1, r2, x) * P)(H) ∧ H[r2] = a × r → (¬ (ll-trav(r0, r2, r, x) * P)(H) ↔ false) | A User Theorem |
| lls-consecutive | ⊦ (lls(r0, r1, x) * lls(r1, r2, y) * P)(H) → (¬ (lls(r0, r2, x + y) * P)(H) ↔ false) | A User Theorem |
| lls-fold-head | ⊦ (r0 => a × r1 * lls(r1, r2, x) * P)(H) ↔ (lls(r0, r2, a ' + x) * P)(H) ∧ True(H[r0] .nxt = r1) | A User Theorem |
| lls-fold-tail | x ≠ [] ⊦ (r1 => x .last × r2 * lls(r0, r1, x .butlast) * P)(H) → (¬ (lls(r0, r2, x) * P)(H) ↔ false) | A User Theorem |
| lls-null | ⊦ lls(null, r, x) = (emp ∧ ⌜r = null⌝ ∧ ⌜x = []⌝ ) | A User Theorem |
| lls-one | ⊦ lls(r0, r1, a ') = r0 => a × r1 | A User Theorem |
| lls-unfold-head | x ≠ [] ⊦ (lls(r0, r2, x) * P)(H) ↔ (∃ a, y, r1. (r0 => a × r1 * lls(r1, r2, y) * P)(H) ∧ x = a ' + y) | A User Theorem |
| lls-unfold-head-simp | r0 ≠ r2 ⊦ H[r0] = ce → (¬ ¬ (lls(r0, r2, x) * P)(H) ↔ (∃ a, y, r1. (r0 => a × r1 * lls(r1, r2, y) * P)(H) ∧ x = a ' + y)) | A User Theorem |
| lls-unfold-tail | ⊦ lls(r0, r2, x + a ') = _∃ λ r1. lls(r0, r1, x) * r1 => a × r2 | A User Theorem |