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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  mklist(a, m + n) ≠ mklist(a, m) + mklist(a, n) ⊦

Rule argument

Additional information

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

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 3:

  mklist(a, m + n0 +1) ≠ mklist(a, m) + mklist(a, n0 +1), ∀ a, m. mklist(a, m + n0) = mklist(a, m) + mklist(a, n0) ⊦

Rule argument

Additional information

Used simplifier rules: mk-zero: ⊦ mklist(a, 0) = []; nat freely generated by 0, +1;; ⊦ 0 + m = m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 3 from proof mk-plus (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  mklist(a, m + n0) ≠ mklist(a, m) + mklist(a, n0), ∀ a, m. mklist(a, m + n0) = mklist(a, m) + mklist(a, n0) ⊦

Rule argument

Additional information

Used simplifier rules: mk-succ: ⊦ mklist(a, n + 1) = a ' + mklist(a, n); mk-last: ⊦ mklist(a, n) + a ' = a ' + mklist(a, n); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = x + z ↔ y = z; (s) 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)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, m