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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(m * n ≤ n ↔ m ≤ 1), n ≠ 0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(m * n ≤ n ↔ m ≤ 1), n ≠ 0 ⊦

Rule argument

Additional information

Proof step 3 from proof leone (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  n0 +1 ≠ 0, ¬(m * n0 +1 ≤ n0 +1 ↔ m ≤ 1), ∀ m. ¬(¬(m * n0 ≤ n0 ↔ m ≤ 1) ∧ n0 ≠ 0) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(n0 * m + m ≤ n0 + 1 ↔ m ≤ 1), n0 ≠ 0, ∀ m0. m0 * n0 ≤ n0 ↔ m0 ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: rsucc-01: ⊦ (m + 1) * n = m * n + n; zero: ⊦ 0 * n = 0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≠ 0; (s)

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  ¬(n0 * m + m ≤ n0 + 1 ↔ m ≤ 1), m ≠ 0, n0 ≠ 0, ∀ m0. m0 * n0 ≤ n0 ↔ m0 ≤ 1 ⊦

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; a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 ≤ m; (s) Used formulas: m = 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  m ≠ 0, m ≠ 1, n0 ≠ 0, n0 * m + m ≤ n0 + 1, ∀ m0. m0 * n0 ≤ n0 ↔ m0 ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: one: ⊦ m0 * 1 = m0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; 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 ≠ 0 → (m ≤ 1 ↔ m = 1); (s)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: zero-06: ⊦ m ≠ 0 → (m * n = 0 ↔ n = 0); coef-18: ⊦ m * n + n ≤ m1 * n ↔ m + 1 ≤ m1 ∨ n = 0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic le-one: ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: m