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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n→i(m * n) ≠ n→i(m) * n→i(n) ⊦

Rule argument

Additional information

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

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 3:

  n→i(m * n0 +1) ≠ n→i(m) * n→i(n0 +1), ∀ m. n→i(m * n0) = n→i(m) * n→i(n0) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ m * 0 = 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ i * 0 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 3 from proof n2i-mult (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  n→i(m * n0) + n→i(m) ≠ n→i(m) * (n→i(n0) + 1), ∀ m. n→i(m * n0) = n→i(m) * n→i(n0) ⊦

Rule argument

Additional information

Used simplifier rules: n2i-add: ⊦ n→i(m + n) = n→i(m) + n→i(n); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m * (n + 1) = m * n + m; (s)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i * j + i = i * (j + 1); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used terms: m