Proof step 1 from proof divi-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  m | dist(n, m0), m | dist(n0, m0), ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Proof step 2 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  m | dist(n0, m0), m | dist(n, m0), ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Proof step 3 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ m | n ↔ (∃ n0. m * n0 = n)

• Proof step 5:

  m | dist(n, m0), ¬ m | dist(n, n0), ∃ n1. m * n1 = dist(n0, m0) ⊦

Rule argument

Additional information

Used terms: dist(n0, m0), m

Proof step 4 from proof divi-same (previous step) (back to tree)

Lemma Divides

Proof step 5 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  m * n1 = dist(n0, m0), m | dist(n, m0), ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Proof step 6 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ m | n ↔ (∃ n0. m * n0 = n)

• Proof step 8:

  m * n1 = dist(n0, m0), ¬ m | dist(n, n0), ∃ n0. m * n0 = dist(n, m0) ⊦

Rule argument

Additional information

Used terms: dist(n, m0), m

Proof step 7 from proof divi-same (previous step) (back to tree)

Lemma Divides

Proof step 8 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  m * n2 = dist(n, m0), m * n1 = dist(n0, m0), ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Proof step 9 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ m ≤ n → dist(m, n) = n - m

• Proof step 11:

  m * n1 = dist(n0, m0), m * n2 = dist(n, m0), ¬ m | dist(n, n0), ¬ n ≤ m0 ⊦

• Proof step 24:

  m * n1 = dist(n0, m0), m * n2 = m0 - n, n ≤ m0, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used terms: m0, n

Proof step 10 from proof divi-same (previous step) (back to tree)

Lemma dist-fst

Proof step 11 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  m * n1 = dist(n0, m0), m * n2 = dist(n, m0), m0 < n, ¬ m | dist(n, 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 12 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ n < m → dist(m, n) = m - n

• Proof step 14:

  m * n2 = n - m0, m * n1 = dist(n0, m0), m0 < n, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used terms: m0, n

Proof step 13 from proof divi-same (previous step) (back to tree)

Lemma dist-snd

Proof step 14 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  m * n1 = dist(n0, m0), m * n2 = n3, n = n3 + m0, m0 < n, m0 ≤ n, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, m0, n3

Proof step 15 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  m * n1 = dist(n0, m0), m ≠ 0, n2 ≠ 0, ¬ m | dist(m * n2 + m0, n0) ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → m ≤ n; (s)

Proof step 16 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ m ≤ n → dist(m, n) = n - m

• Proof step 18:

  m * n1 = dist(n0, m0), m ≠ 0, n2 ≠ 0, ¬ m | dist(m * n2 + m0, n0), ¬ n0 ≤ m0 ⊦

• Proof step 23:

  m * n1 = m0 - n0, m ≠ 0, n2 ≠ 0, n0 ≤ m0, ¬ m | dist(m * n2 + m0, n0) ⊦

Rule argument

Additional information

Used terms: m0, n0

Proof step 17 from proof divi-same (previous step) (back to tree)

Lemma dist-fst

Proof step 18 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  m * n1 = dist(n0, m0), m ≠ 0, n2 ≠ 0, m0 < n0, ¬ m | dist(m * n2 + m0, 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 19 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ n < m → dist(m, n) = m - n

• Proof step 21:

  m * n1 = n0 - m0, m ≠ 0, n2 ≠ 0, m0 < n0, ¬ m | dist(m * n2 + m0, n0) ⊦

Rule argument

Additional information

Used terms: m0, n0

Proof step 20 from proof divi-same (previous step) (back to tree)

Lemma dist-snd

Proof step 21 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 22:

  m * n1 = n3, n0 = n3 + m0, m ≠ 0, n2 ≠ 0, m0 < n0, m0 ≤ n0, ¬ m | dist(m * n2 + m0, n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0, m0, n

Proof step 22 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: dist-add-01: ⊦ dist(m + n, m0 + n) = dist(m, m0); dist-mult: ⊦ dist(m * n, m * n0) = m * dist(n, n0); divi-mult: ⊦ m | m * n0; mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → m ≤ n; (s)

Proof step 23 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: dist-add: ⊦ dist(m + n, m) = n; divi-add-01: ⊦ m | m * n + n0 ↔ m | n0; divi-mult: ⊦ m | m * n0; ⊦ m ≤ m + n; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m0, n0, n

Proof step 24 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 25:

  m * n2 = n3, m * n1 = dist(n0, m0), m0 = n3 + n, n ≤ m0, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m0, n, n3

Proof step 25 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  m * n1 = dist(n0, m * n2 + n), ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 26 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ m ≤ n → dist(m, n) = n - m

• Proof step 28:

  m * n1 = dist(n0, m * n2 + n), ¬ m | dist(n, n0), ¬ n0 ≤ m * n2 + n ⊦

• Proof step 32:

  m * n1 = m * n2 + n - n0, n0 ≤ m * n2 + n, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used terms: m * n2 + n, n0

Proof step 27 from proof divi-same (previous step) (back to tree)

Lemma dist-fst

Proof step 28 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  m * n1 = dist(n0, m * n2 + n), m * n2 + n < n0, ¬ m | dist(n, 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 29 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ n < m → dist(m, n) = m - n

• Proof step 31:

  m * n1 = n0 - m * n2 + n, m * n2 + n < n0, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used terms: m * n2 + n, n0

Proof step 30 from proof divi-same (previous step) (back to tree)

Lemma dist-snd

Proof step 31 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: dist-add: ⊦ dist(m + n, m) = n; dist-c: ⊦ dist(m, n) = dist(n, m); divi-add-01: ⊦ m | m * n + n0 ↔ m | n0; divi-mult: ⊦ m | m * n0; ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m ≤ m + n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0, m * n2 + n, n3

Proof step 32 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 33:

  m * n1 = n3, m * n2 + n = n3 + n0, n0 ≤ m * n2 + n, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m * n2 + n, n0, n3

Proof step 33 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  m * n2 + n = m * n1 + n0, ¬ m | dist(n, n0) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 34 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ m ≤ n → dist(m, n) = n - m

• Proof step 36:

  m * n2 + n = m * n1 + n0, ¬ m | dist(n, n0), ¬ n ≤ n0 ⊦

• Proof step 50:

  m * n2 + n = m * n1 + n0, n ≤ n0, ¬ m | n0 - n ⊦

Rule argument

Additional information

Used terms: n0, n

Proof step 35 from proof divi-same (previous step) (back to tree)

Lemma dist-fst

Proof step 36 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  m * n2 + n = m * n1 + n0, n0 < n, ¬ m | dist(n, 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 37 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ n < m → dist(m, n) = m - n

• Proof step 39:

  m * n2 + n = m * n1 + n0, n0 < n, ¬ m | n - n0 ⊦

Rule argument

Additional information

Used terms: n0, n

Proof step 38 from proof divi-same (previous step) (back to tree)

Lemma dist-snd

Proof step 39 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 40:

  m * n2 + n = m * n1 + n0, n = n3 + n0, n0 < n, n0 ≤ n, ¬ m | n3 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, n0, n3

Proof step 40 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  m * n2 + n3 = m * n1, n3 ≠ 0, ¬ m | n3 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → m ≤ n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 41 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ m | n ↔ (∃ n0. m * n0 = n)

• Proof step 43:

  m * n2 + n3 = m * n1, n3 ≠ 0, ∀ n0. m * n0 ≠ n3 ⊦

Rule argument

Additional information

Used terms: n3, m

Proof step 42 from proof divi-same (previous step) (back to tree)

Lemma Divides

Proof step 43 from proof divi-same (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 44:

  m * n2 + n3 = m * n1, m * (n1 - n2) ≠ n3, n3 ≠ 0 ⊦

Rule argument

Additional information

Used terms: n1 - n2

Proof step 44 from proof divi-same (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 45:

  m * n2 + n3 = m * n1, m * (n1 - n2) ≠ n3, n3 ≠ 0, ¬ n2 ≤ n1 ⊦

• Proof step 47:

  m * n2 + n3 = m * n1, n1 = n0 + n2, m * n0 ≠ n3, n3 ≠ 0, n2 ≤ n1 ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1, n2, n0

Proof step 45 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  m * n2 + n3 = m * n1, m * (n1 - n2) ≠ n3, n3 ≠ 0, n1 < n2 ⊦

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 46 from proof divi-same (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; (ws) ⊦ 0 + m = m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 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 ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → ¬ n1 < m0; (s) Used formulas: m * n1 < m * n2

Proof step 47 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  m * n2 + n3 = m * (n0 + n2), m * n0 ≠ n3, n3 ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 48 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ m0 * (m + n) = m0 * m + m0 * n

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n2, n0, m

Proof step 49 from proof divi-same (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof divi-same (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 51:

  m * n2 + n = m * n1 + n0, n0 = n3 + n, n ≤ n0, ¬ m | n3 ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0, n, n3

Proof step 51 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  m * n2 = m * n1 + n3, ¬ m | n3 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 52 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 53:

  ⊦ m | n ↔ (∃ n0. m * n0 = n)

• Proof step 54:

  m * n2 = m * n1 + n3, ∀ n0. m * n0 ≠ n3 ⊦

Rule argument

Additional information

Used terms: n3, m

Proof step 53 from proof divi-same (previous step) (back to tree)

Lemma Divides

Proof step 54 from proof divi-same (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  m * n2 = m * n1 + n3, m * (n2 - n1) ≠ n3 ⊦

Rule argument

Additional information

Used terms: n2 - n1

Proof step 55 from proof divi-same (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 56:

  m * n2 = m * n1 + n3, m * (n2 - n1) ≠ n3, ¬ n1 ≤ n2 ⊦

• Proof step 58:

  m * n2 = m * n1 + n3, n2 = n0 + n1, m * n0 ≠ n3, n1 ≤ n2 ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n2, n1, n0

Proof step 56 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  m * n2 = m * n1 + n3, m * (n2 - n1) ≠ n3, n2 < n1 ⊦

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 57 from proof divi-same (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; (ws) ⊦ 0 + m = m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 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 ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → ¬ n1 < m0; (s) Used formulas: m * n2 < m * n1

Proof step 58 from proof divi-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  m * (n0 + n1) = m * n1 + n3, m * n0 ≠ n3 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s)

Proof step 59 from proof divi-same (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ m0 * (m + n) = m0 * m + m0 * n

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n1, n0, m

Proof step 60 from proof divi-same (previous step) (back to tree)

A spec-lemma