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: |
|---|---|---|
| toinf-fin | ⊦ σ to∞ ⌜n⌝ = σ to n | An Axiom |
| to-inf | ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ | An Axiom |
| hd-fin | ⊦ hd(⌜a + x⌝ ) = a | An Axiom |
| tl-fin | ⊦ tl(⌜a + x⌝ ) = ⌜x⌝ | An Axiom |
| sel-fin | ⊦ ⌜x⌝ [n] = x[n] | An Axiom |
| sel-inf | ⊦ ⌜nf⌝ [n] = nf(n) | An Axiom |
| modify-fin | ⊦ ⌜x⌝ [n, a] = ⌜x[n, a]⌝ | An Axiom |
| modify-inf | ⊦ ⌜nf⌝ [n, a] = ⌜λ m. (m = n ⊃ a;nf(m))⌝ | An Axiom |
| empty | ⊦ ⌜[]⌝ = [] | An Axiom |
| cons-fin | ⊦ ⌜a + x⌝ = a + ⌜x⌝ | An Axiom |
| cons-inf | ⊦ a + ⌜nf⌝ = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝ | An Axiom |
| append-finfin | ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ | An Axiom |
| append-fininf | ⊦ ⌜x⌝ + ⌜nf⌝ = ⌜λ n. (n < # x ⊃ x[n];nf(n - # x))⌝ | An Axiom |
| append-inf | ⊦ ⌜nf⌝ + σ = ⌜nf⌝ | An Axiom |
| size-inf | ⊦ # ⌜nf⌝ = ∞ | An Axiom |
| size-fin | ⊦ # ⌜x⌝ = ⌜# x⌝ | An Axiom |
| prefix-def | ⊦ σ1 ≤ σ2 ↔ (∃ σ. σ1 + σ = σ2) | An Axiom |
| tl-inf | ⊦ tl(⌜nf⌝ ) = ⌜λ n. nf(n +1)⌝ | An Axiom |
| hd-inf | ⊦ hd(⌜nf⌝ ) = nf(0) | An Axiom |
| from-nf | ⊦ nf from n = (λ m. nf(n + m)) | An Axiom |
| to-succ-nf | ⊦ nf to n + 1 = nf(0) + ((λ n. nf(n + 1)) to n) | An Axiom |
| to-zero-nf | ⊦ nf to 0 = [] | An Axiom |
| to-succ-cons-l | ⊦ a + x to n + 1 = a + (x to n) | An Axiom |
| to-zero-l | ⊦ x to 0 = [] | An Axiom |
| from-succ-cons-l | ⊦ a + x from n + 1 = x from n | An Axiom |
| from-zero-l | ⊦ x from 0 = x | An Axiom |
| from-inf | ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ | An Axiom |
| from-fin | ⊦ ⌜x⌝ from n = ⌜x from n⌝ | An Axiom |
| to-fin | ⊦ ⌜x⌝ to n = ⌜x to n⌝ | An Axiom |
| toinf-inf | ⊦ σ to∞ ∞ = σ | An Axiom |
| append-assoc | ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2 | A User Theorem |
| append-cancel-l | ⊦ ⌜x⌝ + σ0 = ⌜x⌝ + σ1 ↔ σ0 = σ1 | A User Theorem |
| append-cancel-l-02 | ⊦ σ0 + σ = σ0 ↔ ¬ ¬(σ = [] ∨ ¬ finp(σ0)) | A User Theorem |
| append-cancel-r-01 | ⊦ finp(σ) → (⌜x⌝ + σ = ⌜y⌝ + σ ↔ ⌜x⌝ = ⌜y⌝ ) | A User Theorem |
| append-cancel-r-02 | finp(σ) ⊦ σ0 + σ = σ ↔ σ0 = [] | A User Theorem |
| append-cancel-r-04 | ⊦ finp(σ) → (⌜z⌝ = σ + ⌜z⌝ ↔ σ = []) | A User Theorem |
| append-cut1 | ⊦ σ + σ1 = σ + σ2 ↔ σ1 = σ2 ∨ # σ = ∞ | A User Theorem |
| append-empty | ⊦ σ + [] = σ | A User Theorem |
| append-empty-01 | ⊦ σ0 + σ1 = [] ↔ σ0 = [] ∧ σ1 = [] | A User Theorem |
| append-eq-inf | ⊦ ⌜nf⌝ = σ + ⌜x⌝ ↔ ⌜nf⌝ = σ | A User Theorem |
| append-extract-list | finp(σ) ⊦ (⌜x⌝ + σ).l = x + σ.l | A User Theorem |
| append-extract-list-2 | finp(σ), finp(σ0) ⊦ (σ0 + σ).l = σ0.l + σ.l | A User Theorem |
| append-from-addsize | ⊦ x1 + x0 from n + # x1 = x0 from n | A User Theorem |
| append-from-addsize-01 | ⊦ ⌜x⌝ + σ from m + # x = σ from m | A User Theorem |
| append-from-ge-01 | ⊦ # x ≤ m → ⌜x⌝ + σ from m = σ from (m - # x) | A User Theorem |
| append-from-ge-02 | ⊦ ¬ ⌜m⌝ < # σ0 → σ0 + σ from m = σ from (m - (# σ0).n) | A User Theorem |
| append-from-gr-01 | ⊦ # x < m → ⌜x⌝ + σ from m = σ from (m - # x) | A User Theorem |
| append-from-gr-02 | ⊦ # σ0 < ⌜m⌝ → σ0 + σ from m = σ from (m - (# σ0).n) | A User Theorem |
| append-from-gt | ⊦ # x < n → x + y from n = y from (n - # x) | A User Theorem |
| append-from-le | ⊦ n ≤ # x → x + y from n = (x from n) + y | A User Theorem |
| append-from-le-01 | ⊦ m ≤ # x → ⌜x⌝ + σ from m = ⌜x from m⌝ + σ | A User Theorem |
| append-from-size | ⊦ x + y from # x = y | A User Theorem |
| append-from-size-01 | ⊦ ⌜x⌝ + σ from # x = σ | A User Theorem |
| append-notsmallersize1 | ⊦ σ + σ0 = σ1 → (¬ ¬ # σ1 < # σ ↔ false) | A User Theorem |
| append-notsmallersize2 | ⊦ σ + σ0 = σ1 → (¬ ¬ # σ1 < # σ0 ↔ false) | A User Theorem |
| append-split | ⊦ finp(σ) ∧ # σ = # σ1 → (σ + σ0 = σ1 + σ2 ↔ σ = σ1 ∧ σ0 = σ2) | A User Theorem |
| append-to-addsize | ⊦ x + y to n + # x = x + (y to n) | A User Theorem |
| append-to-addsize-01 | ⊦ ⌜x⌝ + σ to m + # x = ⌜x⌝ + (σ to m) | A User Theorem |
| append-to-gr | ⊦ # x < n → x + y to n = x + (y to (n - # x)) | A User Theorem |
| append-to-gr-01 | ⊦ # x < m → ⌜x⌝ + σ to m = ⌜x⌝ + (σ to (m - # x)) | A User Theorem |
| append-to-le | ⊦ n ≤ # x → x + y to n = x to n | A User Theorem |
| append-to-le-01 | ⊦ m ≤ # x → ⌜x⌝ + σ to m = ⌜x to m⌝ | A User Theorem |
| append-to-ls | ⊦ ¬ # σ < ⌜n⌝ → σ + σ0 to n = σ to n | A User Theorem |
| append-to-size | ⊦ x + y to # x = x | A User Theorem |
| append-to-size-01 | ⊦ ⌜x⌝ + σ to # x = ⌜x⌝ | A User Theorem |
| append-toinf-ls | ⊦ ¬ # σ < n∞ → σ + σ0 to∞ n∞ = σ to∞ n∞ | A User Theorem |
| appendend-equal | ⊦ σ + σ0 = σ ↔ ¬ ¬(σ0 = [] ∨ # σ = ∞) | A User Theorem |
| cons-append | ⊦ a + σ = ⌜a '⌝ + σ | A User Theorem |
| cons-empty | ⊦ ⌜a '⌝ + σ ≠ [] | A User Theorem |
| cons-eq | ⊦ ⌜a '⌝ + σ = ⌜a0 '⌝ + σ0 ↔ a = a0 ∧ σ = σ0 | A User Theorem |
| cons-eq-inf | ⊦ ⌜nf⌝ = a0 + σ ↔ nf(0) = a0 ∧ ⌜λ n. nf(n + 1)⌝ = σ | A User Theorem |
| cons-extract-list | finp(σ) ⊦ (⌜a '⌝ + σ).l = a ' + σ.l | A User Theorem |
| cons-from-addnum | ⊦ n ≠ 0 → ⌜a '⌝ + σ from (* n) + m = σ from (n - 1) + m | A User Theorem |
| cons-from-num | ⊦ n ≠ 0 → ⌜a '⌝ + σ from (* n) = σ from (n - 1) | A User Theorem |
| cons-to-addnum | ⊦ n ≠ 0 → ⌜a '⌝ + σ to (* n) + m = ⌜a '⌝ + (σ to (n - 1) + m) | A User Theorem |
| cons-to-num | ⊦ n ≠ 0 → ⌜a '⌝ + σ to (* n) = ⌜a '⌝ + (σ to (n - 1)) | A User Theorem |
| constrrew | ⊦ ⌜a + x⌝ = ⌜a '⌝ + ⌜x⌝ | A User Theorem |
| contractinf-from1 | ⊦ ⌜nf(0) '⌝ + ⌜nf from 1⌝ = ⌜nf⌝ | A User Theorem |
| contractinf-tl | ⊦ ⌜nf(0) '⌝ + tl(⌜nf⌝ ) = ⌜nf⌝ | A User Theorem |
| elim-fromto | ⊦ ¬ # σ < ⌜n⌝ → (σ0 = σ to n ∧ σ1 = σ from n ↔ σ = σ0 + σ1 ∧ # σ0 = ⌜n⌝ ) | A User Theorem |
| elim-fromto-fin | ⊦ ¬ # x < n → (x0 = x to n ∧ x1 = x from n ↔ x = x0 + x1 ∧ # x0 = n) | A User Theorem |
| elim-fromto-inf | ⊦ x0 = nf to n ∧ nf0 = nf from n ↔ nf = (⌜x0⌝ + ⌜nf0⌝ ).f ∧ # x0 = n | A User Theorem |
| elim-hd-tl | ⊦ σ ≠ [] → (a = hd(σ) ∧ σ0 = tl(σ) ↔ σ = a + σ0) | A User Theorem |
| empty-append | ⊦ [] + σ = σ | A User Theorem |
| empty-leq | ⊦ σ ≤ [] ↔ σ = [] | A User Theorem |
| eq-stream-to-list-2-1 | ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z | A User Theorem |
| eq-stream-to-list-2-2 | ⊦ ⌜x⌝ + ⌜y⌝ = ⌜x0⌝ + ⌜z⌝ ↔ x + y = x0 + z | A User Theorem |
| eq-stream-to-list-3-1 | ⊦ ⌜x⌝ + ⌜y⌝ + ⌜z⌝ = ⌜x0⌝ ↔ x + y + z = x0 | A User Theorem |
| eq-stream-to-list-3-2 | ⊦ ⌜x1⌝ + ⌜x⌝ + ⌜y⌝ = ⌜x0⌝ + ⌜z⌝ ↔ x1 + x + y = x0 + z | A User Theorem |
| eq-stream-to-list-3-3 | ⊦ ⌜x1⌝ + ⌜x⌝ + ⌜y⌝ = ⌜x2⌝ + ⌜x0⌝ + ⌜z⌝ ↔ x1 + x + y = x2 + x0 + z | A User Theorem |
| expand-cons | ⊦ σ ≠ [] → (∃ a, σ0. σ = ⌜a '⌝ + σ0) | A User Theorem |
| extensionality | ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0[n] = σ1[n]) | A User Theorem |
| extensionality-to | ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ¬ # σ0 < ⌜n⌝ → σ0 to n = σ1 to n) | A User Theorem |
| extract-empty | ⊦ [].l = [] | A User Theorem |
| fin-empty | ⊦ ⌜x⌝ = [] ↔ x = [] | A User Theorem |
| fin-finlen-tolen | ⊦ # x = n → x to n = x | A User Theorem |
| fin-neq-inf | ⊦ a + ⌜nf⌝ ≠ ⌜x⌝ | A User Theorem |
| fin-size-from | ⊦ ⌜n⌝ < # σ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝ | A User Theorem |
| fin-size-from2 | ⊦ ¬ # σ < ⌜n⌝ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝ | A User Theorem |
| fin-to | ⊦ finp(σ to m) | A User Theorem |
| fin-toinf | ⊦ finp(σ to∞ n∞) ↔ n∞ ≠ ∞ ∨ finp(σ) | A User Theorem |
| finlen-tolen | ⊦ # σ = ⌜n⌝ → σ to n = σ | A User Theorem |
| finp-append-01 | ⊦ finp(σ) ∧ finp(σ1) → finp(σ + σ1) | A User Theorem |
| finp-append-02 | ⊦ finp(⌜x⌝ + σ) ↔ finp(σ) | A User Theorem |
| finp-empty | ⊦ finp([]) | A User Theorem |
| finp-infto | ⊦ finp(⌜nf to n⌝ ) | A User Theorem |
| finp-to | ¬ # σ < ⌜n⌝ ⊦ finp(σ to n) | A User Theorem |
| from-all | ⊦ x from # x = [] | A User Theorem |
| from-append-add | ⊦ ¬ # σ < ⌜n⌝ ∧ ¬ # σ0 < ⌜n1⌝ → (σ to n) + σ0 from n1 + n = σ0 from n1 | A User Theorem |
| from-append-tofrom | ⊦ ¬ # σ < ⌜n + n1⌝ → (σ to n) + ((σ from n) to n1) = σ to n + n1 | A User Theorem |
| from-append-toinffrom | ⊦ ¬ # σ < ⌜n⌝ + n∞1 → (σ to n) + ((σ from n) to∞ n∞1) = σ to∞ ⌜n⌝ + n∞1 | A User Theorem |
| from-appfin | ⊦ ⌜x⌝ + ⌜y⌝ from n = ⌜x + y from n⌝ | A User Theorem |
| from-cons-one | ⊦ ⌜a '⌝ + σ from 1 = σ | A User Theorem |
| from-cons-one-fin | ⊦ a ' + x from 1 = x | A User Theorem |
| from-from | ⊦ ¬ # σ < ⌜m + n⌝ → σ from m from n = σ from m + n | A User Theorem |
| from-from-inf | ⊦ nf from m from n = nf from m + n | A User Theorem |
| from-infto-exchange | ⊦ ¬ # σ < ⌜m⌝ + n∞ → (σ to∞ ⌜m⌝ + n∞) from m = (σ from m) to∞ n∞ | A User Theorem |
| from-nf-zero | ⊦ nf from 0 = nf | A User Theorem |
| from-succ | ⊦ ⌜n⌝ < # σ → σ from n = σ[n] + (σ from n + 1) | A User Theorem |
| from-succ-cons | ⊦ ⌜a '⌝ + σ from n + 1 = σ from n | A User Theorem |
| from-succ-cons-l-lem | ⊦ a ' + x from n + 1 = x from n | A User Theorem |
| from-to-exchange | ⊦ ¬ # σ < ⌜m⌝ + ⌜n⌝ → (σ to m + n) from m = (σ from m) to n | A User Theorem |
| from-zero | ⊦ σ from 0 = σ | A User Theorem |
| fun-nonempty | ⊦ [] ≠ ⌜nf⌝ | A User Theorem |
| get-append-ls | ⊦ ⌜m⌝ < # σ → (σ + σ1)[m] = σ[m] | A User Theorem |
| get-append-notls | ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)[m] = σ1[m - (# σ).n] | A User Theorem |
| get-append2-fin | ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m] | A User Theorem |
| get-append3-fin | ⊦ (⌜x⌝ + ⌜x0⌝ + ⌜x1⌝ )[m] = (x + x0 + x1)[m] | A User Theorem |
| get-cons-num | n ≠ 0 ⊦ (⌜a '⌝ + σ)[(* n)] = σ[n - 1] | A User Theorem |
| get-cons-succ | ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n] | A User Theorem |
| get-cons-zero | ⊦ (⌜a '⌝ + σ)[0] = a | A User Theorem |
| get-finto | ¬ # x < n, m < n ⊦ (x to n)[m] = x[m] | A User Theorem |
| get-fintoinf | ¬ ⌜# x⌝ < n∞, ⌜m⌝ < n∞ ⊦ (⌜x⌝ to∞ n∞)[m] = x[m] | A User Theorem |
| get-from | ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m] | A User Theorem |
| get-from-01 | m + m0 < # x ⊦ (x from m)[m0] = x[m + m0] | A User Theorem |
| get-from-inf | ⊦ ((nf from n))(m) = nf(m + n) | A User Theorem |
| get-from-inf-zero | ⊦ ((nf from n))(0) = nf(n) | A User Theorem |
| get-from-zero | ⊦ ⌜n⌝ < # σ → (σ from n)[0] = σ[n] | A User Theorem |
| get-infto | m < n ⊦ (nf to n)[m] = nf(m) | A User Theorem |
| get-inftoinf | ⌜m⌝ < n∞ ⊦ (⌜nf⌝ to∞ n∞)[m] = nf(m) | A User Theorem |
| get-to | m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m] | A User Theorem |
| get-to-02 | m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n).l[m] = σ[m] | A User Theorem |
| get-toinf | ⌜m⌝ < n∞, ¬ # σ < n∞ ⊦ (σ to∞ n∞)[m] = σ[m] | A User Theorem |
| hd-fin-lem | ⊦ hd(⌜a '⌝ + ⌜x⌝ ) = a | A User Theorem |
| hd-lem | ⊦ hd(⌜a '⌝ + σ) = a | A User Theorem |
| hd-one | ⊦ hd(⌜a '⌝ ) = a | A User Theorem |
| inf-not-to | ⊦ ⌜nf⌝ ≠ σ to n | A User Theorem |
| inf-not-toinf-exceptinf | ⊦ ⌜nf⌝ = σ to∞ n∞ ↔ ¬ ¬(n∞ = ∞ ∧ ⌜nf⌝ = σ) | A User Theorem |
| inf-size-from | ⊦ # σ = ∞ → #(σ from n) = ∞ | A User Theorem |
| inf-size-to | ⊦ # ⌜nf to n⌝ = ⌜n⌝ | A User Theorem |
| intrace-expand | ⊦ ⌜nf⌝ = nf(0) + ⌜λ n. nf(n + 1)⌝ | A User Theorem |
| length-from | ¬ # x < n ⊦ #(x from n) = # x - n | A User Theorem |
| length-to | ¬ # x < n ⊦ #(x to n) = n | A User Theorem |
| leq-append-both | ⊦ ⌜x⌝ + σ1 ≤ ⌜x⌝ + σ2 ↔ σ1 ≤ σ2 | A User Theorem |
| leq-append-left | ⊦ σ0 + σ1 ≤ σ → (¬ σ0 ≤ σ ↔ false) | A User Theorem |
| leq-append-right | ⊦ σ1 ≤ σ1 + σ2 | A User Theorem |
| leq-empty | ⊦ [] ≤ σ | A User Theorem |
| leq-prefix | ⊦ σ1 ≤ σ2 → σ1 = σ2 ∨ (∃ n. ⌜n⌝ < # σ2 ∧ σ2 to n = σ1) | A User Theorem |
| leq-refl | ⊦ σ ≤ σ | A User Theorem |
| leq-symm | ⊦ σ1 ≤ σ2 ∧ σ2 ≤ σ1 → σ1 = σ2 | A User Theorem |
| leq-symm-2 | ⊦ σ1 ≤ σ2 → (σ2 ≤ σ1 ↔ σ1 = σ2) | A User Theorem |
| leq-trans | ⊦ σ ≤ σ1 ∧ σ1 ≤ σ2 → σ ≤ σ2 | A User Theorem |
| less-size-from | ⌜n⌝ < # σ ⊦ ⌜n0⌝ < #(σ from n) ↔ ⌜n0 + n⌝ < # σ | A User Theorem |
| lslen-fromnotempty | ⊦ ⌜n⌝ < # σ → (σ from n = [] ↔ false) | A User Theorem |
| lslen-fromnotempty-list | ⊦ n < # x → (x from n = [] ↔ false) | A User Theorem |
| neq-fin-inf-01 | ⊦ ⌜x⌝ ≠ σ + ⌜nf0⌝ | A User Theorem |
| neq-fin-inf-02 | ⊦ σ0 + ⌜x⌝ = σ + ⌜nf0⌝ ↔ σ0 = σ + ⌜nf0⌝ | A User Theorem |
| neq-fin-inf-03 | ⊦ σ0 + ⌜x⌝ = ⌜nf0⌝ ↔ σ0 = ⌜nf0⌝ | A User Theorem |
| nlslen-lslensn-eqlensn | ⊦ ⌜n⌝ < # σ ∧ ¬ ⌜n⌝ + ⌜1⌝ < # σ → # σ = ⌜n⌝ + ⌜1⌝ | A User Theorem |
| notfin-sizeinf | ⊦ ¬ finp(σ) → # σ = ∞ | A User Theorem |
| one-inf | ⊦ ⌜a '⌝ + ⌜nf⌝ = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝ | A User Theorem |
| single-to-one | ⊦ a ' to 1 = a ' | A User Theorem |
| size-append | ⊦ #(σ + σ1) = # σ + # σ1 | A User Theorem |
| size-empty | ⊦ # [] = ⌜0⌝ | A User Theorem |
| size-empty-equiv | ⊦ # σ = ⌜0⌝ ↔ σ = [] | A User Theorem |
| size-from-inf | ⊦ #(⌜nf⌝ from n) = ∞ | A User Theorem |
| size-from-less | ⊦ ¬ # σ < ⌜n⌝ → (#(σ from n) < ⌜n0⌝ ↔ # σ < ⌜n + n0⌝ ) | A User Theorem |
| size-inf-to | ⊦ #(nf to n) = n | A User Theorem |
| size-inf-toinf | ⊦ #(⌜nf⌝ to∞ n∞) = n∞ | A User Theorem |
| size-succ | ⊦ # σ < ⌜n⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < # σ | A User Theorem |
| size-to | ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ | A User Theorem |
| size-to-02 | ¬ # σ < ⌜n⌝ ⊦ # (σ to n).l = n | A User Theorem |
| size-toinf | ¬ # σ < n∞ ⊦ #(σ to∞ n∞) = n∞ | A User Theorem |
| stream-empty | ⊦ [] = σ1 + σ2 ↔ σ1 = [] ∧ σ2 = [] | A User Theorem |
| swap-from-to | ⊦ ¬ # σ < ⌜m⌝ + ⌜n⌝ → (σ from m) to n = (σ to m + n) from m | A User Theorem |
| swap-inf-from-to | ⊦ (nf from m) to n = (nf to m + n) from m | A User Theorem |
| swap-inf-to-from | ⊦ m ≤ n → (nf to n) from m = (nf from m) to (n - m) | A User Theorem |
| swap-inf-to-from-app | ⊦ m ≤ n → ⌜nf to n⌝ + σ0 from m = ⌜(nf from m) to (n - m)⌝ + σ0 | A User Theorem |
| swap-to-from | ⊦ m ≤ n ∧ ¬ # σ < ⌜n⌝ → (σ to n) from m = (σ from m) to (n - m) | A User Theorem |
| swap-to-from-app | ⊦ m ≤ n ∧ ¬ # σ < ⌜n⌝ → (σ to n) + σ0 from m = ((σ from m) to (n - m)) + σ0 | A User Theorem |
| tl-fin-1 | ⊦ tl(⌜a ' + x⌝ ) = ⌜x⌝ | A User Theorem |
| tl-fin-lem | ⊦ tl(⌜a '⌝ + ⌜x⌝ ) = ⌜x⌝ | A User Theorem |
| tl-inf-1 | ⊦ tl(a + ⌜nf⌝ ) = ⌜nf⌝ | A User Theorem |
| tl-lem | ⊦ tl(⌜a '⌝ + σ) = σ | A User Theorem |
| tl-one | ⊦ tl(⌜a '⌝ ) = [] | A User Theorem |
| to-all | ⊦ x to # x = x | A User Theorem |
| to-append-add | ⊦ ¬ # σ < ⌜n⌝ ∧ ¬ # σ0 < ⌜n1⌝ → (σ to n) + σ0 to n1 + n = (σ to n) + (σ0 to n1) | A User Theorem |
| to-appfin | ⊦ ⌜x⌝ + ⌜y⌝ to n = ⌜x + y to n⌝ | A User Theorem |
| to-attach | ⊦ ⌜x + a '⌝ to # x = ⌜x⌝ | A User Theorem |
| to-empty | ⊦ ⌜n⌝ < # σ → (σ to n = [] ↔ n = 0) | A User Theorem |
| to-empty-fin | ⊦ n < # x → (x to n = [] ↔ n = 0) | A User Theorem |
| to-empty-fin2 | ⊦ n ≤ # x → (x to n = [] ↔ n = 0) | A User Theorem |
| to-empty-inf | ⊦ nf to n = [] ↔ n = 0 | A User Theorem |
| to-empty2 | ⊦ ¬ # σ < ⌜n⌝ → (σ to n = [] ↔ n = 0) | A User Theorem |
| to-empty3 | ⊦ ⌜n⌝ < # σ → σ to n + 1 ≠ [] | A User Theorem |
| to-empty4 | ⊦ σ ≠ [] → σ to 1 ≠ [] | A User Theorem |
| to-from-01 | ⌜n⌝ < # σ ⊦ (σ to n) from n = [] | A User Theorem |
| to-inf-one | ⊦ nf to 1 = nf(0) ' | A User Theorem |
| to-plus-from | ⊦ ¬ # σ < ⌜n⌝ → (σ to n) + (σ from n) = σ | A User Theorem |
| to-plus-from-fin | ⊦ n ≤ # x → (x to n) + (x from n) = x | A User Theorem |
| to-plus-from-fin-simp | ⊦ ¬ # x < n → ((x to n) + (x from n) ≠ x ↔ false) | A User Theorem |
| to-plus-from-inf | ⊦ ⌜nf to n⌝ + ⌜nf from n⌝ = ⌜nf⌝ | A User Theorem |
| to-plus-from-inf-simp | ⊦ ⌜nf to n⌝ + ⌜nf from n⌝ ≠ ⌜nf⌝ ↔ false | A User Theorem |
| to-plus-from-simp | ¬ # σ < ⌜n⌝ ⊦ (σ to n) + (σ from n) ≠ σ ↔ false | A User Theorem |
| to-succ-cons | ⊦ ⌜a '⌝ + σ to n + 1 = a + (σ to n) | A User Theorem |
| to-succ-cons-l-lem | ⊦ a ' + x to n + 1 = a + (x to n) | A User Theorem |
| to-to-eq | ¬ # σ < ⌜n⌝ ⊦ σ to n to n = σ to n | A User Theorem |
| to-to-eq-inf | ⊦ (nf to n) to n = nf to n | A User Theorem |
| to-to-leq | ¬ # σ < ⌜n⌝ ⊦ m ≤ n → σ to n to m = σ to m | A User Theorem |
| to-to-leq-inf | ⊦ m ≤ n → (nf to n) to m = nf to m | A User Theorem |
| to-to-ls | ¬ # σ < ⌜n⌝ ⊦ m < n → σ to n to m = σ to m | A User Theorem |
| to-unwind-begin | ⌜n⌝ < # σ ⊦ σ to n + 1 = σ[0] + (tl(σ) to n) | A User Theorem |
| to-unwind-begin-fin | m < # x ⊦ x to m + 1 = x.first + (x.rest to m) | A User Theorem |
| to-unwind-end | ⌜n⌝ < # σ ⊦ σ to n + 1 = (σ to n) + ⌜σ[n] '⌝ | A User Theorem |
| to-unwind-end-fin | m < # x ⊦ x to m + 1 = (x to m) + x[m] ' | A User Theorem |
| to-unwind-end-inf | ⊦ nf to m + 1 = (nf to m) + nf(m) ' | A User Theorem |
| to-zero | ⊦ σ to 0 = [] | A User Theorem |
| toinf-add | ⊦ σ to∞ ⌜n⌝ + ⌜m⌝ = σ to n + m | A User Theorem |
| toinf-empty | ⊦ n∞ < # σ → (σ to∞ n∞ = [] ↔ n∞ = ⌜0⌝ ) | A User Theorem |
| toinf-empty-inf | ⊦ ⌜nf⌝ to∞ n∞ = [] ↔ n∞ = ⌜0⌝ | A User Theorem |
| toinf-empty2 | ⊦ ¬ # σ < n∞ → (σ to∞ n∞ = [] ↔ n∞ = ⌜0⌝ ) | A User Theorem |
| toinf-empty3 | ⊦ n∞ < # σ → σ to∞ n∞ + ⌜1⌝ ≠ [] | A User Theorem |
| toinf-to-eq | ¬ # σ < n∞ ⊦ σ to∞ n∞ to∞ n∞ = σ to∞ n∞ | A User Theorem |
| toinf-to-eq-inf | ⊦ ⌜nf⌝ to∞ n∞ to∞ n∞ = ⌜nf⌝ to∞ n∞ | A User Theorem |
| toinf-to-leq | ¬ # σ < n∞ ⊦ ¬ n∞ < ⌜m⌝ → (σ to∞ n∞) to m = σ to m | A User Theorem |
| toinf-to-leq-inf | ⊦ ¬ n∞ < ⌜m⌝ → (⌜nf⌝ to∞ n∞) to m = ⌜nf to m⌝ | A User Theorem |
| toinf-to-ls | ¬ # σ < n∞ ⊦ ⌜m⌝ < n∞ → (σ to∞ n∞) to m = σ to m | A User Theorem |
| toinflen | ⊦ # σ = n∞ → σ to∞ n∞ = σ | A User Theorem |
| toinfto-append-add | ⊦ ¬ # σ < n∞ ∧ ¬ # σ0 < ⌜n1⌝ → (σ to∞ n∞) + σ0 to∞ ⌜n1⌝ + n∞ = (σ to∞ n∞) + (σ0 to n1) | A User Theorem |
| toinftoinf-append-add | ⊦ ¬ # σ < n∞ ∧ ¬ # σ0 < n∞1 → (σ to∞ n∞) + σ0 to∞ n∞1 + n∞ = (σ to∞ n∞) + (σ0 to∞ n∞1) | A User Theorem |
| ton-fromn | ⊦ ¬ # σ < ⌜n⌝ → (σ to n) from n = [] | A User Theorem |
| ton-fromn-fin | ⊦ ¬ # x < n → (x to n) from n = [] | A User Theorem |
| ton-fromn-inf | ⊦ (nf to n) from n = [] | A User Theorem |
| toone-cons | ⊦ ⌜a '⌝ + σ to 1 = ⌜a '⌝ | A User Theorem |
| toone-cons-fin | ⊦ a ' + y to 1 = a ' | A User Theorem |
| toone-equal | σ ≠ [] ⊦ σ to 1 = ⌜a '⌝ ↔ σ[0] = a | A User Theorem |
| toone-one | ⊦ ⌜a '⌝ to 1 = ⌜a '⌝ | A User Theorem |
| zero-len | ⊦ ⌜0⌝ < # σ ↔ σ ≠ [] | A User Theorem |