Proof step 1 from proof gcd-divides-both-h (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i < j, j0 | gcd(i, j), 0 ≤ i ⊦ j0 | j ∧ j0 | i

Rule argument

Additional information

Proof step 2 from proof gcd-divides-both-h (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  i < j, j0 | gcd(i, j), 0 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(j) → i < j0 ∧ j1 | gcd(i, j0) ∧ 0 ≤ i → j1 | j0 ∧ j1 | i ⊦ j0 | j ∧ j0 | i

Rule argument

Additional information

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

Proof step 3 from proof gcd-divides-both-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  i < j, 0 < j, j0 | gcd(i, j), 0 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(j) → i < j0 ∧ j1 | gcd(i, j0) ∧ 0 ≤ i → j1 | j0 ∧ j1 | i ⊦ j0 | j ∧ j0 | i

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 4 from proof gcd-divides-both-h (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  0 < j, i < j, j0 | gcd(i, j - i), 0 ≤ i, ∀ j0, i, j1. i→n(j0) < i→n(j) → i < j0 ∧ j1 | gcd(i, j0) ∧ 0 ≤ i → j1 | j0 ∧ j1 | i ⊦ j0 | j ∧ j0 | i

Rule argument

Additional information

Used terms: j, i

Proof step 5 from proof gcd-divides-both-h (previous step) (back to tree)

Lemma gcd-rec-sub-01

Proof step 6 from proof gcd-divides-both-h (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

Proof step 7 from proof gcd-divides-both-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  0 < i0 + i, 0 < i0, j0 | gcd(i, i0), 0 ≤ i, ∀ j0, i1, j1. i→n(j0) < i→n(i0 + i) → i1 < j0 ∧ j1 | gcd(i1, j0) ∧ 0 ≤ i1 → j1 | j0 ∧ j1 | i1 ⊦ j0 | i0 ∧ j0 | i

Rule argument

Additional information

Used simplifier rules: divides-add: ⊦ i | j → (i | j + j0 ↔ i | j0); forward-le-05: ⊦ 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 ⊦ i < i + j ↔ 0 < j; (s)

Proof step 8 from proof gcd-divides-both-h (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 9:

  0 < i0, 0 < i0 + i, j0 | gcd(i, i0), 0 ≤ i, ∀ j0, i1, j1. i→n(j0) < i→n(i0 + i) → i1 < j0 ∧ j1 | gcd(i1, j0) ∧ 0 ≤ i1 → j1 | j0 ∧ j1 | i1 ⊦ j0 | i0 ∧ j0 | i, i < i0 ∧ j0 | gcd(i, i0) ∧ 0 ≤ i

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); div-zero: ⊦ i | 0; ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i + j ≤ i ↔ j ≤ 0; (s) ⊦ i ≤ j → (j ≤ i ↔ i = 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 ⊦ 0 < j → abs(j) = j; (s) Used terms: i0, i, j0

Proof step 9 from proof gcd-divides-both-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  0 < i, 0 < i0, j0 | gcd(i, i0), i0 ≤ i, 0 ≤ i, ∀ j0, i1, j1. i→n(j0) < i→n(i0 + i) → i1 < j0 ∧ j1 | gcd(i1, j0) ∧ 0 ≤ i1 → j1 | j0 ∧ j1 | i1 ⊦ j0 | i0 ∧ j0 | i

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 ⊦ 0 < i ∧ 0 < j → 0 < i + j; (s) forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)

Proof step 10 from proof gcd-divides-both-h (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 11:

  0 < i0, 0 < i, j0 | gcd(i, i0), 0 ≤ i, i0 ≤ i, ¬ i→n(i) < i→n(i0 + i), ∀ j0, i1, j1. i→n(j0) < i→n(i0 + i) → i1 < j0 ∧ j1 | gcd(i1, j0) ∧ 0 ≤ i1 → j1 | j0 ∧ j1 | i1 ⊦ j0 | i0 ∧ j0 | i

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-same-01: ⊦ 0 < j → gcd(j, j) = j; ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i ≤ i; (s) Used terms: i, i0, j0

Proof step 11 from proof gcd-divides-both-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  0 < i, 0 < i0, j0 | gcd(i, i0), i0 ≤ i, 0 ≤ i, abs(i0 + i) ≤ i, ∀ j0, i1, j1. i→n(j0) < i→n(i0 + i) → i1 < j0 ∧ j1 | gcd(i1, j0) ∧ 0 ≤ i1 → j1 | j0 ∧ j1 | i1 ⊦ j0 | i0 ∧ j0 | i

Rule argument

Additional information

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

Proof step 12 from proof gcd-divides-both-h (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i + j ≤ i ↔ j ≤ 0; (s) ⊦ i < j → (j ≤ i ↔ false); (as) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i ≤ j ↔ 0 ≤ i + j; (s) ⊦ i + i = 2 * i; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i + j < j ↔ i < 0; (s) ⊦ i < j → ¬ j < i; (s) Used terms: i0 + i

Proof step 13 from proof gcd-divides-both-h (previous step) (back to tree)

A spec-lemma