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: |
|---|---|---|
| case-1 | ⊦ x = [] ∨ x = x.first + x.rest | An Axiom |
| disj-1 | ⊦ [] ≠ a + x | An Axiom |
| inj-1 | ⊦ a + x = a0 + x0 ↔ a = a0 ∧ x = x0 | An Axiom |
| sel-2 | ⊦ (a + x).rest = x | An Axiom |
| sel-1 | ⊦ (a + x).first = a | An Axiom |
| elim-1 | ⊦ x ≠ [] → (a = x.first ∧ x0 = x.rest ↔ x = a + x0) | An Axiom |
| noeth | < wellfounded | An Axiom |
| gen | list freely generated by [], +; | An Axiom |
| less-01 | ⊦ ¬ x < [] | An Axiom |
| less-02 | ⊦ x0 < a + x ↔ x0 = x ∨ x0 < x | An Axiom |
| trans-01 | ⊦ x < x0 ∧ x0 < x1 → x < x1 | An Axiom |
| ref-01 | ⊦ ¬ x < x | An Axiom |
| size-01 | ⊦ # [] = 0 | An Axiom |
| size-02 | ⊦ #(a + x) = (# x)+1 | An Axiom |
| elim-list | ⊦ x ≠ [] → (a = x.first ∧ y = x.rest ↔ x = a + y) | A User Theorem |
| elim-list-c | x ≠ [] ⊦ a = x.first ∧ y = x.rest ↔ x = a + y | A User Theorem |
| eq-one | ⊦ # x + # y = 1 ∧ x ≠ [] → # x = 1 ∧ y = [] | A User Theorem |
| exa | x ≠ [] ⊦ ∃ a, y. x = a + y | A User Theorem |
| f | ⊦ a + x = a + y ↔ x = y | A User Theorem |
| fr | ⊦ x ≠ [] ∧ x ≠ x.first + [] → x.rest.first + x.rest.rest = x.rest | A User Theorem |
| fr-01 | ⊦ x ≠ [] ∧ x ≠ x.first + [] → x.first + x.rest.first + x.rest.rest = x | A User Theorem |
| fr-02 | ⊦ x ≠ [] → x.first + x.rest = x | A User Theorem |
| fr-03 | ⊦ x.rest = [] ∧ x ≠ [] → x.first + [] = x | A User Theorem |
| fr-04 | ⊦ x.first = y.first → x.rest = y.rest → x = y ∨ x = [] ∨ y = [] | A User Theorem |
| fr-05 | ⊦ x ≠ [] → (x ≠ x.first + y ↔ x.rest ≠ y) | A User Theorem |
| fr-06 | ⊦ x ≠ [] ∧ x.rest = [] → x.first + [] = x | A User Theorem |
| fr-07 | ⊦ x ≠ [] → (x = x.first + y ↔ x.rest = y) | A User Theorem |
| l | ⊦ # x = 0 ↔ x = [] | A User Theorem |
| le-one | ⊦ # x ≤ 1 ∧ x ≠ [] → # x = 1 | A User Theorem |
| le-one-01 | ⊦ # x + # y ≤ 1 ∧ x ≠ [] → # x = 1 ∧ y = [] | A User Theorem |
| length-neq | ⊦ # x ≠ # y → x ≠ y | A User Theorem |
| length-rest | ⊦ x ≠ [] → # x.rest = (# x)-1 | A User Theorem |
| length-rest-intro | ⊦ x ≠ [] → # x = # x.rest + 1 | A User Theorem |
| lf | ⊦ 1 < # x → x ≠ x.first + [] | A User Theorem |
| lf-01 | ⊦ # x = 1 ↔ x = x.first + [] | A User Theorem |
| lfr | ⊦ n < # x → (x = x.first + y ↔ x.rest = y) | A User Theorem |
| lr | ⊦ true → # x + 1 < # x.rest → x = [] | A User Theorem |
| lr-01 | ⊦ x ≠ [] ∧ y ≠ [] → # x.rest + # y.rest < # x + # y | A User Theorem |
| lr-02 | ⊦ x ≠ [] → ¬ # x < # x.rest | A User Theorem |
| lr-03 | ⊦ x ≠ [] ∧ y ≠ [] → (# x.rest = # y.rest ↔ # x = # y) | A User Theorem |
| lr-04 | ⊦ # x.rest < # x ↔ x ≠ [] | A User Theorem |
| lr-05 | ⊦ ¬ # x.rest + 1 < # x | A User Theorem |
| lr-06 | ⊦ # x = # x.rest + 1 ↔ x ≠ [] | A User Theorem |
| p-fr | a + x = y ⊦ a = y.first ∧ x = y.rest | A User Theorem |