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

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

  ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0

• Proof step 3:

  j ≠ 0, ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

Used terms: i, j

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

Lemma gcdex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  gcd(i, j) = i * i0 + j * j0, j ≠ 0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  gcd(i, j) = i * i0 + j * j0 ⊦ ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i)

• Proof step 6:

  gcd(i, j) = i * i0 + j * j0, j ≠ 0, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

Used terms: i, j, i0, j0

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

Lemma gcdex-not-unique

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

User applied rule exists right

And obtained the following new goals

• Proof step 7:

  gcd(i, j) = i * i0 + j * j0, j ≠ 0, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0, gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

Used terms: i0, j0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gcd(i, j) = i * i0 + j * j0, j ≠ 0, ¬ 0 ≤ i0, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

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

• Proof step 15:

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

Rule argument

Additional information

Used formulas: j < 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  gcd(i, j) = i * i0 + j * j0, j ≠ 0, j < 0, i0 < 0, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used terms: abs(i0)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gcd(i, j) = i * i0 + j * j0, gcd(i, j) = i * i0 * (j + 1) + j * (j0 - i0 * i), j ≠ 0, j < 0, i0 < 0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ 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 ⊦ ~ i * j = ~(i * j); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i * j + i = i * (j + 1); (s) ⊦ i - ~ j = i + j; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  gcd(i, j) = i * i0 * (j + 1) + j * i1, gcd(i, j) = i * i0 + j * j0, j0 = i1 + i0 * i, j ≠ 0, i0 < 0, j < 0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: j0, i0 * i, i1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  gcd(i, j) = i * i0 + j * (i1 + i0 * i), gcd(i, j) = i * i0 * (j + 1) + j * i1, j ≠ 0, j < 0, i0 < 0 ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 → (0 ≤ i * j ↔ j ≤ 0); (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ ~1 ↔ i < 0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: (j + 1) * i0, i1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  gcd(i, j) = i * i0 + j * j0, 0 < j, ¬ 0 ≤ i0, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); ⊦ i * 0 = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + 0 = i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: j = 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  gcd(i, j) = i * i0 + j * j0, j ≠ 0, 0 < j, i0 < 0, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 19:

  gcd(i, j) = i * i0 + j * j0, gcd(i, j) = i * (i0 - i0 * j) + j * (j0 + i0 * i), j ≠ 0, i0 < 0, 0 < j, ∀ i1. gcd(i, j) = i * (i0 - i1 * j) + j * (j0 + i1 * i) ⊦ ∃ i0, j0. gcd(i, j) = i * i0 + j * j0 ∧ 0 ≤ i0

Rule argument

Additional information

Used terms: i0

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i + 0 = i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i < 0 → (i * j ≤ i ↔ 1 ≤ j); (s) ⊦ 1 ≤ i ↔ 0 < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i0 - i0 * j, j0 + i0 * i