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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

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 + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 3 from proof from-append-tofrom (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:

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

Rule argument

Additional information

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

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

Lemma extensionality

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: size-append: ⊦ #(σ + σ1) = # σ + # σ1; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; 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 c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ m + n < m; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) lels-trans: ⊦ ¬ n∞1 < n∞ ∧ n∞1 < n∞2 → n∞ < n∞2; (forward) from specification nat-inf ⊦ ⌜n⌝ + n∞1 = ⌜n⌝ + n∞2 ↔ n∞1 = n∞2; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝

• Proof step 8:

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

• Proof step 9:

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

Rule argument

Additional information

Used terms: σ from n, n1

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

Lemma size-to

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

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; length-from: ¬ # x < n ⊦ #(x from n) = # x - n; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; size-inf: ⊦ # ⌜nf⌝ = ∞; stream freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ¬ ∞ < n∞; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: get-to: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]; ⊦ m < n → n ≠ 0; (s) 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⌝ + ⌜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 10 from proof from-append-tofrom (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ ⌜m⌝ < # σ → (σ + σ1)[m] = σ[m]

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; get-to: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]; ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lels-trans: ⊦ ¬ n∞1 < n∞ ∧ n∞1 < n∞2 → n∞ < n∞2; (forward) from specification nat-inf ⊦ m < n → n ≠ 0; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic 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: σ to n, (σ from n) to n1, n0

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

Lemma get-append-ls

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (σ from n)[n0 - n] ≠ σ[n0], n1 ≠ 0, n0 < n + n1, n ≤ n0, ¬ #(σ from n) < ⌜n1⌝ , ¬ # σ < ⌜n⌝ + ⌜n1⌝ ⊦

Rule argument

Additional information

Used simplifier rules: get-append-notls: ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)[m] = σ1[m - (# σ).n]; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; size-to: ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; get-to: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]; 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) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ ⌜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 ⊦ ¬ m + n < m; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) lels-trans: ⊦ ¬ n∞1 < n∞ ∧ n∞1 < n∞2 → n∞ < n∞2; (forward) from specification nat-inf ⊦ ⌜n⌝ .n = n; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0, n, n2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (σ from n)[n2] ≠ σ[n2 + n], n2 < n1, ¬ # σ < ⌜n⌝ + ⌜n1⌝ , ¬ #(σ from n) < ⌜n1⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) 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 ≤ m + n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m]

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic lele-trans: ⊦ ¬ n∞1 < n∞ ∧ ¬ n∞2 < n∞1 → ¬ n∞2 < n∞; (forward) from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic 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: σ, n, n2

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

Lemma get-from