Proof step 1 from proof gcdhex (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof gcdhex (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

Proof step 3 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

Proof step 4 from proof gcdhex (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 5:

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

• Proof step 7:

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

Rule argument

Additional information

Used formulas: j = 0

Proof step 5 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

Proof step 6 from proof gcdhex (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ 1 * i = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 1

Proof step 7 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

Proof step 8 from proof gcdhex (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

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

Rule argument

Additional information

Used terms: j, i

Proof step 9 from proof gcdhex (previous step) (back to tree)

Lemma gcd-rec

Proof step 10 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

Proof step 11 from proof gcdhex (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 12:

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

• Proof step 14:

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

Rule argument

Additional information

Used formulas: i = j

Proof step 12 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: gcd-zero-03: ⊦ i ≠ 0 → gcd(i, 0) = abs(i); gcd-same-01: ⊦ 0 < j → gcd(j, j) = j; ⊦ i ≤ i; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 < j → abs(j) = j; (s) i ≠ 0 ⊦ i % i = 0; (s)

Proof step 13 from proof gcdhex (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ i * 0 = 0; (s) ⊦ 1 * i = i; (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 terms: 0, 1

Proof step 14 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 15 from proof gcdhex (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 16:

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

• Proof step 19:

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

Rule argument

Additional information

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

Proof step 16 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

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 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i % j; (s)

Proof step 17 from proof gcdhex (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ j ≤ i0 ∧ 0 < j → ¬ i0 < i % j

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ i; (s) Used terms: j, i, j

Proof step 18 from proof gcdhex (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Proof step 20 from proof gcdhex (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  j ≠ 0 ⊦ i % j = i - i / j * j

• Proof step 22:

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

Rule argument

Additional information

Used terms: j, i

Proof step 21 from proof gcdhex (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof gcdhex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof gcdhex (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ (i - j) * j0 = i * j0 - j * j0

• Proof step 25:

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

Rule argument

Additional information

Used terms: j0, i / j * j, i

Proof step 24 from proof gcdhex (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof gcdhex (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 26:

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

• Proof step 28:

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

Rule argument

Additional information

Used formulas: j * i1 + (i * j0 - (i / j * j) * j0) = i * j0 + j * (i1 - i / j * j0)

Proof step 26 from proof gcdhex (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Proof step 27 from proof gcdhex (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: j0, i1 - i / j * j0

Proof step 28 from proof gcdhex (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ (i - j) * j0 = i * j0 - j * j0

Rule argument

Additional information

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

Proof step 29 from proof gcdhex (previous step) (back to tree)

A spec-lemma