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: |
|---|---|---|
| last-02 | ⊦ x ≠ [] → x.butlast + x.last = x | An Axiom |
| rev-e | ⊦ rev([]) = [] | An Axiom |
| rev-r | ⊦ rev(a ' + x) = rev(x) + a | An Axiom |
| mk-len | ⊦ # mklist(a, n) = n | An Axiom |
| mk-elem | ⊦ a ∈ mklist(b, n) → a = b | An Axiom |
| postfix | ⊦ x ⊒ y ↔ (∃ z. z + x = y) | An Axiom |
| prefix | ⊦ x ⊑ y ↔ (∃ z. x + z = y) | An Axiom |
| butlastN-rec | ⊦ butlastn(n + 1, x) = butlastn(n, x.butlast) | An Axiom |
| butlastN-base | ⊦ butlastn(0, x) = x | An Axiom |
| fillfirst-fill | ⊦ # x < n → fillfirst(n, a, x) = mklist(a, n - # x) + x | An Axiom |
| fillfirst-longer | ⊦ n ≤ # x → fillfirst(n, a, x) = x | An Axiom |
| b | ⊦ a '.butlast = [] | A User Theorem |
| b-01 | ⊦ x ≠ [] → (x.butlast = [] ↔ x = x.first ') | A User Theorem |
| b-02 | ⊦ (a ' + x).butlast = [] ↔ x = [] | A User Theorem |
| bapp | ⊦ y ≠ [] → (x + y).butlast = x + y.butlast | A User Theorem |
| bc | ⊦ x ≠ [] → (a ' + x).butlast = a ' + x.butlast | A User Theorem |
| bin | ⊦ (x + a ' + y).butlast = x + (a ' + y).butlast | A User Theorem |
| bin-01 | x ≠ [] ⊦ a ∈ x.butlast → a ∈ x | A User Theorem |
| bin-02 | ⊦ ¬ a ∈ x.butlast ∧ a ∈ x → a = x.last | A User Theorem |
| bl | ⊦ (a ' + x).butlast + (a ' + x).last ' + y = a ' + x + y | A User Theorem |
| blapp | ⊦ x ≠ [] → (x.butlast ≠ y ↔ x ≠ y + x.last ') | A User Theorem |
| blapp-01 | ⊦ x ≠ [] → (x.butlast = y ↔ x = y + x.last ') | A User Theorem |
| blast-first | ⊦ a ∈ x.butlast ∧ x ≠ [] → x.butlast.first = x.first | A User Theorem |
| blastN-all | ⊦ butlastn(# x, x) = [] | A User Theorem |
| blastN-all-01 | n = # x ⊦ butlastn(n, x) = [] | A User Theorem |
| blastN-len | ⊦ n ≤ # x → # butlastn(n, x) = # x - n | A User Theorem |
| blastN-mklist | ⊦ butlastn(n, x + mklist(a, n)) = x | A User Theorem |
| blastN-rec | ⊦ n ≠ 0 → butlastn(n, x + a ') = butlastn(n -1, x) | A User Theorem |
| blastN-rec-01 | ⊦ n ≤ # x → butlastn(n, a ' + x) = a ' + butlastn(n, x) | A User Theorem |
| blastn-app-1 | ⊦ butlastn(1, x + a ') = x | A User Theorem |
| blastn-len-0 | ⊦ # x = n0 + n1 → # butlastn(n0, x) = n1 | A User Theorem |
| bnotempty | ⊦ 1 < # x → x.butlast ≠ [] | A User Theorem |
| btwo | ⊦ (a ' + b ' + x).butlast = a ' + (b ' + x).butlast | A User Theorem |
| butlast-def | ⊦ (x + a ').butlast = x | A User Theorem |
| butlast-eq | ⊦ x ≠ [] → (x.butlast + a ' = x ↔ a = x.last) | A User Theorem |
| butlast-last | x ≠ [] ⊦ x.butlast + x.last ' = x | A User Theorem |
| butlast-last-01 | ⊦ x.last = a ∧ x ≠ [] → x.butlast + a ' = x | A User Theorem |
| butlast-len | ⊦ # (a ' + x).butlast = # x | A User Theorem |
| consmklist-last | ⊦ (a ' + mklist(a, n)).last = a | A User Theorem |
| l | ⊦ a '.last = a | A User Theorem |
| l-01 | ⊦ x ≠ [] ∧ x.rest = [] → x.last = x.first | A User Theorem |
| l-02 | ⊦ x ≠ [] → (a ' + x).last = x.last | A User Theorem |
| l-03 | ⊦ x ≠ [] ∧ x.rest ≠ [] → x.rest.last = x.last | A User Theorem |
| l-04 | ⊦ x ≠ [] → x.rest.last ≠ x.last → x = x.first ' | A User Theorem |
| l-05 | ⊦ (b ' + a ' + x).last = (a ' + x).last | A User Theorem |
| l-06 | ⊦ x = x.first ' → x.last = x.first | A User Theorem |
| l-in | ⊦ a ∈ x → (b ' + x).last = x.last | A User Theorem |
| lapp | ⊦ y ≠ [] → (x + y).last = y.last | A User Theorem |
| lapp-01 | ⊦ (x + a ' + y).last = (a ' + y).last | A User Theorem |
| lapp-02 | ⊦ y ≠ [] → (a ' + x + y).last = y.last | A User Theorem |
| lapp-03 | ⊦ (a ' + x + b ' + y).last = (b ' + y).last | A User Theorem |
| lapp-04 | ⊦ a ' + x = y + b ' ∧ a ≠ b → x.last = b | A User Theorem |
| lapp-05 | ⊦ a ' + b ' + x = y + a ' → (b ' + x).last = a | A User Theorem |
| last-01 | ⊦ (a ' + x + b ').last = b | A User Theorem |
| last-def | ⊦ (x + a ').last = a | A User Theorem |
| last-elim | x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a ' | A User Theorem |
| last-ex | a ≠ x.last, a ∈ x ⊦ ∃ y, z. x = y + a ' + z ∧ z ≠ [] | A User Theorem |
| last-one | ⊦ # x = 1 → (y + x).last = x.first | A User Theorem |
| lb | ⊦ x ≠ [] → # x.butlast = # x - 1 | A User Theorem |
| lb-01 | ⊦ # x.butlast < # x ↔ x ≠ [] | A User Theorem |
| le-leq-one-empty-or-first-equal-last | ⊦ # x ≤ 1 → x = [] ∨ x.first = x.last | A User Theorem |
| lin | ⊦ true → ¬ x.last ∈ x.rest → x = [] ∨ x.rest = [] | A User Theorem |
| lin-01 | ⊦ x.last ∈ x ↔ x ≠ [] | A User Theorem |
| lin-02 | ⊦ x.last = a ∧ x ≠ [] → a ∈ x | A User Theorem |
| lthree | ⊦ y ≠ [] → (x + y + z).last = (y + z).last | A User Theorem |
| mk-butlast | ⊦ m ≠ 0 → (x + mklist(a, m)).butlast = x + mklist(a, m - 1) | A User Theorem |
| mk-butlast-01 | ⊦ m ≠ 0 → mklist(a, m).butlast = mklist(a, m - 1) | A User Theorem |
| mk-empty | ⊦ mklist(a, m) = [] ↔ m = 0 | A User Theorem |
| mk-first | ⊦ n ≠ 0 → (mklist(a, n) + x).first = a | A User Theorem |
| mk-first-01 | ⊦ m ≠ 0 → mklist(a, m).first = a | A User Theorem |
| mk-in | ⊦ a ∈ mklist(a, m) ↔ m ≠ 0 | A User Theorem |
| mk-inj | ⊦ m ≠ 0 → (mklist(a, m) = mklist(b, n) ↔ a = b ∧ m = n) | A User Theorem |
| mk-inj-01 | ⊦ mklist(a, m) = mklist(a, n) ↔ m = n | A User Theorem |
| mk-last | ⊦ mklist(a, n) + a ' = a ' + mklist(a, n) | A User Theorem |
| mk-last-01 | ⊦ m ≠ 0 → mklist(a, m).last = a | A User Theorem |
| mk-last-01-01 | ⊦ m ≠ 0 → (x + mklist(a, m)).last = a | A User Theorem |
| mk-last-02 | ⊦ n ≠ 0 → mklist(a, n) = mklist(a, n -1) + a ' | A User Theorem |
| mk-one | ⊦ m ≠ 0 → (mklist(a, m) + x = a ' ↔ m = 1 ∧ x = []) | A User Theorem |
| mk-one-01 | ⊦ mklist(a, n) = a ' ↔ n = 1 | A User Theorem |
| mk-plus | ⊦ mklist(a, m + n) = mklist(a, m) + mklist(a, n) | A User Theorem |
| mk-rec | ⊦ m ≠ 0 → mklist(a, m) = a + mklist(a, m - 1) | A User Theorem |
| mk-rest | ⊦ n ≠ 0 → mklist(a, n).rest = mklist(a, n -1) | A User Theorem |
| mk-rest-01 | ⊦ m ≠ 0 → (mklist(a, m) + x).rest = mklist(a, m -1) + x | A User Theorem |
| mk-succ | ⊦ mklist(a, n + 1) = a ' + mklist(a, n) | A User Theorem |
| mk-two | ⊦ mklist(a, n + 2) = a ' + a ' + mklist(a, n) | A User Theorem |
| mk-two-01 | ⊦ mklist(a, 2) = a ' + a ' | A User Theorem |
| mk-zero | ⊦ mklist(a, 0) = [] | A User Theorem |
| mklist-append | ⊦ mklist(a, m) + mklist(a, n) = mklist(a, m + n) | A User Theorem |
| mklist-last | ⊦ mklist(a, n) + a ' = mklist(a, n + 1) | A User Theorem |
| mklist-one | ⊦ mklist(a, 1) = a ' | A User Theorem |
| mklist-rmdup | ⊦ ¬ a ∈ x ∧ n ≠ 0 → rmdup(x + mklist(a, n)) = rmdup(x) + a ' | A User Theorem |
| mklist-rmdup-01 | ⊦ n ≠ 0 → rmdup(mklist(a, n)) = a ' | A User Theorem |
| mklist-split-intro | ⊦ n ≤ m → mklist(a, m) = mklist(a, m - n) + mklist(a, n) | A User Theorem |
| nodups-butlastn | ⊦ ¬ dups(x) ∧ n ≤ # x → (dups(butlastn(n, x)) ↔ false) | A User Theorem |
| postfix-app | ⊦ x + y ⊒ z → y ⊒ z | A User Theorem |
| postfix-app-01 | ⊦ x ⊒ y + x | A User Theorem |
| postfix-app-02 | ⊦ y + x ⊒ z + x ↔ y ⊒ z | A User Theorem |
| postfix-app-04 | ⊦ x = (y + a ') + z → a ' + z ⊒ x | A User Theorem |
| postfix-app-05 | ⊦ b ' + x ⊒ (y + b ') + x | A User Theorem |
| postfix-app-06 | ⊦ x + a ' ⊒ y + b ' ↔ a = b ∧ x ⊒ y | A User Theorem |
| postfix-empty | ⊦ [] ⊒ x | A User Theorem |
| postfix-empty-01 | ⊦ ¬ a ' + x ⊒ [] | A User Theorem |
| postfix-empty-02 | ⊦ ¬ x + a ' ⊒ [] | A User Theorem |
| postfix-empty-03 | ⊦ x ⊒ [] ↔ x = [] | A User Theorem |
| postfix-in | ⊦ a ∈ x ∧ x ⊒ y → a ∈ y | A User Theorem |
| postfix-in-01 | ⊦ a ∈ x ∧ ¬ a ∈ y → ¬ x ⊒ y | A User Theorem |
| postfix-in-02 | ⊦ a ∈ x ∧ x ⊒ y → (¬ a ∈ y ↔ false) | A User Theorem |
| postfix-in-03 | ⊦ a ' + x ⊒ y → (¬ a ∈ y ↔ false) | A User Theorem |
| postfix-is-lessOrEqual | ⊦ x ⊒ y ↔ x = y ∨ x < y | A User Theorem |
| postfix-length | ⊦ x ⊒ y → # x ≤ # y | A User Theorem |
| postfix-more | ⊦ ¬ x + a ' + y ⊒ x | A User Theorem |
| postfix-more-01 | ⊦ ¬ a ' + x ⊒ x | A User Theorem |
| postfix-one | ⊦ x ⊒ a ' ↔ x = [] ∨ x = a ' | A User Theorem |
| postfix-one-less | ⊦ a ' + x ⊒ y → (¬ x ⊒ y ↔ false) | A User Theorem |
| postfix-rec | ⊦ x ≠ [] ∧ y ≠ [] → (x ⊒ y ↔ x.last = y.last ∧ x.butlast ⊒ y.butlast) | A User Theorem |
| postfix-rec-right | ⊦ x ⊒ a ' + y ↔ x = a ' + y ∨ x ⊒ y | A User Theorem |
| postfix-reflexivity | ⊦ x ⊒ x | A User Theorem |
| postfix-rest | ⊦ x ≠ [] → x.rest ⊒ x | A User Theorem |
| postfix-rest-01 | ⊦ x ≠ [] ∧ x ⊒ y → x.rest ⊒ y | A User Theorem |
| postfix-same | ⊦ x + a ' ⊒ y + a ' ↔ x ⊒ y | A User Theorem |
| postfix-split-stronger | x ⊒ y + z, ¬ x ⊒ z ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y | A User Theorem |
| postfix-trans | ⊦ x ⊒ x0 ∧ x0 ⊒ y → x ⊒ y | A User Theorem |
| postifx-app-03 | ⊦ x + y ⊑ x + z ↔ y ⊑ z | A User Theorem |
| postifx-split | x ⊒ y + z, ¬ x ⊒ z ⊦ ∃ x0. x0 + z = x | A User Theorem |
| prefix-app | ⊦ ¬ x ⊑ y + z → ¬ x ⊑ y | A User Theorem |
| prefix-app-01 | ⊦ x + y ⊑ x ↔ y = [] | A User Theorem |
| prefix-app-02 | ⊦ x + y ⊑ y ↔ x = [] | A User Theorem |
| prefix-app-03 | ⊦ x + y + z ⊑ y ↔ x = [] ∧ z = [] | A User Theorem |
| prefix-app-04 | ⊦ x + y ⊑ z → x ⊑ z | A User Theorem |
| prefix-app-05 | ⊦ x ⊑ x + y | A User Theorem |
| prefix-app-size-eq | ⊦ # x0 = # x1 → (x0 ⊑ x1 + x2 ↔ x0 = x1) | A User Theorem |
| prefix-attach | ⊦ ¬ x ⊑ y → (x ⊑ y + a ' ↔ y + a ' = x) | A User Theorem |
| prefix-butlast | ⊦ x0 ≠ [] ∧ x0 ⊑ x1 → x0.butlast ⊑ x1 | A User Theorem |
| prefix-butlast-append | ⊦ x ≠ [] → (x ⊑ x.butlast + a ' ↔ a = x.last) | A User Theorem |
| prefix-empty | ⊦ x ⊑ [] ↔ x = [] | A User Theorem |
| prefix-empty-03 | ⊦ ¬ x + a ' + y ⊑ [] | A User Theorem |
| prefix-eq | ⊦ x ⊑ y → (y ⊑ x ↔ x = y) | A User Theorem |
| prefix-equality | ⊦ x = y ↔ x ⊑ y ∧ y ⊑ x | A User Theorem |
| prefix-ex | ⊦ ¬ x ⊑ y → (x ⊑ y + z ↔ (∃ x0. x = y + x0 ∧ x0 ⊑ z)) | A User Theorem |
| prefix-in | ⊦ x + a ' ⊑ y → (¬ a ∈ y ↔ false) | A User Theorem |
| prefix-in-01 | ⊦ ¬ a ∈ y → ¬ x + a ' + x0 ⊑ y | A User Theorem |
| prefix-in-02 | ⊦ a ∈ x ∧ x ⊑ y → a ∈ y | A User Theorem |
| prefix-in-03 | ⊦ a ' + x ⊑ y → (¬ a ∈ y ↔ false) | A User Theorem |
| prefix-intro | ⊦ ¬ x ⊑ y ∧ # x ≤ # y → x + x0 ≠ y + y0 | A User Theorem |
| prefix-longer | ⊦ ¬ x + a ' ⊑ x | A User Theorem |
| prefix-longer-01 | ⊦ # y < # x → ¬ x ⊑ y | A User Theorem |
| prefix-more | ⊦ ¬ x + a ' + y ⊑ x | A User Theorem |
| prefix-nil | ⊦ [] ⊑ x | A User Theorem |
| prefix-notin | ⊦ a ∈ x ∧ ¬ a ∈ y → ¬ x ⊑ y | A User Theorem |
| prefix-one | ⊦ a ' ⊑ b ' + x ↔ a = b | A User Theorem |
| prefix-one-01 | ⊦ x ⊑ a ' ↔ ¬ ¬(x = [] ∨ x = a ') | A User Theorem |
| prefix-rec | ⊦ x ≠ [] → (x ⊑ a ' + y ↔ x.first = a ∧ x.rest ⊑ y) | A User Theorem |
| prefix-rec-01 | ⊦ a ' + x ⊑ y ↔ y ≠ [] ∧ a = y.first ∧ x ⊑ y.rest | A User Theorem |
| prefix-rec-02 | ⊦ b ' + x ⊑ b ' + y ↔ x ⊑ y | A User Theorem |
| prefix-rec-03 | ⊦ a ' + x ⊑ b ' + y ↔ a = b ∧ x ⊑ y | A User Theorem |
| prefix-same | ⊦ x + a ' ⊑ x + a ' + y | A User Theorem |
| prefix-same-01 | ⊦ x = y + a ' + z → y + a ' ⊑ x | A User Theorem |
| prefix-self | ⊦ x ⊑ x | A User Theorem |
| prefix-size-eq | ⊦ # x0 = # x1 → (x0 ⊑ x1 ↔ x0 = x1) | A User Theorem |
| prefix-split | x ⊑ y + z, ¬ x ⊑ y ⊦ ∃ x0. y + x0 = x | A User Theorem |
| prefix-split-stronger | x ⊑ y + z, ¬ x ⊑ y ⊦ ∃ x0. x = y + x0 ∧ x0 ⊑ z | A User Theorem |
| prefix-trans | ⊦ x ⊑ y ∧ y ⊑ z → x ⊑ z | A User Theorem |
| rev-app | ⊦ rev(x + y) = rev(y) + rev(x) | A User Theorem |
| rev-disjoint | ⊦ disj(x, rev(y)) ↔ disj(x, y) | A User Theorem |
| rev-disjoint-01 | ⊦ disj(rev(x), y) ↔ disj(x, y) | A User Theorem |
| rev-dups | ⊦ dups(rev(x)) ↔ dups(x) | A User Theorem |
| rev-empty | ⊦ rev(x) = [] ↔ x = [] | A User Theorem |
| rev-in | ⊦ a ∈ rev(x) ↔ a ∈ x | A User Theorem |
| rev-length | ⊦ # rev(x) = # x | A User Theorem |
| rev-mklist | ⊦ rev(mklist(a, n)) = mklist(a, n) | A User Theorem |
| rev-one | ⊦ rev(a ') = a ' | A User Theorem |
| rev-rest | ⊦ x ≠ [] → (rev(x) + y).rest = rev(x).rest + y | A User Theorem |
| rev-rev-identity | ⊦ rev(rev(x)) = x | A User Theorem |
| rev-rewrite | ⊦ rev(x) = y ↔ x = rev(y) | A User Theorem |
| revert-equal | ⊦ rev(x) = rev(y) ↔ x = y | A User Theorem |
| revert-last | ⊦ a ' + rev(x) = rev(x + a ') | A User Theorem |
| splitlasteq | y ≠ [] ⊦ x + a ' = y ↔ x = y.butlast ∧ a = y.last | A User Theorem |
| splitlasteq-01 | y ≠ [] ⊦ y = x + a ' ↔ x = y.butlast ∧ a = y.last | A User Theorem |