Proof step 1 from proof gcd-rec (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gcd(i, j) ≠ gcd(abs(j), abs(i) % abs(j)), j ≠ 0 ⊦

Rule argument

Additional information

Proof step 2 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gcd(i, j) ≠ gcd(abs(j), abs(i) % abs(j)), j ≠ 0 ⊦

Rule argument

Additional information

Proof step 3 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ gcd(i, j) = gcd(abs(i), abs(j))

• Proof step 5:

  gcd(abs(i), abs(j)) ≠ gcd(abs(j), abs(i) % abs(j)), j ≠ 0 ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 4 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-abs-rew-02

Proof step 5 from proof gcd-rec (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), j ≠ 0, j0 < abs(j), 0 < abs(j), 0 ≤ j0, 0 ≤ i0, 0 ≤ abs(i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < abs(i) ↔ i ≠ 0; (s) ⊦ 0 ≤ abs(i); (s) ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j ∧ 0 ≤ i0); (elim) Used terms: abs(i), abs(j), i0, j0

Proof step 6 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), j ≠ 0, j0 < abs(j), 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < abs(i) ↔ i ≠ 0; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ 0 ≤ abs(i); (s)

Proof step 7 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ¬ i < j → (i = j ↔ ¬ j < i)

• Proof step 9:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0 ⊦

• Proof step 36:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(i), abs(j)) < gcd(abs(j), j0) ⊦

Rule argument

Additional information

Used terms: gcd(abs(j), j0), gcd(abs(i), abs(j))

Proof step 8 from proof gcd-rec (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), j ≠ 0, j0 < abs(j), gcd(abs(i), abs(j)) < gcd(abs(j), j0), 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Proof step 10 from proof gcd-rec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

  ⊦ i1 | i ∧ i1 | j ∧ 0 ≠ i → i1 ≤ gcd(i, j)

• Proof step 12:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0, gcd(abs(j), j0) | abs(i) ∧ gcd(abs(j), j0) | abs(j) ∧ 0 ≠ abs(i) → gcd(abs(j), j0) ≤ gcd(abs(i), abs(j)) ⊦

Rule argument

Additional information

Used terms: gcd(abs(j), j0), abs(i), abs(j)

Proof step 11 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-less

Proof step 12 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0 ⊦ gcd(abs(j), j0) | abs(j) ∧ gcd(abs(j), j0) | abs(i)

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-nls-01: ⊦ i ≠ 0 → ¬ abs(i) < gcd(abs(i), j); ⊦ abs(abs(i)) = abs(i); (s) ⊦ i < j → ¬ j < i; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ abs(i) = 0 ↔ i = 0; (s)

Proof step 13 from proof gcd-rec (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(abs(i), abs(j)) < gcd(abs(j), j0), 0 ≤ j0, 0 ≤ i0 ⊦ gcd(abs(j), j0) | abs(j) ∧ gcd(abs(j), j0) | abs(i)

Rule argument

Additional information

Used formulas: i = 0

Proof step 14 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0 ⊦ gcd(abs(j), j0) | abs(j) ∧ gcd(abs(j), j0) | abs(i)

Rule argument

Additional information

Proof step 15 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ gcd(i, j) | i

• Proof step 17:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(abs(i), abs(j)) < gcd(abs(j), j0), 0 ≤ j0, 0 ≤ i0 ⊦ true ∧ gcd(abs(j), j0) | abs(i)

Rule argument

Additional information

Used terms: j0, abs(j)

Proof step 16 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-div1

Proof step 17 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(j), j0) | abs(i) ⊦

Rule argument

Additional information

Proof step 18 from proof gcd-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 19:

  abs(i) = i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(j), j0) | i0 * abs(j) + j0 ⊦

Rule argument

Additional information

Proof step 19 from proof gcd-rec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 20:

  ⊦ gcd(i, j) | i

• Proof step 21:

  abs(i) = i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), j0 < abs(j), gcd(abs(j), j0) | abs(j), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(j), j0) | i0 * abs(j) + j0 ⊦

Rule argument

Additional information

Used terms: abs(j), j0

Proof step 20 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-div1

Proof step 21 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(abs(i), abs(j)) < gcd(abs(j), j0), gcd(abs(j), j0) | abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(j), j0) | abs(i) ⊦

Rule argument

Additional information

Proof step 22 from proof gcd-rec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 23:

  ⊦ gcd(i, j) | j

• Proof step 24:

  abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), gcd(abs(j), j0) | abs(j), gcd(abs(j), j0) | j0, 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(j), j0) | abs(i) ⊦

Rule argument

Additional information

Used terms: abs(j), j0

Proof step 23 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-div2

Proof step 24 from proof gcd-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 25:

  abs(i) = i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), gcd(abs(j), j0) | j0, gcd(abs(j), j0) | abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(j), j0) | i0 * abs(j) + j0 ⊦

Rule argument

Additional information

Proof step 25 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 27:

  abs(i) = i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), j0 < abs(j), gcd(abs(j), j0) | abs(j), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(j), j0) | i0 * abs(j) + j0, ∃ i0. gcd(abs(j), j0) * i0 = j0 ⊦

Rule argument

Additional information

Used terms: j0, gcd(abs(j), j0)

Proof step 26 from proof gcd-rec (previous step) (back to tree)

Lemma divides

Proof step 27 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  gcd(abs(j), j0) * i1 = j0, abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(abs(i), abs(j)) < gcd(abs(j), j0), gcd(abs(j), j0) | abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(j), j0) | abs(i) ⊦

Rule argument

Additional information

Proof step 28 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 30:

  gcd(abs(j), j0) * i1 = j0, abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(abs(i), abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(j), j0) | abs(i), ∃ i0. gcd(abs(j), j0) * i0 = abs(j) ⊦

Rule argument

Additional information

Used terms: abs(j), gcd(abs(j), j0)

Proof step 29 from proof gcd-rec (previous step) (back to tree)

Lemma divides

Proof step 30 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  gcd(abs(j), j0) * i2 = abs(j), gcd(abs(j), j0) * i1 = j0, abs(i) = i0 * abs(j) + j0, gcd(abs(i), abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(abs(i), abs(j)) < gcd(abs(j), j0), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(j), j0) | abs(i) ⊦

Rule argument

Additional information

Proof step 31 from proof gcd-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 32:

  gcd(abs(j), j0) * i1 = j0, gcd(abs(j), j0) * i2 = abs(j), abs(i) = i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(j), j0) | i0 * abs(j) + j0 ⊦

Rule argument

Additional information

Proof step 32 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 34:

  gcd(abs(j), j0) * i2 = abs(j), gcd(abs(j), j0) * i1 = j0, abs(i) = i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, j0 < abs(j), gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), 0 ≤ j0, 0 ≤ i0, ∀ i1. gcd(abs(j), j0) * i1 ≠ i0 * abs(j) + j0 ⊦

Rule argument

Additional information

Used terms: i0 * abs(j) + j0, gcd(abs(j), j0)

Proof step 33 from proof gcd-rec (previous step) (back to tree)

Lemma divides

Proof step 34 from proof gcd-rec (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 35:

  gcd(abs(j), j0) * i1 = j0, gcd(abs(j), j0) * i2 = abs(j), abs(i) = i0 * abs(j) + j0, gcd(abs(j), j0) * (i2 * i0 + i1) ≠ i0 * abs(j) + j0, gcd(i0 * abs(j) + j0, abs(j)) ≠ gcd(abs(j), j0), i ≠ 0, j ≠ 0, gcd(i0 * abs(j) + j0, abs(j)) < gcd(abs(j), j0), j0 < abs(j), 0 ≤ i0, 0 ≤ j0 ⊦

Rule argument

Additional information

Used terms: i2 * i0 + i1

Proof step 35 from proof gcd-rec (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (i + j) * i0 = j0 + j * i0 ↔ i * i0 = j0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 neq-not-zero: ⊦ i * j ≠ i * j0 → i ≠ 0; (forward) from specification int-mult ⊦ i ≠ 0 → (i * j = i * j0 ↔ j = j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult

Proof step 36 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → ¬ j < i; (s)

Proof step 37 from proof gcd-rec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 38:

  ⊦ i1 | i ∧ i1 | j ∧ 0 ≠ i → i1 ≤ gcd(i, j)

• Proof step 39:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), 0 ≤ i0, 0 ≤ j0, gcd(abs(i), abs(j)) | abs(j) ∧ gcd(abs(i), abs(j)) | j0 ∧ 0 ≠ abs(j) → gcd(abs(i), abs(j)) ≤ gcd(abs(j), j0) ⊦

Rule argument

Additional information

Used terms: gcd(abs(i), abs(j)), abs(j), j0

Proof step 38 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-less

Proof step 39 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), 0 ≤ j0, 0 ≤ i0 ⊦ gcd(abs(i), abs(j)) | abs(j) ∧ gcd(abs(i), abs(j)) | j0

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → (j ≤ i ↔ false); (as) ⊦ abs(i) = 0 ↔ i = 0; (s)

Proof step 40 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ gcd(i, j) | j

• Proof step 42:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), 0 ≤ i0, 0 ≤ j0 ⊦ true ∧ gcd(abs(i), abs(j)) | j0

Rule argument

Additional information

Used terms: abs(j), abs(i)

Proof step 41 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-div2

Proof step 42 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(i), abs(j)) | j0 ⊦

Rule argument

Additional information

Proof step 43 from proof gcd-rec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 44:

  ⊦ gcd(i, j) | i

• Proof step 45:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | abs(i), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(i), abs(j)) | j0 ⊦

Rule argument

Additional information

Used terms: abs(i), abs(j)

Proof step 44 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-div1

Proof step 45 from proof gcd-rec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 46:

  ⊦ gcd(i, j) | j

• Proof step 47:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), gcd(abs(i), abs(j)) | abs(i), gcd(abs(i), abs(j)) | abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(i), abs(j)) | j0 ⊦

Rule argument

Additional information

Used terms: abs(i), abs(j)

Proof step 46 from proof gcd-rec (previous step) (back to tree)

Lemma gcd-div2

Proof step 47 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 49:

  abs(i) = i0 * abs(j) + j0, j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | abs(i), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(i), abs(j)) | j0, ∃ i0. gcd(abs(i), abs(j)) * i0 = abs(j) ⊦

Rule argument

Additional information

Used terms: abs(j), gcd(abs(i), abs(j))

Proof step 48 from proof gcd-rec (previous step) (back to tree)

Lemma divides

Proof step 49 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  gcd(abs(i), abs(j)) * i1 = abs(j), abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), gcd(abs(i), abs(j)) | abs(i), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(i), abs(j)) | j0 ⊦

Rule argument

Additional information

Proof step 50 from proof gcd-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 52:

  gcd(abs(i), abs(j)) * i1 = abs(j), abs(i) = i0 * abs(j) + j0, j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(i), abs(j)) | j0, ∃ i0. gcd(abs(i), abs(j)) * i0 = abs(i) ⊦

Rule argument

Additional information

Used terms: abs(i), gcd(abs(i), abs(j))

Proof step 51 from proof gcd-rec (previous step) (back to tree)

Lemma divides

Proof step 52 from proof gcd-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  gcd(abs(i), abs(j)) * i2 = abs(i), gcd(abs(i), abs(j)) * i1 = abs(j), abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(i), abs(j)) | j0 ⊦

Rule argument

Additional information

Proof step 53 from proof gcd-rec (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 54:

  gcd(abs(i), abs(j)) * i1 = abs(j), gcd(abs(i), abs(j)) * i2 = abs(i), abs(i) = i0 * abs(j) + j0, j0 = abs(i) - i0 * abs(j), j ≠ 0, j0 < abs(j), gcd(abs(j), j0) < gcd(abs(i), abs(j)), 0 ≤ i0, 0 ≤ j0, ¬ gcd(abs(i), abs(j)) | j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i - j = i0 ↔ i = i0 + j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: j0 = abs(i) - i0 * abs(j)

Proof step 54 from proof gcd-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 55:

  gcd(abs(i), abs(j)) * i2 = abs(i), gcd(abs(i), abs(j)) * i1 = abs(j), abs(i) = i0 * abs(j) + j0, j ≠ 0, gcd(abs(j), j0) < gcd(abs(i), abs(j)), j0 < abs(j), 0 ≤ j0, 0 ≤ i0, ¬ gcd(abs(i), abs(j)) | abs(i) - i0 * abs(j) ⊦

Rule argument

Additional information

Proof step 55 from proof gcd-rec (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: divides-mult-sub: ⊦ i | i * j - j0 ↔ i | j0; gcd-divides: ⊦ gcd(i, j) | i * i0; gcd-com: ⊦ gcd(i, j) = gcd(j, i); associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult