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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(m0 * m + n0 < m0 * n ↔ m < n), n0 < m0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(m0 * m + n0 < m0 * n ↔ m < n), n0 < m0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  n0 < m0, m0 * m + n0 < m0 * n, ¬ m < n ⊦

• Proof step 6:

  n0 < m0, m < n, ¬ m0 * m + n0 < m0 * n ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  n ≠ 0, n0 < m0, m0 * m + n0 < m0 * n, n ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: zero-01: ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ls: ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; mult-a: ⊦ m0 * m * n = (m0 * m) * n; mult-c: ⊦ m * n = n * m; ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → n ≠ 0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: m0 * n ≤ m0 * m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  n0 < m0, m < n, m0 * n ≤ m0 * m + n0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  m0 * n ≠ m0 * m + n0, m < n, n0 < m0, m0 * n ≤ m0 * m + n0 ⊦

Rule argument

Additional information

Used simplifier rules: modeq-01: ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 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 lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used formulas: m0 * n = m0 * m + n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  m0 * n ≠ m0 * m + n0, m0 * n < m0 * m + n0, m < n, n0 < m0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  n0 < m0, m0 * n ≤ m0 * m + n0 ⊦ n ≤ m

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n → m ≤ n; (s) Used terms: n0, m0, n, m

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

Lemma modp