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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i1, 0 < i, 0 ≤ j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i, 0 < i1, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: 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

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

User applied rule induction

And obtained the following new goals

• Proof step 4:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i, 0 < i1, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: i→n(j * i1 + i * i1)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i1, 0 < i, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i, 0 < i1, i < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

• Proof step 27:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i, 0 < i1, 0 ≤ j, ¬ i < j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used formulas: i < j

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 1 < j, 0 < i, 0 < i1, i < j, 0 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  gcd(j * i1, i * i1) ≠ gcd(i, j) * i1, 0 < j, i < j, 0 < i1, 0 < i, 1 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: j * i1, i * i1

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

Lemma gcd-com

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  i * i1 ≠ 0, gcd(abs(i * i1), abs(j * i1) % abs(i * i1)) ≠ gcd(i, j) * i1, 1 < j, 0 < i, 0 < i1, i < j, 0 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: gcd-zero: ⊦ gcd(0, 0) = 0; ⊦ 0 < i → (i * j = 0 ↔ j = 0); (s) ⊦ i * 0 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i * i1, j * i1

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

Lemma gcd-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j) * i1, i ≠ 0, i1 ≠ 0, 0 < j, i < j, 0 < i1, 0 < i, 1 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult 0 ≠ j, i0 ≠ 0 ⊦ (i0 * i) % (i0 * j) = i % j * i0; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  gcd(i * i1, j % i * i1) ≠ gcd(j, i) * i1, i ≠ 0, i1 ≠ 0, 1 < j, 0 < i, 0 < i1, i < j, 0 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: j, i

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

Lemma gcd-com

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  gcd(i * i1, j % i * i1) ≠ gcd(abs(i), abs(j) % abs(i)) * i1, i ≠ 0, i1 ≠ 0, 0 < j, i < j, 0 < i1, 0 < i, 1 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: i, j

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

Lemma gcd-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 1 < j, 0 < i, 0 < i1, i < j, 0 < j, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j → abs(j) = j; (s)

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

User applied rule apply induction

And obtained the following new goals

• Proof step 18:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 0 < j, i < j, 0 < i1, 0 < i, 1 < j, 0 ≤ j, ¬ i→n(j % i * i1 + i * i1) < i→n(j * i1 + i * i1), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s) Used terms: j % i, i1, i

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 1 < j, 0 < i, 0 < i1, i < j, 0 < j, 0 ≤ j, abs(j * i1 + i * i1) ≤ abs(j % i * i1 + i * i1), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ 0 ≤ i ∧ 0 ≤ j → abs(i + j) = abs(i) + abs(j)

• Proof step 21:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 0 < j, i < j, 0 < i1, 0 < i, 1 < j, abs(j * i1) + abs(i * i1) ≤ abs(j % i * i1 + i * i1), 0 ≤ j, 0 ≤ j * i1, 0 ≤ i * i1, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: i * i1, j * i1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 1 < j, 0 < i, i < j, 0 < j, 0 < i1, 0 ≤ j, j * i1 + i * i1 ≤ abs(j % i * i1 + i * i1), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ 0 ≤ i ∧ 0 ≤ j → abs(i + j) = abs(i) + abs(j)

• Proof step 24:

  gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 0 < i1, 0 < j, i < j, 0 < i, 1 < j, j * i1 + i * i1 ≤ abs(j % i * i1) + abs(i * i1), 0 ≤ j, 0 ≤ j % i * i1, 0 ≤ i * i1, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: i * i1, j % i * i1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  j % i ≠ 0, gcd(i * i1, j % i * i1) ≠ gcd(i, j % i) * i1, i ≠ 0, i1 ≠ 0, 1 < abs(j % i), 1 < j, 0 < i, i < j, 0 < j, 0 < i1, i < abs(j % i), 0 ≤ j, j ≤ abs(j % i), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < abs(i) ↔ i ≠ 0; (s) forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ 0 ≤ abs(i); (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ i + j ≤ i0 + j ↔ i ≤ i0; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ ¬ j < 0 → abs(j) = j

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ 0 < i ∧ 0 ≤ j → (j ≤ j % i ↔ j < i); (s) ⊦ i < j → ¬ j < i; (s) ⊦ 0 < j ∧ 0 ≤ i → ¬ i % j < 0; (s) Used terms: j % i

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  gcd(i * i1, j * i1) ≠ gcd(i, j) * i1, 0 < i1, 0 < i, 0 ≤ j, j ≤ i, 0 ≤ i, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  j * i1 ≠ 0, gcd(abs(j * i1), abs(i * i1) % abs(j * i1)) ≠ gcd(i, j) * i1, 0 < i, 0 < i1, 0 ≤ i, j ≤ i, 0 ≤ j, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); ⊦ 0 < i → (i * j = 0 ↔ j = 0); (s) ⊦ i * 0 = 0; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ 0 < i → (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 Used terms: j * i1, i * i1

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

Lemma gcd-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  gcd(j * i1, i % j * i1) ≠ gcd(i, j) * i1, i1 ≠ 0, j ≠ 0, 0 < i1, 0 < i, 0 < j, j ≤ i, 0 ≤ i, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult 0 ≠ j, i0 ≠ 0 ⊦ (i0 * i) % (i0 * j) = i % j * i0; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

  gcd(j * i1, i % j * i1) ≠ gcd(abs(j), abs(i) % abs(j)) * i1, i1 ≠ 0, j ≠ 0, 0 < j, 0 < i, 0 < i1, 0 ≤ i, j ≤ i, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used terms: j, i

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

Lemma gcd-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < i1, 0 < i, 0 < j, j ≤ i, 0 ≤ i, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j → abs(j) = j; (s)

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

User applied rule apply induction

And obtained the following new goals

• Proof step 35:

  gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < j, 0 < i, 0 < i1, 0 ≤ i, j ≤ i, ¬ i→n(i % j * i1 + j * i1) < i→n(j * i1 + i * i1), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s) Used terms: i % j, i1, j

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < i1, 0 < i, 0 < j, j ≤ i, 0 ≤ i, abs(j * i1 + i * i1) ≤ abs(i % j * i1 + j * i1), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ 0 ≤ i ∧ 0 ≤ j → abs(i + j) = abs(i) + abs(j)

• Proof step 38:

  gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < j, 0 < i, 0 < i1, abs(j * i1) + abs(i * i1) ≤ abs(i % j * i1 + j * i1), 0 ≤ i, j ≤ i, 0 ≤ j * i1, 0 ≤ i * i1, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: i * i1, j * i1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < i, 0 < j, 0 < i1, j ≤ i, 0 ≤ i, j * i1 + i * i1 ≤ abs(i % j * i1 + j * i1), ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ 0 ≤ i ∧ 0 ≤ j → abs(i + j) = abs(i) + abs(j)

• Proof step 41:

  gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < i1, 0 < j, 0 < i, j * i1 + i * i1 ≤ abs(i % j * i1) + abs(j * i1), 0 ≤ i, j ≤ i, 0 ≤ i % j * i1, 0 ≤ j * i1, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: j * i1, i % j * i1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  i % j ≠ 0, gcd(j * i1, i % j * i1) ≠ gcd(j, i % j) * i1, i1 ≠ 0, j ≠ 0, 0 < i1, 0 < j, 0 < i, j ≤ abs(i % j), i ≤ abs(i % j), 0 ≤ i, j ≤ i, ∀ j0, i0, i2. i→n(j0 * i0 + i2 * i0) < i→n(j * i1 + i * i1) → gcd(i2 * i0, j0 * i0) ≠ gcd(i2, j0) * i0 ∧ 0 < i2 ∧ 0 < i0 ∧ 0 ≤ j0 → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ abs(i); (s) ⊦ 0 < abs(i) ↔ i ≠ 0; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ i + j ≤ i0 + j ↔ i ≤ i0; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(i * j) = abs(i) * abs(j); (s) ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ ¬ j < 0 → abs(j) = j

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ 0 < j → ¬ j ≤ i % j; (s) ⊦ 0 < j ∧ 0 ≤ i → ¬ i % j < 0; (s) Used terms: i % j

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

A spec-lemma