Proof step 1 from proof from-append-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (σ to n) + σ0 from n1 + n ≠ σ0 from n1, ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Proof step 2 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (σ to n) + σ0 from n1 + n ≠ σ0 from n1, ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Proof step 3 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0[n] = σ1[n])

• Proof step 5:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ (∃ n0. ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0])) ⊦

Rule argument

Additional information

Used terms: σ0 from n1, (σ to n) + σ0 from n1 + n

Proof step 4 from proof from-append-add (previous step) (back to tree)

Lemma extensionality

Proof step 5 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦

Rule argument

Additional information

Proof step 6 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ⌜n⌝ < # σ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝

• Proof step 8:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦ ⌜n1⌝ < # σ0 ∧ finp(σ0)

• Proof step 32:

  ⌜n1⌝ < # σ0, finp(σ0), ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ ⌜(# σ0).n - n1⌝ ∨ ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦

Rule argument

Additional information

Used terms: n1, σ0

Proof step 7 from proof from-append-add (previous step) (back to tree)

Lemma fin-size-from

Proof step 8 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦ ⌜n1⌝ < # σ0 ∧ finp(σ0)

Rule argument

Additional information

Proof step 9 from proof from-append-add (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  σ0 = ⌜x⌝ , ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦ ⌜n1⌝ < # σ0 ∧ finp(σ0)

• Proof step 21:

  σ0 = ⌜nf⌝ , ¬ # σ0 < ⌜n1⌝ , ¬ # σ < ⌜n⌝ , #((σ to n) + σ0 from n1 + n) ≠ #(σ0 from n1) ∨ ¬(⌜n0⌝ < #((σ to n) + σ0 from n1 + n) → ((σ to n) + σ0 from n1 + n)[n0] = (σ0 from n1)[n0]) ⊦ ⌜n1⌝ < # σ0 ∧ finp(σ0)

Rule argument

Additional information

Used simplifier rules: stream freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 10 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ¬ # σ < ⌜n⌝ , (σ to n) + ⌜x⌝ from # x + n ≠ [] ∨ ¬(⌜n0⌝ < #((σ to n) + ⌜x⌝ from # x + n) → ((σ to n) + ⌜x⌝ from # x + n)[n0] = [][n0]) ⊦

Rule argument

Additional information

Used simplifier rules: length-from: ¬ # x < n ⊦ #(x from n) = # x - n; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; size-empty-equiv: ⊦ # σ = ⌜0⌝ ↔ σ = []; from-all: ⊦ x from # x = []; ⊦ m - m = 0; (s) ⊦ m ≤ m; (s) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ finp(⌜x⌝ ); (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 11 from proof from-append-add (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  σ = ⌜x0⌝ , ¬ # σ < ⌜n⌝ , (σ to n) + ⌜x⌝ from # x + n ≠ [] ∨ ¬(⌜n0⌝ < #((σ to n) + ⌜x⌝ from # x + n) → ((σ to n) + ⌜x⌝ from # x + n)[n0] = [][n0]) ⊦

• Proof step 18:

  σ = ⌜nf⌝ , ¬ # σ < ⌜n⌝ , (σ to n) + ⌜x⌝ from # x + n ≠ [] ∨ ¬(⌜n0⌝ < #((σ to n) + ⌜x⌝ from # x + n) → ((σ to n) + ⌜x⌝ from # x + n)[n0] = [][n0]) ⊦

Rule argument

Additional information

Used simplifier rules: stream freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 12 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (x0 to n) + x from # x + n ≠ [], n ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: fin-empty: ⊦ ⌜x⌝ = [] ↔ x = []; to-fin: ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; from-appfin: ⊦ ⌜x⌝ + ⌜y⌝ from n = ⌜x + y from n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; length-to: ¬ # x < n ⊦ #(x to n) = n; ⊦ ¬ n < 0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m - m = 0; (s) ⊦ m + n - n + n1 = m - n1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ #(x + y) = # x + # y; (s) ⊦ ¬ n < n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 13 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ # x < n → x + y from n = y from (n - # x)

• Proof step 15:

  (x0 to n) + x from # x + n ≠ [], n ≤ # x0, ¬ #(x0 to n) < # x + n ⊦

Rule argument

Additional information

Used simplifier rules: length-to: ¬ # x < n ⊦ #(x to n) = n; from-all: ⊦ x from # x = []; ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: # x + n, x, x0 to n

Proof step 14 from proof from-append-add (previous step) (back to tree)

Lemma append-from-gt

Proof step 15 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (x0 to n) from n ≠ [], n ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: length-to: ¬ # x < n ⊦ #(x to n) = n; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ # [] = 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m + m0 ≤ m ↔ m0 = 0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 16 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

Rule argument

Additional information

Used simplifier rules: length-from: ¬ # x < n ⊦ #(x from n) = # x - n; length-to: ¬ # x < n ⊦ #(x to n) = n; ⊦ # [] = 0; (s) ⊦ ¬ n < n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m - m = 0; (s) ⊦ ¬ n < 0; (s) Used terms: [], (x0 to n) from n

Proof step 17 from proof from-append-add (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  (nf to n) + x from # x + n ≠ [] ⊦

Rule argument

Additional information

Used simplifier rules: size-inf: ⊦ # ⌜nf⌝ = ∞; fin-empty: ⊦ ⌜x⌝ = [] ↔ x = []; to-inf: ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; from-appfin: ⊦ ⌜x⌝ + ⌜y⌝ from n = ⌜x + y from n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-inf-to: ⊦ #(nf to n) = n; ⊦ ¬ n < 0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m - m = 0; (s) ⊦ m + n - n + n1 = m - n1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) ⊦ ¬ n < n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ ∞ < n∞; (s)

Proof step 19 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

Rule argument

Additional information

Used simplifier rules: length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-inf-to: ⊦ #(nf to n) = n; ⊦ # [] = 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ n < n; (s) ⊦ #(x + y) = # x + # y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + n - n + n1 = m - n1; (s) ⊦ m - m = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ n < 0; (s) Used terms: [], (nf to n) + x from # x + n

Proof step 20 from proof from-append-add (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ¬ # σ < ⌜n⌝ , #((σ to n) + ⌜nf⌝ from n1 + n) ≠ ∞ ∨ ((σ to n) + ⌜nf⌝ from n1 + n)[n0] ≠ nf(n0 + n1) ⊦

Rule argument

Additional information

Used simplifier rules: less-size-from: ⌜n⌝ < # σ ⊦ ⌜n0⌝ < #(σ from n) ↔ ⌜n0 + n⌝ < # σ; size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); get-from-inf: ⊦ ((nf from n))(m) = nf(m + n); size-inf: ⊦ # ⌜nf⌝ = ∞; ⊦ ¬ finp(⌜nf⌝ ); (s) ⊦ ⌜m⌝ < ∞; (s) 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⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ ⌜m⌝ + ∞ = ∞; (s) 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) ⊦ ¬ ∞ < n∞; (s)

Proof step 22 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ ⌜n⌝ < # σ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝

• Proof step 24:

  ¬ # σ < ⌜n⌝ , #((σ to n) + ⌜nf⌝ from n1 + n) ≠ ∞ ∨ ((σ to n) + ⌜nf⌝ from n1 + n)[n0] ≠ nf(n0 + n1) ⊦ ⌜n1 + n⌝ < #((σ to n) + ⌜nf⌝ ) ∧ finp((σ to n) + ⌜nf⌝ )

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; size-inf: ⊦ # ⌜nf⌝ = ∞; neq-fin-inf-01: ⊦ ⌜x⌝ ≠ σ + ⌜nf0⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ ⌜m⌝ + ∞ = ∞; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ ⌜n⌝ ≠ ∞; (s) stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic Used terms: n1 + n, (σ to n) + ⌜nf⌝

Proof step 23 from proof from-append-add (previous step) (back to tree)

Lemma fin-size-from

Proof step 24 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ⌜nf0⌝ = (σ to n) + ⌜nf⌝ , nf0(n0 + n1 + n) ≠ nf(n0 + n1), ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-inf: ⊦ # ⌜nf⌝ = ∞; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); get-from-inf: ⊦ ((nf from n))(m) = nf(m + n); ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s) ⊦ ¬ finp(⌜nf⌝ ); (s) stream-inf-forward: ⊦ ¬ finp(σ) → (∃ nf. ⌜nf⌝ = σ); (forward) from specification stream-basic 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⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ ⌜m⌝ + ∞ = ∞; (s) 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)

Proof step 25 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0[n] = σ1[n])

• Proof step 27:

  # ⌜nf0⌝ = #((σ to n) + ⌜nf⌝ ), nf0(n0 + n1 + n) ≠ nf(n0 + n1), ¬ # σ < ⌜n⌝ , ∀ n0. ⌜n0⌝ < # ⌜nf0⌝ → ⌜nf0⌝ [n0] = ((σ to n) + ⌜nf⌝ )[n0] ⊦

Rule argument

Additional information

Used terms: (σ to n) + ⌜nf⌝ , ⌜nf0⌝

Proof step 26 from proof from-append-add (previous step) (back to tree)

Lemma extensionality

Proof step 27 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  nf0(n0 + n1 + n) ≠ nf(n0 + n1), ¬ # σ < ⌜n⌝ , ∀ n2. nf0(n2) = ((σ to n) + ⌜nf⌝ )[n2] ⊦

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-inf: ⊦ # ⌜nf⌝ = ∞; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); ⊦ ⌜m⌝ < ∞; (s) 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 ⊦ ⌜m⌝ + ∞ = ∞; (s)

Proof step 28 from proof from-append-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

  nf0(n0 + n1 + n) = ((σ to n) + ⌜nf⌝ )[n0 + n1 + n], nf0(n0 + n1 + n) ≠ nf(n0 + n1), ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Used terms: n0 + n1 + n

Proof step 29 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  nf0(n0 + n1 + n) = ((σ to n) + ⌜nf⌝ )[n0 + n1 + n], ((σ to n) + ⌜nf⌝ )[n0 + n1 + n] ≠ nf(n0 + n1), ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Proof step 30 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)[m] = σ1[m - (# σ).n]

Rule argument

Additional information

Used simplifier rules: get-append-ls: ⊦ ⌜m⌝ < # σ → (σ + σ1)[m] = σ[m]; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; sel-inf: ⊦ ⌜nf⌝ [n] = nf(n); ⊦ ⌜n⌝ .n = n; (s) ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n1 + n + m < n0; (s) ⊦ ¬ m + n < m; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf Used terms: n0 + n1 + n, ⌜nf⌝ , σ to n

Proof step 31 from proof from-append-add (previous step) (back to tree)

Lemma get-append-notls

Proof step 32 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  x ≠ [], n1 < # x, ¬ # σ < ⌜n⌝ , #((σ to n) + ⌜x⌝ from n1 + n) ≠ ⌜# x - n1⌝ ∨ ¬(n0 + n1 < # x → ((σ to n) + ⌜x⌝ from n1 + n)[n0] = x[n1 + n0]) ⊦

Rule argument

Additional information

Used simplifier rules: less-size-from: ⌜n⌝ < # σ ⊦ ⌜n0⌝ < #(σ from n) ↔ ⌜n0 + n⌝ < # σ; size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; get-from: ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m]; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ finp(⌜x⌝ ); (s) stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2; (s) 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) ⊦ n∞ < n∞0 → ¬ n∞0 < n∞; (s)

Proof step 33 from proof from-append-add (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 34:

  # x = n2 + n1, x ≠ [], n1 < # x, n1 ≤ # x, ¬ # σ < ⌜n⌝ , #((σ to n) + ⌜x⌝ from n1 + n) ≠ ⌜n2⌝ ∨ ¬(n0 + n1 < # x → ((σ to n) + ⌜x⌝ from n1 + n)[n0] = x[n1 + n0]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x, n1, n2

Proof step 34 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # x = n2 + n1, n2 ≠ 0, x ≠ [], ¬ # σ < ⌜n⌝ , #((σ to n) + ⌜x⌝ from n1 + n) ≠ ⌜n2⌝ ∨ ¬(n0 < n2 → ((σ to n) + ⌜x⌝ from n1 + n)[n0] = x[n1 + n0]) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s)

Proof step 35 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ ⌜n⌝ < # σ ∧ finp(σ) → #(σ from n) = ⌜(# σ).n - n⌝

• Proof step 37:

  # x = n2 + n1, n2 ≠ 0, x ≠ [], ⌜n1 + n⌝ < #((σ to n) + ⌜x⌝ ), finp((σ to n) + ⌜x⌝ ), ¬ # σ < ⌜n⌝ , ⌜(#((σ to n) + ⌜x⌝ )).n - n1 + n⌝ ≠ ⌜n2⌝ ∨ ¬(n0 < n2 → ((σ to n) + ⌜x⌝ from n1 + n)[n0] = x[n1 + n0]) ⊦

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; neq-fin-inf-03: ⊦ σ0 + ⌜x⌝ = ⌜nf0⌝ ↔ σ0 = ⌜nf0⌝ ; inf-not-to: ⊦ ⌜nf⌝ ≠ σ to n; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ m < m + n ↔ n ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic stream-inf-forward: ⊦ ¬ finp(σ) → (∃ nf. ⌜nf⌝ = σ); (forward) from specification stream-basic Used terms: n1 + n, (σ to n) + ⌜x⌝

Proof step 36 from proof from-append-add (previous step) (back to tree)

Lemma fin-size-from

Proof step 37 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  # x = n2 + n1, ⌜x0⌝ = (σ to n) + ⌜x⌝ , (x0 from n1 + n)[n0] ≠ x[n1 + n0], x ≠ [], n0 < n2, ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ m < n → n ≠ 0; (s) stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m + n - m = n; (s) ⊦ m < m + n ↔ n ≠ 0; (s) n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ m < n → m ≤ n; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ m + n - n + n1 = m - n1; (s) 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⌝ .n = n; (s) n∞ ≠ ∞ ⊦ (⌜m⌝ + n∞).n = m + n∞.n; (s) ⊦ ⌜n⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; (s)

Proof step 38 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0[n] = σ1[n])

• Proof step 40:

  # ⌜x0⌝ = #((σ to n) + ⌜x⌝ ), # x = n2 + n1, (x0 from n1 + n)[n0] ≠ x[n1 + n0], x ≠ [], n0 < n2, ¬ # σ < ⌜n⌝ , ∀ n0. ⌜n0⌝ < # ⌜x0⌝ → ⌜x0⌝ [n0] = ((σ to n) + ⌜x⌝ )[n0] ⊦

Rule argument

Additional information

Used terms: (σ to n) + ⌜x⌝ , ⌜x0⌝

Proof step 39 from proof from-append-add (previous step) (back to tree)

Lemma extensionality

Proof step 40 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  # x = n2 + n1, n + n2 + n1 = # x0, x0[(n1 + n) + n0] ≠ x[n1 + n0], x ≠ [], n0 < n2, ¬ # σ < ⌜n⌝ , ∀ n3. n3 < # x0 → x0[n3] = ((σ to n) + ⌜x⌝ )[n3] ⊦

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; get-from-01: m + m0 < # x ⊦ (x from m)[m0] = x[m + m0]; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) 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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)

Proof step 41 from proof from-append-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 42:

  # x = n2 + n1, n + n2 + n1 = # x0, x0[(n1 + n) + n0] ≠ x[n1 + n0], x ≠ [], n0 < n2, ¬ # σ < ⌜n⌝ , (n1 + n) + n0 < # x0 → x0[(n1 + n) + n0] = ((σ to n) + ⌜x⌝ )[(n1 + n) + n0] ⊦

Rule argument

Additional information

Used terms: (n1 + n) + n0

Proof step 42 from proof from-append-add (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 43:

  # x = n2 + n1, n + n2 + n1 = # x0, x0[(n1 + n) + n0] = ((σ to n) + ⌜x⌝ )[(n1 + n) + n0], x0[(n1 + n) + n0] ≠ x[n1 + n0], x ≠ [], n0 < n2, ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 43 from proof from-append-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  # x = n2 + n1, n + n2 + n1 = # x0, x0[(n1 + n) + n0] = ((σ to n) + ⌜x⌝ )[(n1 + n) + n0], ((σ to n) + ⌜x⌝ )[(n1 + n) + n0] ≠ x[n1 + n0], x ≠ [], n0 < n2, ¬ # σ < ⌜n⌝ ⊦

Rule argument

Additional information

Proof step 44 from proof from-append-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

  ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)[m] = σ1[m - (# σ).n]

Rule argument

Additional information

Used simplifier rules: get-append-ls: ⊦ ⌜m⌝ < # σ → (σ + σ1)[m] = σ[m]; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; sel-fin: ⊦ ⌜x⌝ [n] = x[n]; ⊦ ⌜n⌝ .n = n; (s) ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n1 + n + m < n0; (s) ⊦ ¬ m + n < m; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf Used terms: (n1 + n) + n0, ⌜x⌝ , σ to n

Proof step 45 from proof from-append-add (previous step) (back to tree)

Lemma get-append-notls