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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  σ from m from n ≠ σ from m + n, ¬ # σ < ⌜m + n⌝ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  σ from m from n ≠ σ from m + n, ¬ # σ < ⌜m⌝ + ⌜n⌝ ⊦

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-from (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ⌜x⌝ from m from n ≠ ⌜x⌝ from m + n, ¬ # ⌜x⌝ < ⌜m⌝ + ⌜n⌝ ⊦

• Proof step 10:

  ⌜nf⌝ from m from n ≠ ⌜nf⌝ from m + n, ¬ # ⌜nf⌝ < ⌜m⌝ + ⌜n⌝ ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  x from m from n ≠ x from m + n, m + n ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: from-fin: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; size-fin: ⊦ # ⌜x⌝ = ⌜# x⌝ ; 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 ↔ ¬ n ≤ m; (ss) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  a + x0 from m from n ≠ a + x0 from m + n, m + n ≤ #(a + x0), ∀ m, n. ¬(x0 from m from n ≠ x0 from m + n ∧ m + n ≤ # x0) ⊦

Rule argument

Additional information

Used simplifier rules: from-zero-l: ⊦ x from 0 = x; list('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a ' + x0 from m from n ≠ a ' + x0 from m + n, m + n ≤ # x0 + 1, ∀ m0, n0. x0 from m0 from n0 = x0 from m0 + n0 ∨ ¬ m0 + n0 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a + x = a ' + x; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 8:

  a ' + x0 from m0 +1 from n ≠ a ' + x0 from m0 +1 + n, m0 +1 + n ≤ # x0 + 1, ∀ m0, n0. x0 from m0 from n0 = x0 from m0 + n0 ∨ ¬ m0 + n0 ≤ # x0, ∀ a, x0, n. ¬(a ' + x0 from m0 from n ≠ a ' + x0 from m0 + n ∧ m0 + n ≤ # x0 + 1 ∧ (∀ m0, n0. x0 from m0 from n0 = x0 from m0 + n0 ∨ ¬ m0 + n0 ≤ # x0)) ⊦

Rule argument

Additional information

Used simplifier rules: from-zero-l: ⊦ x from 0 = x; nat freely generated by 0, +1;; ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  x0 from m0 from n ≠ x0 from m0 + n, m0 + n ≤ # x0, ∀ m0, n0. x0 from m0 from n0 = x0 from m0 + n0 ∨ ¬ m0 + n0 ≤ # x0, ∀ a, x, n0. a ' + x from m0 from n0 = a ' + x from m0 + n0 ∨ ¬ m0 + n0 ≤ # x + 1 ∨ ¬(∀ m0, n0. x from m0 from n0 = x from m0 + n0 ∨ ¬ m0 + n0 ≤ # x) ⊦

Rule argument

Additional information

Used simplifier rules: from-succ-cons-l-lem: ⊦ a ' + x from n + 1 = x from n; 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 +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m0, n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  nf from m from n ≠ nf from m + n ⊦

Rule argument

Additional information

Used simplifier rules: from-inf: ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; size-inf: ⊦ # ⌜nf⌝ = ∞; ⊦ ¬ ∞ < n∞; (s) ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ nf from n = (λ m. nf(n + m))

• Proof step 13:

  (λ m0. nf(m + m0)) from n ≠ nf from m + n ⊦

Rule argument

Additional information

Used terms: m, nf

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

Lemma from-nf

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ nf from n = (λ m. nf(n + m))

Rule argument

Additional information

Used simplifier rules: get-from-inf: ⊦ ((nf from n))(m) = nf(m + n); a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: m + n, nf

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

Lemma from-nf