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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(m0 * m = 1 ↔ m0 = 1 ∧ m = 1) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  m0 * m = 1 ⊦ m0 = 1 ∧ m = 1

Rule argument

Additional information

Used simplifier rules: mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m;

Proof step 3 from proof one-01 (previous step) (back to tree)

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: zero: ⊦ 0 * n = 0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; rsucc-01: ⊦ (m + 1) * n = m * n + n; zero: ⊦ 0 * n = 0; one: ⊦ m0 * 1 = m0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; nat freely generated by 0, +1;; ⊦ m +1 = m + 1; (s) ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ n ≠ 0 → (m + n = 1 ↔ n = 1 ∧ m = 0); (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic