Proof step 1 from proof cong-equiv (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(m | dist(n, n0) ↔ n % m = n0 % m), m ≠ 0 ⊦

Rule argument

Additional information

Proof step 2 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(m | dist(n, n0) ↔ n % m = n0 % m), m ≠ 0 ⊦

Rule argument

Additional information

Proof step 3 from proof cong-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  ¬(m | dist(n, n0) ↔ n % m = n0 % m), m ≠ 0, ¬ n ≤ n0 ⊦

• Proof step 26:

  ¬(m | n0 - n ↔ n % m = n0 % m), m ≠ 0, n ≤ n0 ⊦

Rule argument

Additional information

Used terms: n0, n

Proof step 4 from proof cong-equiv (previous step) (back to tree)

Lemma dist-fst

Proof step 5 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬(m | dist(n, n0) ↔ n % m = n0 % m), m ≠ 0, n0 < n ⊦

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 6 from proof cong-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  ¬(m | n - n0 ↔ n % m = n0 % m), m ≠ 0, n0 < n ⊦

Rule argument

Additional information

Used terms: n0, n

Proof step 7 from proof cong-equiv (previous step) (back to tree)

Lemma dist-snd

Proof step 8 from proof cong-equiv (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  n = n1 + n0, ¬(m | n1 ↔ n % m = n0 % m), m ≠ 0, n0 < n, n0 ≤ n ⊦

Rule argument

Additional information

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

Proof step 9 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬(m | n1 ↔ (n1 + n0) % m = n0 % m), m ≠ 0, n1 ≠ 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 ↔ n ≠ 0; (s) ⊦ m < n → m ≤ n; (s)

Proof step 10 from proof cong-equiv (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  (n1 + n0) % m ≠ n0 % m, m ≠ 0, n1 ≠ 0, m | n1 ⊦

• Proof step 13:

  (n1 + n0) % m = n0 % m, m ≠ 0, n1 ≠ 0, ¬ m | n1 ⊦

Rule argument

Additional information

Proof step 11 from proof cong-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ (m + n0 * n) % n = 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 Used terms: n1, m

Proof step 12 from proof cong-equiv (previous step) (back to tree)

Lemma Divides

Proof step 13 from proof cong-equiv (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  n1 + n0 = m0 * m + n2, n2 = n0 % m, m ≠ 0, n1 ≠ 0, n2 < m, ¬ m | n1 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n1 + n0, m, m0, n

Proof step 14 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  n1 + n0 = m0 * m + n0 % m, n1 ≠ 0, n0 % m < m, ¬ m | n1 ⊦

Rule argument

Additional information

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

Proof step 15 from proof cong-equiv (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  n1 + n0 = m0 * m + n2, n0 = m1 * m + n2, m ≠ 0, n1 ≠ 0, n2 < m, ¬ m | n1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 * n = 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ n < 0; (s) n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n0, m, m1, n

Proof step 16 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  n1 + m1 * m = m0 * m, n1 ≠ 0, n2 < m, ¬ m | n1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) 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)

Proof step 17 from proof cong-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  n1 + m1 * m = m0 * m, n1 ≠ 0, n2 < m, ∀ n0. m * n0 ≠ n1 ⊦

Rule argument

Additional information

Used terms: n1, m

Proof step 18 from proof cong-equiv (previous step) (back to tree)

Lemma Divides

Proof step 19 from proof cong-equiv (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used terms: m0 - m1

Proof step 20 from proof cong-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ m0 ≤ m → (m - m0) * n = m * n - m0 * n

• Proof step 22:

  n1 + m1 * m = m0 * m, m * (m0 - m1) ≠ n1, n1 ≠ 0, n2 < m, ¬ m1 ≤ m0 ⊦

• Proof step 25:

  n1 + m1 * m = m0 * m, m0 * m - m1 * m ≠ n1, n1 ≠ 0, n2 < m, m1 ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: m, m1, m0

Proof step 21 from proof cong-equiv (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

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 23 from proof cong-equiv (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n; (ws) ⊦ m < n → n ≠ 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used formulas: m0 * m < m1 * m

Proof step 24 from proof cong-equiv (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

Proof step 25 from proof cong-equiv (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

Proof step 26 from proof cong-equiv (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 27:

  n0 = n1 + n, ¬(m | n1 ↔ n % m = n0 % m), m ≠ 0, n ≤ n0 ⊦

Rule argument

Additional information

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

Proof step 27 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  ¬(m | n1 ↔ n % m = (n1 + n) % m), m ≠ 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 28 from proof cong-equiv (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  n % m ≠ (n1 + n) % m, m ≠ 0, m | n1 ⊦

• Proof step 31:

  n % m = (n1 + n) % m, m ≠ 0, ¬ m | n1 ⊦

Rule argument

Additional information

Proof step 29 from proof cong-equiv (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ (m + n0 * n) % n = 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 Used terms: n1, m

Proof step 30 from proof cong-equiv (previous step) (back to tree)

Lemma Divides

Proof step 31 from proof cong-equiv (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 32:

  n = m0 * m + n0, n0 = (n1 + n) % m, m ≠ 0, n0 < m, ¬ m | n1 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n, m, m0, n0

Proof step 32 from proof cong-equiv (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

Proof step 33 from proof cong-equiv (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  n1 % m = 0, n0 < m, ¬ m | n1 ⊦

Rule argument

Additional information

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

Proof step 34 from proof cong-equiv (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: divi-mult: ⊦ m | m * n0; ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m < n → n ≠ 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ ¬ n < 0; (s) n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: n1, m, m0, n