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: |
|---|---|---|
| In | ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z)) | An Axiom |
| Nil | ⊦ [] + x = x | An Axiom |
| Cons | ⊦ (a + x) + y = a + (x + y) | An Axiom |
| One | ⊦ a ' = a + [] | An Axiom |
| Last | ⊦ x + a = x + a ' | An Axiom |
| Two | ⊦ a + b = a ' + b ' | An Axiom |
| Noassoc | ⊦ (a ' + x) + y = a ' + x + y | A User Theorem |
| a | ⊦ (x + y) + z = x + y + z | A User Theorem |
| app | ⊦ x + [] = x | A User Theorem |
| app-01 | ⊦ x + y = x + z ↔ y = z | A User Theorem |
| app-02 | ⊦ x + y = [] ↔ x = [] ∧ y = [] | A User Theorem |
| app-02-ant | ⊦ ¬ x + y ≠ [] ↔ x = [] ∧ y = [] | A User Theorem |
| app-03 | ⊦ x + y = z + y ↔ x = z | A User Theorem |
| app-04 | ⊦ x = x + y ↔ y = [] | A User Theorem |
| app-05 | ⊦ x = y + x ↔ y = [] | A User Theorem |
| app-06 | ⊦ x + a ' = y + b ' ↔ x = y ∧ a = b | A User Theorem |
| app-07 | ⊦ a ' + x = b ' + x ↔ a = b | A User Theorem |
| app-08 | ⊦ a ' + x = a ' + y ↔ x = y | A User Theorem |
| app-09 | ⊦ y ≠ a + (x + y) | A User Theorem |
| append-size-less | ⊦ # x < # x1 → (x + x0 = x1 + x2 ↔ (∃ y. x1 = x + y ∧ x0 = y + x2)) | A User Theorem |
| c | ⊦ a + x = a ' + x | A User Theorem |
| c-01 | ⊦ x + (a + y) = x + a ' + y | A User Theorem |
| c-02 | ⊦ y ≠ [] → (a ' + x = y + z ↔ a = y.first ∧ x = y.rest + z) | A User Theorem |
| c-03 | ⊦ a ' = b ' + x ↔ a = b ∧ x = [] | A User Theorem |
| c-04 | ⊦ a ' = b ' ↔ a = b | A User Theorem |
| c-05 | ⊦ a ' = x + b ' ↔ a = b ∧ x = [] | A User Theorem |
| c-06 | ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y | A User Theorem |
| c-07 | ⊦ (a ' + x).rest = x | A User Theorem |
| c-08 | ⊦ (a ' + x).first = a | A User Theorem |
| c-09 | ⊦ x = [] ∨ x = x.first ' + x.rest | A User Theorem |
| constrrew | ⊦ a + [] = a ' | A User Theorem |
| e | ⊦ a ' ≠ [] | A User Theorem |
| e-01 | ⊦ a ' + x ≠ [] | A User Theorem |
| e-02 | ⊦ x + a ' ≠ [] | A User Theorem |
| e-03 | ⊦ x + a ' + y ≠ [] | A User Theorem |
| e-04 | ⊦ x = z0 + y + z ∧ # x = # y → z0 = [] ∧ z = [] | A User Theorem |
| elim-first | ⊦ x = [] ↔ ¬(∃ a, y. x = a ' + y) | A User Theorem |
| eq | ⊦ c ' + z = x0 + a ' ∧ x + c ' + z = b ' + y0 + a0 ' → a = a0 | A User Theorem |
| eq-01 | ⊦ x + a ' + y = b ' + z ∧ x + a ' + y0 = b0 ' + z0 → b = b0 | A User Theorem |
| eq-02 | ⊦ c ' + z = x0 + a ' ∧ x + b0 ' + c ' + z = b ' + y0 + a0 ' → a = a0 | A User Theorem |
| eq-03 | ⊦ x = y + a ' ∧ x = z + b ' → a = b ∧ y = z | A User Theorem |
| eq-04 | ⊦ x + a ' + y = b ' ↔ x = [] ∧ a = b ∧ y = [] | A User Theorem |
| eq-05 | ⊦ x = a ' + y ∧ x = b ' + z → a = b ∧ y = z | A User Theorem |
| first | ⊦ a '.first = a | A User Theorem |
| first-01 | ⊦ x ≠ [] → (x + y).first = x.first | A User Theorem |
| first-02 | ⊦ (x + a ' + y).first = (x + a ').first | A User Theorem |
| first-app | ⊦ a ∈ x → (x + y).first = x.first | A User Theorem |
| firsteq | y ≠ [] ⊦ a ' + x = y + z ↔ a = y.first ∧ x = y.rest + z | A User Theorem |
| firsteq-01 | y ≠ [] ⊦ y + z = a ' + x ↔ a = y.first ∧ x = y.rest + z | A User Theorem |
| firstoc | ⊦ a ∈ x → (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ y) | A User Theorem |
| firstoc-rew | ⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ y) | A User Theorem |
| firstrest | ⊦ (x + a ').first ' + (x + a ').rest = x + a ' | A User Theorem |
| fr | ⊦ x ≠ [] → x.first ' + x.rest = x | A User Theorem |
| if-in | ⊦ a ∈ b ' + x ↔ (a = b ⊃ true;a ∈ x) | A User Theorem |
| in | ⊦ a ∈ a ' + x | A User Theorem |
| in-01 | ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x) | A User Theorem |
| in-06 | ⊦ ¬ a ∈ b ' + x ↔ a ≠ b ∧ ¬ a ∈ x | A User Theorem |
| in-07 | ⊦ ¬ a ∈ x ∧ x ≠ [] → ¬ a ∈ x.rest | A User Theorem |
| in-08 | ⊦ x.first ∈ x ↔ x ≠ [] | A User Theorem |
| in-09 | ⊦ ¬ a ∈ x.rest → (a ∈ x ↔ a = x.first ∧ x ≠ []) | A User Theorem |
| in-10 | ⊦ ¬ a ∈ x → (a ∈ b ' + x ↔ a = b) | A User Theorem |
| in-11 | ⊦ a ∈ x → a ∈ x + y | A User Theorem |
| in-12 | ⊦ a ∈ y → a ∈ x + y | A User Theorem |
| in-13 | ⊦ x = y + a ' + z → a ∈ x | A User Theorem |
| in-14 | ⊦ a ' + x = y → a ∈ y | A User Theorem |
| in-15 | ⊦ x + a ' = y → a ∈ y | A User Theorem |
| in-16 | ⊦ x + a ' = y + b ' + z ∧ a ≠ b → a ∈ z | A User Theorem |
| in-17 | ⊦ a ∈ b ' ↔ a = b | A User Theorem |
| in-append | ⊦ a ∈ x + y ↔ ¬ ¬(a ∈ x ∨ a ∈ y) | A User Theorem |
| in-append0-not-left | ⊦ a ' + x = x0 + x1 → (¬ a ∈ x0 ↔ x0 = []) | A User Theorem |
| in-empty | ⊦ ¬ a ∈ [] | A User Theorem |
| in-last-rest | ⊦ x ≠ [] → (a ∈ (x + b ').rest ↔ a = b ∨ a ∈ x.rest) | A User Theorem |
| in-rec | ⊦ a ∈ b ' + x ↔ ¬ ¬(a = b ∨ a ∈ x) | A User Theorem |
| inapp | ⊦ ¬ a ∈ x ∧ ¬ a ∈ y → (x + a ' + y = z + a ' + y0 ↔ y = y0 ∧ x = z) | A User Theorem |
| inapp-01 | ⊦ ¬ a ∈ x ∧ ¬ a ∈ z → (x + a ' + y = z + a ' + y0 ↔ y = y0 ∧ x = z) | A User Theorem |
| inapp-02 | ⊦ ¬ a ∈ y → (y + c ' + z = a ' + z0 ↔ y = [] ∧ c = a ∧ z = z0) | A User Theorem |
| inapp-03 | ⊦ ¬ a ∈ y ∧ ¬ b ∈ x → (x + a ' + z = y + b ' + y0 ↔ a = b ∧ x = y ∧ z = y0) | A User Theorem |
| inapp-04 | ⊦ ¬ a ∈ x → (a ' + x = y + a ' + z ↔ y = [] ∧ z = x) | A User Theorem |
| inapp-05 | ⊦ a ≠ b ∧ ¬ b ∈ x ∧ ¬ b ∈ x0 → (a ' + x + b ' + y = x0 + b ' + y0 ↔ a ' + x = x0 ∧ y = y0) | A User Theorem |
| inapp-06 | ⊦ ¬ b ∈ y ∧ ¬ a ∈ z → (x + a ' + y = x0 + b ' + z ↔ x = x0 ∧ a = b ∧ y = z) | A User Theorem |
| inapp-07 | ⊦ a ' + x = y + b ' ∧ x ≠ [] → a ∈ y ∧ b ∈ x | A User Theorem |
| inapp-08 | ⊦ a ' + x = y + b ' ∧ y ≠ [] → a ∈ y ∧ b ∈ x | A User Theorem |
| inapp-09 | ⊦ x + y = z + a ' ∧ c ' + x = x0 + b ' ∧ x0 ≠ [] ∧ a ≠ b → b ∈ z | A User Theorem |
| inapp-10 | ⊦ a ' + x = y + b ' ∧ a ≠ b → a ∈ y ∧ b ∈ x | A User Theorem |
| inapp-11 | ⊦ x + y = z + a ' ∧ b ∈ x ∧ a ≠ b → b ∈ z | A User Theorem |
| inapp-12 | ⊦ x + y = z + a ' ∧ b ∈ x ∧ y ≠ [] → b ∈ z | A User Theorem |
| inapp-13 | ⊦ a ' + x = y + b ' ∧ c ∈ x ∧ c ≠ b → c ∈ y | A User Theorem |
| inapp-14 | ⊦ ¬ a ∈ x → (x + a ' = y + a ' + z ↔ y = x ∧ z = []) | A User Theorem |
| inex | ⊦ x + a ' = y + b ' + z ∧ a ≠ b → (∃ z0. z = z0 + a ') | A User Theorem |
| inex-01 | ⊦ a ' + x = y + b ' + z ∧ a ≠ b → (∃ y0. y = a ' + y0) | A User Theorem |
| inex-02 | ⊦ a ' + x = y → (∃ y0. y = a ' + y0) | A User Theorem |
| inex-03 | ⊦ x + a ' = y → (∃ y0. y = y0 + a ') | A User Theorem |
| ins | ⊦ x + a ' = y → x + a ' + z = y + z | A User Theorem |
| ins-01 | ⊦ a ' + x = z → a ' + x + y = z + y | A User Theorem |
| isin | ⊦ a ' + x = y + b ' + z ∧ y ≠ [] → b ∈ x | A User Theorem |
| isin-01 | ⊦ c ' + x + b ' = y + a ' + a ' + z ∧ a ≠ b → a ∈ x | A User Theorem |
| k-In | ⊦ a ∈ x ↔ x ≠ [] ∧ (a = x.first ∨ a ∈ x.rest) | A User Theorem |
| k-Last-base | ⊦ [] + a = a ' | A User Theorem |
| k-Last-rec | ⊦ (a + x) + b = a + (x + b) | A User Theorem |
| k-Two | ⊦ a + b = a + b ' | A User Theorem |
| last | ⊦ x + a ' = b ' + y → (a ∈ y ↔ y ≠ []) | A User Theorem |
| last-01 | ⊦ x + b ' = a ' + y → (a ∈ x ↔ x ≠ []) | A User Theorem |
| lastdiv | ⊦ x ≠ [] → (∃ y, a. x = y + a ') | A User Theorem |
| lastdiv-rew | ⊦ x ≠ [] ↔ (∃ y, a. x = y + a ') | A User Theorem |
| lastoc | ⊦ a ∈ x → (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z) | A User Theorem |
| lastoc-rew | ⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ z) | A User Theorem |
| lasttwo | a ∈ x, a0 ∈ x ⊦ ∃ b, y, z. x = y + b ' + z ∧ (b = a ∨ b = a0) ∧ ¬ a ∈ z ∧ ¬ a0 ∈ z | A User Theorem |
| len | ⊦ #(x + y) = # x + # y | A User Theorem |
| len-01 | ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0) | A User Theorem |
| len-02 | ⊦ # a ' = 0 +1 | A User Theorem |
| len-03 | ⊦ a ' + x = y + b ' + z → ¬ # x < # z | A User Theorem |
| len-04 | ⊦ a ' + x0 = x + b ' + y + c ' + z → # x + # z < # x0 | A User Theorem |
| len-05 | ⊦ #(a ' + x) = (# x)+1 | A User Theorem |
| len-06 | ⊦ # y = # y0 → (x + y = z + y0 ↔ x = z ∧ y = y0) | A User Theorem |
| len-last-rest | ⊦ # (x + a ').rest = # x | A User Theorem |
| less-append | ⊦ x < a ' + y ↔ x = y ∨ x < y | A User Theorem |
| longest-common-prefix | ⊦ ∃ z, x0, y0. x = z + x0 ∧ y = z + y0 ∧ (x0 ≠ [] ∧ y0 ≠ [] → x0.first ≠ y0.first) | A User Theorem |
| neq | ⊦ ¬ a ∈ x → x ≠ y + a ' + z | A User Theorem |
| neq-01 | ⊦ ¬ a ∈ y ∧ ¬ a ∈ z ∧ a ≠ c → y + c ' + z ≠ y1 + a ' + x | A User Theorem |
| neq-02 | ⊦ ¬ a ∈ z ∧ a ≠ c → c ' + z ≠ y1 + a ' + x | A User Theorem |
| neq-03 | ⊦ ¬ c ∈ y ∧ c ≠ b → y + b ' ≠ y0 + c ' + z | A User Theorem |
| neq-04 | ⊦ a ∈ y0 ∧ ¬ a ∈ y ∧ a ≠ b → y + b ' ≠ y0 + c ' + z | A User Theorem |
| neq-05 | ⊦ ¬ b ∈ x → c ' + x ≠ y + a ' + b ' + z | A User Theorem |
| neq-06 | ⊦ ¬ a ∈ x ∧ a ≠ b → b ' + x + a ' ≠ y + a ' + b ' + z | A User Theorem |
| neq-07 | ⊦ a ≠ a0 ∧ a1 ≠ a0 ∧ a ≠ a1 ∧ ¬ a ∈ y1 ∧ ¬ a1 ∈ y0 → y1 + a0 ' + y0 + a ' ≠ y2 + a ' + a1 ' + z0 | A User Theorem |
| neq-09 | ⊦ ¬ a ∈ y ∧ a ≠ c ∧ ¬ a ∈ z → y + c ' + z ≠ y1 + c ' + a ' + z0 | A User Theorem |
| ni | ⊦ x + a ' = y + z ∧ ¬ a ∈ z → z = [] | A User Theorem |
| one | ⊦ x + y = a ' ∧ b ∈ x → a = b ∧ x = a ' ∧ y = [] | A User Theorem |
| one-01 | ⊦ y ≠ [] → (a ' = x + y ↔ x = [] ∧ a ' = y) | A User Theorem |
| onein | ⊦ # x = 1 ∧ a ∈ x → x = a ' | A User Theorem |
| rest | ⊦ a '.rest = [] | A User Theorem |
| rest-01 | ⊦ x ≠ [] → (x + y).rest = x.rest + y | A User Theorem |
| rewlem | ⊦ x + y = z → x + y + y0 = z + y0 | A User Theorem |
| some-element | ⊦ x = [] ↔ ¬(∃ a. a ∈ x) | A User Theorem |
| split-first | n ≤ # x ⊦ ∃ y, z. x = y + z ∧ # y = n | A User Theorem |
| split-rest | n ≤ # x ⊦ ∃ y, z. x = y + z ∧ # z = n | A User Theorem |
| two | ⊦ a ' + b ' = x + a0 ' + c ' + y ↔ x = [] ∧ y = [] ∧ a = a0 ∧ b = c | A User Theorem |
| unequal | # x = # y, x ≠ y ⊦ ∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y = z + b ' + z1 | A User Theorem |