Proof step 1 from proof to-unwind-end (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  σ to n + 1 ≠ (σ to n) + ⌜σ[n] '⌝ , ⌜n⌝ < # σ ⊦

Rule argument

Additional information

Proof step 2 from proof to-unwind-end (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ σ ≠ [] → (∃ a, σ0. σ = ⌜a '⌝ + σ0)

• Proof step 4:

  σ to n + 1 ≠ (σ to n) + ⌜σ[n] '⌝ , ⌜n⌝ < # σ, σ ≠ [] → (∃ a, σ0. σ = ⌜a '⌝ + σ0) ⊦

Rule argument

Additional information

Used terms: σ

Proof step 3 from proof to-unwind-end (previous step) (back to tree)

Lemma expand-cons

Proof step 4 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⌜a '⌝ + σ0 ≠ [], ⌜a '⌝ + (σ0 to n) ≠ (⌜a '⌝ + σ0 to n) + ⌜(⌜a '⌝ + σ0)[n] '⌝ , ¬ # σ0 < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: size-empty: ⊦ # [] = ⌜0⌝ ; to-succ-cons: ⊦ ⌜a '⌝ + σ to n + 1 = a + (σ to n); cons-append: ⊦ a + σ = ⌜a '⌝ + σ; size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ n < 0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)

Proof step 5 from proof to-unwind-end (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ n ≠ 0 → ⌜a '⌝ + σ to (* n) = ⌜a '⌝ + (σ to (n - 1))

• Proof step 7:

  ⌜a '⌝ + σ0 ≠ [], ⌜a '⌝ + (σ0 to n) ≠ (⌜a '⌝ + (σ0 to (n - 1))) + ⌜(⌜a '⌝ + σ0)[n] '⌝ , n ≠ 0, ¬ # σ0 < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: append-empty: ⊦ σ + [] = σ; to-zero: ⊦ σ to 0 = []; get-cons-zero: ⊦ (⌜a '⌝ + σ)[0] = a; empty-append: ⊦ [] + σ = σ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) Used terms: n, σ0, a

Proof step 6 from proof to-unwind-end (previous step) (back to tree)

Lemma cons-to-num

Proof step 7 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ⌜a '⌝ + σ0 ≠ [], n ≠ 0, σ0 to n ≠ (σ0 to (n - 1)) + ⌜(⌜a '⌝ + σ0)[n] '⌝ , ¬ # σ0 < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: append-cancel-l: ⊦ ⌜x⌝ + σ0 = ⌜x⌝ + σ1 ↔ σ0 = σ1; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2;

Proof step 8 from proof to-unwind-end (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  n = m + 1, ⌜a '⌝ + σ0 ≠ [], n ≠ 0, σ0 to n ≠ (σ0 to m) + ⌜(⌜a '⌝ + σ0)[n] '⌝ , ¬ # σ0 < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 9 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ⌜a '⌝ + σ0 ≠ [], σ0 to m + 1 ≠ (σ0 to m) + ⌜σ0[m] '⌝ , ⌜m⌝ < # σ0 ⊦

Rule argument

Additional information

Used simplifier rules: get-cons-succ: ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-succ: ⊦ # σ < ⌜n⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < # σ; add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 10 from proof to-unwind-end (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 11:

  ⌜a '⌝ + ⌜x⌝ ≠ [], ⌜x⌝ to m + 1 ≠ (⌜x⌝ to m) + ⌜⌜x⌝ [m] '⌝ , ⌜m⌝ < # ⌜x⌝ ⊦

• Proof step 14:

  ⌜a '⌝ + ⌜nf⌝ ≠ [], ⌜nf⌝ to m + 1 ≠ (⌜nf⌝ to m) + ⌜⌜nf⌝ [m] '⌝ , ⌜m⌝ < # ⌜nf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 11 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (x to m) + x[m] ' ≠ x to m + 1, ⌜a '⌝ + ⌜x⌝ ≠ [], x ≠ [], m < # x ⊦

Rule argument

Additional information

Used simplifier rules: to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; eq-stream-to-list-2-1: ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)

Proof step 12 from proof to-unwind-end (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  m < # x ⊦ x to m + 1 = (x to m) + x[m] '

Rule argument

Additional information

Used terms: m, x

Proof step 13 from proof to-unwind-end (previous step) (back to tree)

Lemma to-unwind-end-fin

Proof step 14 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ⌜a '⌝ + ⌜nf⌝ ≠ [], (nf to m) + nf(m) ' ≠ nf to m + 1 ⊦

Rule argument

Additional information

Used simplifier rules: to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); eq-stream-to-list-2-1: ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-inf: ⊦ # ⌜nf⌝ = ∞; ⊦ ⌜m⌝ < ∞; (s)

Proof step 15 from proof to-unwind-end (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ ⌜a '⌝ + ⌜nf⌝ = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝

• Proof step 17:

  (nf to m) + nf(m) ' ≠ nf to m + 1, ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝ ≠ [] ⊦

Rule argument

Additional information

Used terms: nf, a

Proof step 16 from proof to-unwind-end (previous step) (back to tree)

Lemma one-inf

Proof step 17 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (nf to m) + nf(m) ' ≠ nf to m + 1 ⊦

Rule argument

Additional information

Used simplifier rules: fun-nonempty: ⊦ [] ≠ ⌜nf⌝ ; ⊦ n -1 = n - 1; (s)

Proof step 18 from proof to-unwind-end (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 19:

  (nf to m0 +1) + nf(m0 +1) ' ≠ nf to m0 +1 + 1, ∀ nf. (nf to m0) + nf(m0) ' = nf to m0 + 1 ⊦

Rule argument

Additional information

Used simplifier rules: to-zero-nf: ⊦ nf to 0 = []; to-inf-one: ⊦ nf to 1 = nf(0) '; nat freely generated by 0, +1;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a ' = a0 ' ↔ a = a0; (s)

Proof step 19 from proof to-unwind-end (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  ((λ n. nf(n + 1)) to m0) + nf(m0 + 1) ' = (λ n. nf(n + 1)) to m0 + 1, (nf to m0 +1) + nf(m0 +1) ' ≠ nf to m0 +1 + 1 ⊦

Rule argument

Additional information

Used terms: λ n. nf(n + 1)

Proof step 20 from proof to-unwind-end (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ nf to n + 1 = nf(0) + ((λ n. nf(n + 1)) to n)

• Proof step 22:

  ((λ n. nf(n + 1)) to m0) + nf(m0 + 1) ' = (λ n. nf(n + 1)) to m0 + 1, (nf to m0 +1) + nf(m0 +1) ' ≠ nf(0) + ((λ n. nf(n + 1)) to m0 +1) ⊦

Rule argument

Additional information

Used terms: m0 +1, nf

Proof step 21 from proof to-unwind-end (previous step) (back to tree)

Lemma to-succ-nf

Proof step 22 from proof to-unwind-end (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ((λ n. nf(n + 1)) to m0) + nf(m0 + 1) ' = (λ n. nf(n + 1)) to m0 + 1, (nf to m0 + 1) + nf(m0 + 1) ' ≠ nf(0) ' + ((λ n. nf(n + 1)) to m0 + 1), nf(m0 + 1) ∈ (λ n. nf(n + 1)) to m0 + 1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s) ⊦ m +1 = m + 1; (s)

Proof step 23 from proof to-unwind-end (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ nf to n + 1 = nf(0) + ((λ n. nf(n + 1)) to n)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ a ' + x = a ' + y ↔ x = y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: m0, nf

Proof step 24 from proof to-unwind-end (previous step) (back to tree)

Lemma to-succ-nf