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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

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

Rule argument

Additional information

Used terms: j, i

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

Lemma gcdex-pos

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

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

User applied rule induction

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: i→n(i0)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used terms: i0, j0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (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

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

User applied rule apply induction

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: i1, i, j, j1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

Proof step 11 from proof gcdex-smallest-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 ≤ j → i ≤ j; (s) Used terms: i2, j2