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: |
|---|---|---|
| del-e | ⊦ [] -l a = [] | An Axiom |
| del-y | ⊦ (a ' + x) -l a = x -l a | An Axiom |
| del-n | ⊦ a ≠ b → (b ' + x) -l a = b ' + (x -l a) | An Axiom |
| del1-e | ⊦ [] -1l a = [] | An Axiom |
| del1-y | ⊦ (a ' + x) -1l a = x | An Axiom |
| del1-n | ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a) | An Axiom |
| pos-n | ⊦ a ≠ b → pos(a, b ' + x) = pos(a, x) + 1 | An Axiom |
| pos-y | ⊦ pos(a, a ' + x) = 0 | An Axiom |
| pos-e | ⊦ pos(a, []) = 0 | An Axiom |
| delpos-rec | ⊦ (a ' + x) -1l (n + 1) = a + (x -1l n) | An Axiom |
| delpos-base | ⊦ (a ' + x) -1l 0 = x | An Axiom |
| delpos-empty | ⊦ [] -1l n = [] | An Axiom |
| put-succ | ⊦ (b ' + x)[n + 1, a] = b + x[n, a] | An Axiom |
| put-zero | ⊦ (b ' + x)[0, a] = a + x | An Axiom |
| get-succ | ⊦ (a ' + x)[n + 1] = x[n] | An Axiom |
| get-zero-01 | ⊦ (a ' + x)[0] = a | An Axiom |
| fromE-no | ⊦ a ≠ b → frome(a ' + x, b) = frome(x, b) | An Axiom |
| fromE-yes | ⊦ frome(a ' + x, a) = a ' + x | An Axiom |
| fromE-empty | ⊦ frome([], a) = [] | An Axiom |
| restN-rec | ⊦ restn(n + 1, x) = restn(n, x.rest) | An Axiom |
| restN-zero | ⊦ restn(0, x) = x | An Axiom |
| firstN-rec | ⊦ firstn(n + 1, x) = x.first + firstn(n, x.rest) | An Axiom |
| firstN-zero | ⊦ firstn(0, x) = [] | An Axiom |
| lastN-rec | ⊦ lastn(n + 1, x) = lastn(n, x.butlast) + x.last | An Axiom |
| lastN-zero | ⊦ lastn(0, x) = [] | An Axiom |
| sublist-def | ⊦ sublist(m, n, x) = firstn(n, restn(m, x)) | An Axiom |
| app | ⊦ a ∈ x → (x + y) -1l a = (x -1l a) + y | A User Theorem |
| app-01 | ⊦ ¬ a ∈ x → (x + y) -1l a = x + (y -1l a) | A User Theorem |
| app-05 | ⊦ a ∈ x → pos(a, x + y) = pos(a, x) | A User Theorem |
| app-05-neg | ⊦ ¬ a ∈ x → pos(a, x + y) = pos(a, y) + # x | A User Theorem |
| append-mod | ⊦ # x ≤ n ∧ n < # x + # x0 → ((x + x0)[n, a] = x + x1 ↔ x0[n - # x, a] = x1) | A User Theorem |
| at-last | ⊦ x ≠ [] → x[# x - 1] = x.last | A User Theorem |
| blastN-firstN | ⊦ n ≤ # x → butlastn(n, x) = firstn(# x - n, x) | A User Theorem |
| del-append | ⊦ (x + y) -l a = (x -l a) + (y -l a) | A User Theorem |
| del-del | ⊦ (x -l a) -l a = x -l a | A User Theorem |
| del-del1-nodups | ⊦ ¬ dups(x) → x -l a = x -1l a | A User Theorem |
| del-del1-switch | ⊦ a ≠ b → (x -1l a) -l b = (x -l b) -1l a | A User Theorem |
| del-length | ⊦ ¬ # x < #(x -l a) | A User Theorem |
| del-n-simp | a ≠ b ⊦ ((* a) ' + x) -l (* b) = a ' + (x -l b) | A User Theorem |
| del-one-simp | a ≠ b ⊦ (* a) ' -l (* b) = a ' | A User Theorem |
| del-rev | ⊦ rev(x) -l a = rev(x -l a) | A User Theorem |
| del-rev-01 | ⊦ rev(x -l a) = rev(x) -l a | A User Theorem |
| del-rmdup | ⊦ rmdup(x -l a) = rmdup(x) -l a | A User Theorem |
| del-rmdup-01 | ⊦ rmdup(x) -l a = rmdup(x -l a) | A User Theorem |
| del-rmdup-length-nle | ⊦ ¬ # rmdup(a ' + x) ≤ # rmdup(x -l a) | A User Theorem |
| del1-del | ⊦ (x -1l a) -l a = x -l a | A User Theorem |
| del1-del-switch | ⊦ a ≠ b → (x -l a) -1l b = (x -1l b) -l a | A User Theorem |
| del1-empty | ⊦ x ≠ [] → (x -1l a = [] ↔ x = a ') | A User Theorem |
| del1-first | ⊦ x.first = a ∧ x ≠ [] → a ' + (x -1l a) = x | A User Theorem |
| del1-in | ⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x) | A User Theorem |
| delete-dups | ⊦ ¬ dups(x) → ¬ dups(x -l a) | A User Theorem |
| delete-one-le | ⊦ #(x -1l a) ≤ # x | A User Theorem |
| delete-one-nls | ⊦ ¬ # x < #(x -1l a) | A User Theorem |
| delnr-one | ⊦ a ' -1l 0 = [] | A User Theorem |
| delpos-atsizeid | ⊦ x -1l # x = x | A User Theorem |
| delpos-in | ⊦ a ∈ x -1l n → (¬ a ∈ x ↔ false) | A User Theorem |
| dups | ⊦ dups(x -1l a) → dups(x) | A User Theorem |
| dups-01 | ⊦ ¬ dups(y) → ¬ b ∈ y -1l b | A User Theorem |
| dups-def | ⊦ dups(x) ↔ (∃ m, n. m < # x ∧ n < # x ∧ m ≠ n ∧ x[m] = x[n]) | A User Theorem |
| dups-first-last-split | ⊦ n ≤ # x → (dups(x) ↔ dups(firstn(n, x) + lastn(# x - n, x))) | A User Theorem |
| elim-firstn-restn | ⊦ n ≤ # x → (y = firstn(n, x) ∧ z = restn(n, x) ↔ x = y + z ∧ # y = n) | A User Theorem |
| elim-lastn-butlastn | ⊦ n ≤ # x → (y = butlastn(n, x) ∧ z = lastn(n, x) ↔ x = y + z ∧ # z = n) | A User Theorem |
| extension | ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n]) | A User Theorem |
| first-all | ⊦ firstn(# x, x) = x | A User Theorem |
| first-all-01 | ⊦ # x = n → firstn(n, x) = x | A User Theorem |
| first-append | ⊦ m ≤ # x → firstn(m, x + y) = firstn(m, x) | A User Theorem |
| first-append-01 | ⊦ n + m ≤ # x → firstn(m, restn(n, x) + y) = firstn(m, restn(n, x)) | A User Theorem |
| first-length | ⊦ # firstn(n, x) = n | A User Theorem |
| first-mklist | ⊦ m ≤ n → firstn(m, mklist(a, n)) = mklist(a, m) | A User Theorem |
| first-mklist-01 | ⊦ m + m0 ≤ n → firstn(m, mklist(a, n)) = mklist(a, m) | A User Theorem |
| first-mklist-02 | ⊦ firstn(m, mklist(a, m) + mklist(a, n)) = mklist(a, m) | A User Theorem |
| first-mklist-03 | ⊦ firstn(m, mklist(a, n) + mklist(a, m)) = mklist(a, m) | A User Theorem |
| first-mklist-04 | ⊦ firstn(m, mklist(a, m)) = mklist(a, m) | A User Theorem |
| first-num | n ≠ 0 ⊦ firstn((* n), x) = x.first ' + firstn(n -1, x.rest) | A User Theorem |
| first-sub | ⊦ firstn(n, x) = sublist(0, n, x) | A User Theorem |
| firstN-dups | ⊦ n < # x ∧ ¬ dups(x + y) → ¬ dups(firstn(n, x) + y) | A User Theorem |
| firstN-dups-01 | ⊦ n < # y ∧ ¬ dups(x + y) → ¬ dups(x + firstn(n, y)) | A User Theorem |
| firstN-dups-02 | ⊦ n ≤ # x ∧ ¬ dups(x + y) → ¬ dups(firstn(n, x) + y) | A User Theorem |
| firstN-dups-03 | ⊦ n ≤ # y ∧ ¬ dups(x + y) → ¬ dups(x + firstn(n, y)) | A User Theorem |
| firstN-dups-04 | ⊦ n ≤ # x ∧ ¬ dups(x) → ¬ dups(firstn(n, x)) | A User Theorem |
| firstN-dups-05 | ⊦ n < # x ∧ ¬ dups(x) → ¬ dups(firstn(n, x)) | A User Theorem |
| firstN-empty | ⊦ firstn(n, x) = [] ↔ n = 0 | A User Theorem |
| firstN-in | ⊦ ¬ a ∈ x ∧ n ≤ # x → ¬ a ∈ firstn(n, x) | A User Theorem |
| firstN-in-01 | ⊦ ¬ a ∈ x ∧ n < # x → ¬ a ∈ firstn(n, x) | A User Theorem |
| firstN-in-02 | ⊦ ¬ a ∈ x ∧ n ≤ # x → ¬ a ∈ firstn(# x - n, x) | A User Theorem |
| firstN-in-03 | ⊦ ¬ a ∈ x ∧ n < # x → ¬ a ∈ firstn(# x - n, x) | A User Theorem |
| firstN-in-04 | ⊦ a ∈ firstn(n, x) ∧ n ≤ # x → a ∈ x | A User Theorem |
| firstN-in-05 | ⊦ a ∈ firstn(n, x) ∧ n < # x → a ∈ x | A User Theorem |
| firstN-lastN | ⊦ n ≤ # x → firstn(# x - n, x) + lastn(n, x) = x | A User Theorem |
| firstN-lastN-in | ⊦ n ≤ # x ∧ a ∈ x ∧ ¬ a ∈ lastn(n, x) → (¬ a ∈ firstn(# x - n, x) ↔ false) | A User Theorem |
| firstN-lastN-in-01 | ⊦ n < # x ∧ a ∈ x ∧ ¬ a ∈ lastn(n, x) → (¬ a ∈ firstn(# x - n, x) ↔ false) | A User Theorem |
| firstN-len | ⊦ firstn(# x, x + y) = x | A User Theorem |
| firstN-num-rec | n ≠ 0 ⊦ firstn((* n), a ' + x) = a ' + firstn(n -1, x) | A User Theorem |
| firstN-rec-01 | ⊦ n ≠ 0 → firstn(n, a ' + x) = a ' + firstn(n -1, x) | A User Theorem |
| firstn-allprefix | ⊦ # x0 = n ∧ x0 ⊑ x2 → firstn(n, x2) = x0 | A User Theorem |
| firstn-app | ⊦ firstn(# x + n, x + y) = x + firstn(n, y) | A User Theorem |
| firstn-app-01 | ⊦ # x ≤ n → firstn(n, x + y) = x + firstn(n - # x, y) | A User Theorem |
| firstn-app-02 | ⊦ m ≤ # x + # y ∧ # x ≤ m → firstn(m, x + y) = x + firstn(m - # x, y) | A User Theorem |
| firstn-app-exact | ⊦ n = # x → firstn(n, x + y) = x | A User Theorem |
| firstn-append | ⊦ x = firstn(n, x) + a ' + y → firstn(n + 1, x) = firstn(n, x) + a ' | A User Theorem |
| firstn-append-01 | ⊦ x = firstn(# x - 1 + # z, x) + a ' + z → (x ≠ firstn(# x - # z, x) + z ↔ false) | A User Theorem |
| firstn-at-in-dups | ⊦ ¬ dups(x) ∧ n < # x → ¬ x[n] ∈ firstn(n, x) | A User Theorem |
| firstn-butlast | ⊦ x = firstn(# x - 1 + # z, x) + a ' + z → firstn(# x - # z, x).butlast = firstn(# x - 1 + # z, x) | A User Theorem |
| firstn-butlast-intro | ⊦ n < # x → firstn(n, x) = firstn(n, x.butlast) | A User Theorem |
| firstn-first | ⊦ n ≠ 0 ∧ x ≠ [] → firstn(n, x).first = x.first | A User Theorem |
| firstn-firstn | ⊦ m ≤ n ∧ n ≤ # x → firstn(m, firstn(n, x)) = firstn(m, x) | A User Theorem |
| firstn-last | ⊦ m ≠ 0 ∧ m ≤ # x → firstn(m, x).last = x[m -1] | A User Theorem |
| firstn-last-01 | ⊦ x = firstn(# x - 1 + # z, x) + a ' + z → firstn(# x - # z, x).last = a | A User Theorem |
| firstn-last-eq | ⊦ n ≤ # x → firstn(n, x) + lastn(# x - n, x) = x | A User Theorem |
| firstn-last-rec | ⊦ n ≠ 0 ∧ n ≤ # x → firstn(n, x) = firstn(n -1, x) + x[n -1] | A User Theorem |
| firstn-length | ⊦ x = firstn(n, y) + a ' + z → (¬ # x ≥ n + 1 ↔ false) | A User Theorem |
| firstn-length-01 | ⊦ x = firstn(n, x) + a ' + z → (¬ # x > # z ↔ false) | A User Theorem |
| firstn-length-02 | ⊦ x = firstn(# x - 1 + # z, x) + a ' + z → (¬ # x - # z ≠ 0 ↔ false) | A User Theorem |
| firstn-length-03 | ⊦ n < # x → # firstn(n, x) = n | A User Theorem |
| firstn-length-04 | ⊦ n ≤ # x → # firstn(n, x) = n | A User Theorem |
| firstn-one | ⊦ firstn(1, a ' + x) = a ' | A User Theorem |
| firstn-one-01 | ⊦ x ≠ [] → firstn(1, x) = x.first ' | A User Theorem |
| firstn-one-02 | ⊦ firstn(1, a ') = a ' | A User Theorem |
| firstn-prefix | ⊦ n ≤ # x → (¬ firstn(n, x) ⊑ x ↔ false) | A User Theorem |
| firstn-prefix-01 | ⊦ x = firstn(n, x) + z → (¬ firstn(n, x) ⊑ x ↔ false) | A User Theorem |
| firstn-prefix-02 | ⊦ # x = n0 + # z ∧ z ⊒ x → (¬ firstn(n0, x) ⊑ x ↔ false) | A User Theorem |
| firstn-prefix-03 | ⊦ # x = (1 + # z) + n0 ∧ a ' + z ⊒ x → (¬ firstn(n0, x) ⊑ x ↔ false) | A User Theorem |
| firstn-prefix-04 | ⊦ # x = (1 + # z) + n0 → (¬ firstn(1 + n0, x) ⊑ x ↔ false) | A User Theorem |
| firstn-restn | ⊦ firstn(m, restn(n, x)) = sublist(n, m, x) | A User Theorem |
| firstn-restn-01 | ⊦ firstn(m, restn(n, x)) = sublist(n, m, x) | A User Theorem |
| firstn-restn-eq | ⊦ n ≤ # x → firstn(n, x) + restn(n, x) = x | A User Theorem |
| firstn-restn-in | ⊦ n ≤ # x → (a ∈ x ↔ a ∈ firstn(n, x) ∨ a ∈ restn(n, x)) | A User Theorem |
| firstn-twice | ⊦ n ≤ # x → firstn(n, firstn(n, x)) = firstn(n, x) | A User Theorem |
| firstn-two | ⊦ firstn(2, a ' + b ') = a ' + b ' | A User Theorem |
| firstrestex | ⊦ n < # x ↔ x = firstn(n, x) + restn(n, x) ∧ n < # x | A User Theorem |
| from-notin | ⊦ ¬ a ∈ x → frome(x, a) = [] | A User Theorem |
| from-rest | ⊦ a ∈ x → frome(x, a) = restn(pos(a, x), x) | A User Theorem |
| get | ⊦ a ∈ x → x[pos(a, x)] = a | A User Theorem |
| get-add-num | n ≠ 0 ⊦ (a ' + x)[m + (* n)] = x[m + (n - 1)] | A User Theorem |
| get-app | ⊦ (x + a ' + y)[# x] = a | A User Theorem |
| get-app-1 | ⊦ (x0 + x1)[# x0] = x1[0] | A User Theorem |
| get-append-grt | ⊦ ¬ n < # x → (x + y)[n] = y[n - # x] | A User Theorem |
| get-append-grt-02 | ⊦ (x + y)[n + # x] = y[n] | A User Theorem |
| get-append-less | ⊦ n < # x → (x + y)[n] = x[n] | A User Theorem |
| get-butlast | ⊦ n < # x → (x + a ')[n] = x[n] | A User Theorem |
| get-firstn | ⊦ n < m ∧ m ≤ # x → firstn(m, x)[n] = x[n] | A User Theorem |
| get-in | ⊦ m < # x → (¬ x[m] ∈ x ↔ false) | A User Theorem |
| get-last | ⊦ n = # x → (x + a ')[n] = a | A User Theorem |
| get-last-01 | ⊦ (a + x)[# x] = (a + x).last | A User Theorem |
| get-last-03 | ⊦ (x + a ')[# x] = a | A User Theorem |
| get-last-04 | ⊦ (a ' + x + y)[# x] = (a ' + x).last | A User Theorem |
| get-last-nonempty | ⊦ n = # x - 1 ∧ 0 < # x → x[n] = x.last | A User Theorem |
| get-last2 | ⊦ (a ' + x)[# x] = (a ' + x).last | A User Theorem |
| get-mklist | ⊦ (a ' + mklist(a, m))[m] = a | A User Theorem |
| get-mklist-01 | ⊦ m < n → mklist(a, n)[m] = a | A User Theorem |
| get-nodups | ⊦ m < # x ∧ n < # x ∧ ¬ dups(x) → (x[m] = x[n] ↔ m = n) | A User Theorem |
| get-numrec | n ≠ 0 ⊦ (a ' + x)[(* n)] = x[n -1] | A User Theorem |
| get-rec | ⊦ x ≠ [] ∧ n ≠ 0 → x[n] = x.rest[n - 1] | A User Theorem |
| get-rec-01 | ⊦ x ≠ [] → x[n + 1] = x.rest[n] | A User Theorem |
| get-restn | ⊦ m + n < # x → restn(n, x)[m] = x[m + n] | A User Theorem |
| get-zero | ⊦ x ≠ [] → x[0] = x.first | A User Theorem |
| in | ⊦ a ∈ x ∧ a ≠ b → a ∈ x -l b | A User Theorem |
| in-01 | ⊦ a ∈ x -l b → a ∈ x ∧ a ≠ b | A User Theorem |
| in-01-01 | ⊦ a ∈ x -1l b → a ∈ x | A User Theorem |
| in-02 | ⊦ ¬ a ∈ x -l a | A User Theorem |
| in-02-01 | ⊦ ¬ a ∈ x → x -1l a = x | A User Theorem |
| in-03 | ⊦ ¬ a ∈ x → x -l a = x | A User Theorem |
| in-04 | ⊦ a ∈ x ∧ a ≠ b → a ∈ x -1l b | A User Theorem |
| in-05 | ⊦ ¬ a ∈ y -1l b ∧ a ∈ y → a = b | A User Theorem |
| in-del | ⊦ a ∈ x → (a ∈ x -l b ↔ a ≠ b) | A User Theorem |
| in-del-new | ⊦ a ∈ x -l b ↔ a ∈ x ∧ a ≠ b | A User Theorem |
| in-get | ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a) | A User Theorem |
| inl | ⊦ a ∈ x → pos(a, x) < # x | A User Theorem |
| inl-01 | ⊦ a ∈ x → ¬ # x ≤ pos(a, x) | A User Theorem |
| l | ⊦ a ∈ x → #(x -1l a) = (# x)-1 | A User Theorem |
| l-01 | ⊦ # x = #(x -1l a) ↔ ¬ a ∈ x | A User Theorem |
| l-02 | ⊦ # x + # y = #(y -1l a) ↔ x = [] ∧ ¬ a ∈ y | A User Theorem |
| lastN-all | ⊦ n = # x → lastn(n, x) = x | A User Theorem |
| lastN-append | ⊦ n = # y → lastn(n, x + y) = y | A User Theorem |
| lastN-append-01 | ⊦ n ≤ # y → lastn(n, x + y) = lastn(n, y) | A User Theorem |
| lastN-blastN | ⊦ n ≤ # x → butlastn(n, x) + lastn(n, x) = x | A User Theorem |
| lastN-dups | ⊦ ¬ dups(x) ∧ n < # x → ¬ dups(lastn(n, x)) | A User Theorem |
| lastN-dups-01 | ⊦ ¬ dups(x) ∧ n ≤ # x → ¬ dups(lastn(n, x)) | A User Theorem |
| lastN-empty | ⊦ lastn(n, x) = [] ↔ n = 0 | A User Theorem |
| lastN-ex | n ≤ # x ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = # x - n | A User Theorem |
| lastN-in | ⊦ ¬ a ∈ x ∧ n < # x → ¬ a ∈ lastn(n, x) | A User Theorem |
| lastN-in-01 | ⊦ ¬ a ∈ x ∧ n ≤ # x → ¬ a ∈ lastn(n, x) | A User Theorem |
| lastN-rec-01 | ⊦ lastn(n + 1, x + a ') = lastn(n, x) + a ' | A User Theorem |
| lastN-rec-02 | ⊦ n < # x → lastn(n, x) = lastn(n, x.rest) | A User Theorem |
| lastN-rest | ⊦ n < # x → lastn(n, x.rest) = lastn(n, x) | A User Theorem |
| lastN-rest-01 | ⊦ # x = n + 1 → lastn(n, x) = x.rest | A User Theorem |
| lastn-app | ⊦ # y ≤ n → lastn(n, x + y) = lastn(n - # y, x) + y | A User Theorem |
| lastn-firstn-in | ⊦ lastn(n, x) = y ∧ ¬ a ∈ y ∧ a ∈ x ∧ n ≤ # x → a ∈ firstn(# x - n, x) | A User Theorem |
| lastn-firstn-in-01 | ⊦ lastn(n, x) = y ∧ ¬ a ∈ y ∧ a ∈ x ∧ n ≤ # x ∧ m = # x - n → a ∈ firstn(m, x) | A User Theorem |
| lastn-lastn | ⊦ lastn(n, lastn(n, x)) = lastn(n, x) | A User Theorem |
| lastn-lastn-01 | ⊦ m ≤ n → lastn(m, lastn(n, x)) = lastn(m, x) | A User Theorem |
| lastn-length | ⊦ # lastn(n, x) = n | A User Theorem |
| lastn-length-01 | ⊦ n ≤ # x → # lastn(n, x) = n | A User Theorem |
| lastn-mklist | ⊦ m ≤ n → lastn(m, mklist(a, n)) = mklist(a, m) | A User Theorem |
| lastn-mklist-01 | ⊦ lastn(n, x + mklist(a, n)) = mklist(a, n) | A User Theorem |
| lastn-mklist-02 | ⊦ lastn(n + 1, x + b ' + mklist(a, n)) = b ' + mklist(a, n) | A User Theorem |
| lastn-mklist-03 | ⊦ lastn(n, mklist(a, n)) = mklist(a, n) | A User Theorem |
| lastn-neq | ⊦ n ≤ # x ∧ ¬ a ∈ x → lastn(n, x) ≠ a ' + y | A User Theorem |
| lastn-neq-01 | ⊦ n ≤ # x ∧ a ∈ y ∧ ¬ a ∈ x → lastn(n, x) ≠ b ' + y | A User Theorem |
| lastn-neq-02 | ⊦ # y ≠ n → lastn(n + 1, x) ≠ a ' + y | A User Theorem |
| lastn-neq-04 | ⊦ n ≤ # x ∧ b ∈ y ∧ ¬ b ∈ x → lastn(n, x) ≠ a ' + y | A User Theorem |
| lastn-one | ⊦ lastn(1, x) = x.last ' | A User Theorem |
| lastn-one-01 | ⊦ lastn(1, a ') = a ' | A User Theorem |
| lastn-rec | ⊦ n ≠ 0 → lastn(n, x) = lastn(n -1, x.butlast) + x.last | A User Theorem |
| lastn-restn | ⊦ m + n ≤ # x → lastn(m, restn(n, x)) = lastn(m, x) | A User Theorem |
| lastn-restn-01 | n ≤ # x ⊦ lastn(n, x) = restn(# x - n, x) | A User Theorem |
| len | ⊦ pos(a, x) ≤ # x | A User Theorem |
| len-01 | ⊦ ¬ # x < pos(a, x) | A User Theorem |
| list-select-not-first | ⊦ x = a ' + x0 → x[m + 1] = x0[m] | A User Theorem |
| nodups-rmposnodups | ⊦ ¬ dups(x) → (dups(x -1l n) ↔ false) | A User Theorem |
| notin-03 | ⊦ ¬ a ∈ x → pos(a, x) = # x | A User Theorem |
| num-lastN | 0 < n ⊦ lastn((* n), x + a ') = lastn(n -1, x) + a ' | A User Theorem |
| one | ⊦ a ' -l a = [] | A User Theorem |
| one-01 | ⊦ a ' -1l a = [] | A User Theorem |
| one-01-01 | ⊦ a ≠ b → a ' -1l b = a ' | A User Theorem |
| one-03 | ⊦ a '[0] = a | A User Theorem |
| pos-equal | ⊦ a ∈ x ∧ pos(a, x) = n → (pos(b, x) = n ↔ a = b) | A User Theorem |
| pos-get | ⊦ ¬ dups(x) ∧ n < # x → pos(x[n], x) = n | A User Theorem |
| pos-get-01 | ⊦ ¬ dups(x) ∧ x[n] = a ∧ n < # x → pos(a, x) = n | A User Theorem |
| pos-one | ⊦ pos(a, a ') = 0 | A User Theorem |
| possize-notin | ⊦ pos(a, x) = # x ↔ ¬ a ∈ x | A User Theorem |
| put-app-left | ⊦ n < # x → (x + y)[n, a] = x[n, a] + y | A User Theorem |
| put-app-right | ⊦ # x ≤ n → (x + y)[n, a] = x + y[n - # x, a] | A User Theorem |
| put-at | m < # x ⊦ m ≠ n → x[m, a][n] = x[n] | A User Theorem |
| put-at-eq | m < # x ⊦ x[m, a][m] = a | A User Theorem |
| put-butlast | ⊦ n < # x → (x + a ')[n, b] = x[n, b] + a ' | A User Theorem |
| put-del1-in | ⊦ x[m] ≠ a ∧ m < # x → (a ∈ x[m, a] -1l a ↔ a ∈ x) | A User Theorem |
| put-firstn-restn | ⊦ n < # x → x[n, a] = firstn(n, x) + a ' + restn(n + 1, x) | A User Theorem |
| put-in | ⊦ a ≠ x[m] ∧ m < # x → (a ∈ x[m, b] ↔ a = b ∨ a ∈ x) | A User Theorem |
| put-in-01 | ⊦ m < # x → (a ∈ x[m, b] ↔ a = b ∨ a ∈ x -1l x[m]) | A User Theorem |
| put-in-02 | ⊦ m < # x → a ∈ x[m, a] | A User Theorem |
| put-last | ⊦ n = # x → (x + a ')[n, b] = x + b ' | A User Theorem |
| put-length | ⊦ n < # x → # x[n, a] = # x | A User Theorem |
| put-one | ⊦ a '[0, b] = b ' | A User Theorem |
| put-one-01 | ⊦ (a ' + b ')[1, a0] = a ' + a0 ' | A User Theorem |
| put-rec | ⊦ n ≠ 0 ∧ x ≠ [] → x[n, a] = x.first ' + x.rest[n -1, a] | A User Theorem |
| put-rec-01 | ⊦ n ≠ 0 ∧ x ≠ [] → x[n, a] = x.first ' + x.rest[n -1, a] | A User Theorem |
| put-rec-02 | ⊦ n ≠ 0 → (a ' + x)[n, b] = a ' + x[n -1, b] | A User Theorem |
| put-same | ⊦ x[m] = a ∧ m < # x → x[m, a] = x | A User Theorem |
| put-sw-in | ⊦ m < # x ∧ n < # x → (a ∈ x[m, x[n]][n, x[m]] ↔ a ∈ x) | A User Theorem |
| put-zero-01 | ⊦ x ≠ [] → x[0, a] = a ' + x.rest | A User Theorem |
| putset-same | ⊦ n < # x → x[n, x[n]] = x | A User Theorem |
| rest-app | ⊦ m ≤ # x + # y ∧ # x ≤ m → restn(m, x + y) = restn(m - # x, y) | A User Theorem |
| rest-append | ⊦ n + m ≤ # x → restn(n, x + y) = restn(n, x) + y | A User Theorem |
| rest-empty | ⊦ # x = n → restn(n, x) = [] | A User Theorem |
| rest-in | ⊦ a ∈ restn(n, x) ∧ n ≤ # x → a ∈ x | A User Theorem |
| rest-in-01 | ⊦ a ∈ restn(n, x) ∧ ¬ a ∈ x → ¬ n ≤ # x | A User Theorem |
| rest-len | n ≤ # x ⊦ # restn(n, x) = # x - n | A User Theorem |
| rest-mklist | ⊦ m ≤ n → restn(m, mklist(a, n)) = mklist(a, n - m) | A User Theorem |
| rest-mklist-01 | ⊦ m + m0 ≤ n → restn(m, mklist(a, n)) = mklist(a, n - m) | A User Theorem |
| rest-mklist-02 | ⊦ restn(m, mklist(a, m) + mklist(a, n)) = mklist(a, n) | A User Theorem |
| rest-mklist-03 | ⊦ restn(m, mklist(a, n) + mklist(a, m)) = mklist(a, n) | A User Theorem |
| rest-mklist-04 | ⊦ restn(m, mklist(a, m)) = [] | A User Theorem |
| rest-one | ⊦ restn(1, a ' + x) = x | A User Theorem |
| rest-one-01 | ⊦ restn(1, a ') = [] | A User Theorem |
| rest-rec | ⊦ 0 < n → restn(n, x) = restn(n -1, x.rest) | A User Theorem |
| rest-rest1 | ⊦ x.rest = restn(1, x) | A User Theorem |
| rest-sub | ⊦ n ≤ # x → restn(n, x) = sublist(n, # x - n, x) | A User Theorem |
| rest-two | ⊦ restn(2, a ' + b ' + x) = x | A User Theorem |
| rest-two-01 | ⊦ restn(2, a ' + b ') = [] | A User Theorem |
| restN-all | ⊦ restn(# x, x) = [] | A User Theorem |
| restN-append | ⊦ n ≤ # x → restn(n, x + y) = restn(n, x) + y | A User Theorem |
| restN-dups | ⊦ ¬ dups(x) ∧ n ≤ # x → ¬ dups(restn(n, x)) | A User Theorem |
| restN-len | ⊦ restn(# x, x + y) = y | A User Theorem |
| restn-apprec | ⊦ restn(m, restn(n, x)) = restn(m + n, x) | A User Theorem |
| restn-at | ⊦ m + n < # x → restn(m, x)[n] = x[m + n] | A User Theorem |
| restn-empty | ⊦ n ≤ # x → (restn(n, x) = [] ↔ n = # x) | A User Theorem |
| restn-first-get | ⊦ n < # x → restn(n, x).first = x[n] | A User Theorem |
| restn-firstn | ⊦ m ≤ n ∧ m + n ≤ # x → restn(m, firstn(n, x)) = firstn(n - m, restn(m, x)) | A User Theorem |
| restn-firstn-better | ⊦ m ≤ n ∧ n ≤ # x → restn(m, firstn(n, x)) = firstn(n - m, restn(m, x)) | A User Theorem |
| restn-last | ⊦ n < # x → restn(n, x).last = x.last | A User Theorem |
| restn-less | ⊦ n < # x → restn(n, x) = x[n] + restn(n +1, x) | A User Theorem |
| restn-nonempty | ⊦ n < # x → restn(n, a ' + x) ≠ [] | A User Theorem |
| restn-nonempty-2 | ⊦ n < # x → restn(n, x) ≠ [] | A User Theorem |
| restn-prefix | ⊦ # x = n → restn(n, x + x0) = x0 | A User Theorem |
| restn-rest | ⊦ restn(n, x).rest = restn(n + 1, x) | A User Theorem |
| restn-restn | ⊦ m + n ≤ # x → restn(m, restn(n, x)) = restn(m + n, x) | A User Theorem |
| restn-size-last | ⊦ restn(# x, a ' + x) = (a ' + x).last ' | A User Theorem |
| rmdup-del1-del | ⊦ rmdup(x) -1l a = rmdup(x -l a) | A User Theorem |
| rmdup-last | ⊦ rmdup(x + a ') = rmdup(x -l a) + a ' | A User Theorem |
| rmpos-get | ⊦ n + 1 < # x ∧ m < # x → (x -1l m)[n] = (n < m ⊃ x[n];x[n + 1]) | A User Theorem |
| rmpos-in | ⊦ ¬ dups(x) ∧ n < # x → (a ∈ x -1l n ↔ a ≠ x[n] ∧ a ∈ x) | A User Theorem |
| rmpos-size | ⊦ n < # x → #(x -1l n) = # x - 1 | A User Theorem |
| rmtoobigpos | ⊦ # x ≤ n → x -1l n = x | A User Theorem |
| size-del-nodups | ⊦ ¬ dups(x) ∧ a ∈ x → #(x -l a) = # x - 1 | A User Theorem |
| size-rmdup-del | ⊦ a ∈ x → # rmdup(x -l a) = # rmdup(x) - 1 | A User Theorem |
| st | ⊦ (x -1l a) -1l b = (x -1l b) -1l a ↔ true | A User Theorem |
| sub-len | ⊦ n ≤ # x → # sublist(0, n, x) = n | A User Theorem |
| sub-len-01 | ⊦ n ≤ # x → # sublist(0, n, x + y) = n | A User Theorem |
| sub-rec | ⊦ sublist(m + 1, n, x) = sublist(m, n, x.rest) | A User Theorem |
| sub-rec-01 | m + n < # x ⊦ sublist(m + 1, n, x) = sublist(m, n, x.rest) | A User Theorem |
| sub-zero | ⊦ sublist(0, # x, x) = x | A User Theorem |
| sub-zerolen | ⊦ sublist(n, 0, x) = [] | A User Theorem |
| sub-zerolen-01 | ⊦ sublist(# x, 0, x) = [] | A User Theorem |
| sub-zerolen-02 | ⊦ n ≤ # x → sublist(n, 0, x) = [] | A User Theorem |
| sub-zerorec | ⊦ x ≠ [] → sublist(0, n + 1, x) = x.first + sublist(0, n, x.rest) | A User Theorem |
| sub-zerorec-01 | n < # x ⊦ sublist(0, n + 1, x) = x.first + sublist(0, n, x.rest) | A User Theorem |
| sub-zerozero | ⊦ sublist(0, 0, x) = [] | A User Theorem |
| sublist-all | ⊦ # x = n → sublist(0, n, x) = x | A User Theorem |
| sublist-append | ⊦ n + m ≤ # x → sublist(n, m, x + y) = sublist(n, m, x) | A User Theorem |
| sublist-append-01 | ⊦ # x ≤ n → sublist(n, m, x + y) = sublist(n - # x, m, y) | A User Theorem |
| sublist-append-01-01 | ⊦ # x ≤ n ∧ n + m ≤ # x + # y → sublist(n, m, x + y) = sublist(n - # x, m, y) | A User Theorem |
| sublist-append-02 | ⊦ # x ≤ m → sublist(0, m, x + y) = x + sublist(0, m - # x, y) | A User Theorem |
| sublist-append-02-01 | ⊦ # x ≤ m ∧ m ≤ # x + # y → sublist(0, m, x + y) = x + sublist(0, m - # x, y) | A User Theorem |
| sublist-append-03 | ⊦ sublist(0, # x, x + y) = x | A User Theorem |
| sublist-append-04 | ⊦ n + n0 + n1 ≤ # x → sublist(n, n0, x) + sublist(n + n0, n1, x) = sublist(n, n0 + n1, x) | A User Theorem |
| sublist-at | ⊦ n0 < n ∧ m + n ≤ # x → sublist(m, n, x)[n0] = x[m + n0] | A User Theorem |
| sublist-empty | ⊦ sublist(0, n, x) = [] ↔ n = 0 | A User Theorem |
| sublist-first-skip | ⊦ n2 ≤ # x ∧ n + n1 ≤ n2 → sublist(n, n1, firstn(n2, x)) = sublist(n, n1, x) | A User Theorem |
| sublist-firsteq | ⊦ sublist(0, n, x) = a ' + y ↔ n = # y + 1 ∧ x.first = a ∧ sublist(0, n -1, x.rest) = y | A User Theorem |
| sublist-good | ⊦ sublist(# x, # y, x + y + z) = y | A User Theorem |
| sublist-last | ⊦ m0 + n < # x → sublist(m0, n + 1, x).last = x[m0 + n] | A User Theorem |
| sublist-length | ⊦ m + n ≤ # x → # sublist(m, n, x) = n | A User Theorem |
| sublist-length-01 | ⊦ # x0 = n2 + n0 → # sublist(0, n0, x0) = n0 | A User Theorem |
| sublist-lenrec | ⊦ m + n < # x → sublist(m, n + 1, x) = sublist(m, n, x) + x[m + n] | A User Theorem |
| sublist-lenrec-01 | ⊦ n < # x → sublist(0, n + 1, x) = sublist(0, n, x) + x[n] | A User Theorem |
| sublist-mklist | ⊦ n + m ≤ m0 → sublist(n, m, mklist(a, m0)) = mklist(a, m) | A User Theorem |
| sublist-mklist-01 | ⊦ n + m ≤ m0 → sublist(n, m, mklist(a, m0) + x) = mklist(a, m) | A User Theorem |
| sublist-mklist-02 | ⊦ m ≤ m0 → sublist(0, m, mklist(a, m0)) = mklist(a, m) | A User Theorem |
| sublist-move | ⊦ n + m ≤ m0 ∧ n0 + m0 ≤ # x → sublist(n, m, sublist(n0, m0, x)) = sublist(n0 + n, m, x) | A User Theorem |
| sublist-not-empty | ⊦ m0 + n2 < # x → (¬ sublist(m0, n2 + 1, x) ≠ [] ↔ false) | A User Theorem |
| sublist-not-empty-01 | ⊦ n0 ≠ 0 → (¬ sublist(m0, n0, x) ≠ [] ↔ false) | A User Theorem |
| sublist-not-empty-02 | ⊦ ¬ sublist(n0, 1, x) ≠ [] ↔ false | A User Theorem |
| sublist-num | ⊦ sublist((* m), (* n), x) = firstn(n, restn(m, x)) | A User Theorem |
| sublist-num-01 | n ≠ 0 ⊦ sublist(0, (* n), a ' + x) = a ' + sublist(0, n -1, x) | A User Theorem |
| sublist-one | ⊦ m < # x → sublist(m, 1, x) = x[m] ' | A User Theorem |
| sublist-one-01 | ⊦ sublist(0, 1, a ') = a ' | A User Theorem |
| sublist-part | ⊦ # x = n0 + m0 → firstn(m0, x) + firstn(n0, restn(m0, x)) = x | A User Theorem |
| sublist-prefix | ⊦ n ≤ n1 ∧ n1 + m0 < # x → (¬ sublist(m0, n + 1, x) ⊑ sublist(m0, n1 + 1, x) ↔ false) | A User Theorem |
| sublist-rec | ⊦ x ≠ [] ∧ n ≠ 0 → sublist(0, n, x) = x.first ' + sublist(0, n -1, x.rest) | A User Theorem |
| sublist-rec-01 | n ≤ # x, n ≠ 0 ⊦ sublist(0, n, x) = x.first ' + sublist(0, n -1, x.rest) | A User Theorem |
| sublist-restn | ⊦ m + n + m0 < # x → sublist(m, n, restn(m0, x)) = sublist(m + m0, n, x) | A User Theorem |
| sublist-restn-01 | ⊦ m + n + m0 ≤ # x → sublist(m, n, restn(m0, x)) = sublist(m + m0, n, x) | A User Theorem |
| sublist-restn-02 | ⊦ n + m = # x → sublist(n, m, x) = restn(n, x) | A User Theorem |
| sublist-two-num | m1 ≤ # x, n + n1 ≤ m1 ⊦ sublist((* n), (* n1), sublist(0, (* m1), x)) = sublist(n, n1, x) | A User Theorem |
| sw | ⊦ (x -l a) -l b = (x -l b) -l a | A User Theorem |
| sw-01 | ⊦ (x -l a) -l b = (x -l b) -l a ↔ true | A User Theorem |
| sw-02 | ⊦ (x -1l a) -1l b = (x -1l b) -1l a | A User Theorem |
| weak-firstN-rec | ⊦ firstn(n + 1, a ' + x) = a + firstn(n, x) | A User Theorem |
| weak-restN-rec | ⊦ restn(n + 1, a ' + x) = restn(n, x) | A User Theorem |