Proof step 1 from proof gcd-rec-sub-03 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  j = i0 + i, gcd(i, j) ≠ gcd(j, i0) ⊦

Rule argument

Additional information

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

Proof step 3 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0) ⊦

Rule argument

Additional information

Proof step 4 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i)

• Proof step 6:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0) ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: ⊦ i + j - i = j; (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: i0 + i, i

Proof step 5 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub-02

Proof step 6 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0) ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Proof step 7 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i < 0 ⊦ 0 < i ∧ i < i0 + i

• Proof step 51:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), ¬ i < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used formulas: i < 0

Proof step 8 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

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

Proof step 9 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: i0 + i, i

Proof step 10 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-abs-rew-02

Proof step 11 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 12:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i < 0, i0 < 0 ⊦ 0 < i ∧ i < i0 + i

• Proof step 18:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i < 0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used formulas: i0 < 0

Proof step 12 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i)

• Proof step 14:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i0 < 0, i < 0 ⊦ 0 < i ∧ i < i0 + i, 0 < abs(i) ∧ abs(i) < abs(i0 + i)

• Proof step 16:

  gcd(abs(i0 + i), abs(i0 + i) - abs(i)) ≠ gcd(i0 + i, i0), i0 < 0, i < 0, 0 < abs(i), abs(i) < abs(i0 + i) ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: abs(i0 + i), abs(i)

Proof step 13 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub-02

Proof step 14 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < j → ¬ j < i; (s) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i + ~ j = ~(i + j); (s) ⊦ ~ j < ~ i ↔ i < j; (s) ⊦ i + j < j ↔ 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 Used terms: i, i0

Proof step 15 from proof gcd-rec-sub-03 (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ ~ i + ~ j = ~(i + j); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i - ~ j = j - i; (s) ⊦ i - j + i = ~ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i - ~ j = i + j; (s) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: i, i0

Proof step 17 from proof gcd-rec-sub-03 (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i < 0, abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

• Proof step 33:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used formulas: abs(i) < i0

Proof step 19 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 20:

  abs(i0 + i) = i0 - abs(i), gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), abs(i) < i0, i < 0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ i - ~ j = i + j; (s) ⊦ abs(i) = i ↔ 0 ≤ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j → ¬ j < i; (s) Used formulas: abs(i0 + i) = i0 - abs(i)

Proof step 20 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 21:

  gcd(abs(i), i0 - abs(i)) ≠ gcd(i0 + i, i0), i < 0, abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Proof step 21 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  gcd(abs(i), i0 - abs(i)) ≠ gcd(abs(i0 + i), abs(i0)), abs(i) < i0, i < 0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: i0, i0 + i

Proof step 22 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-abs-rew-02

Proof step 23 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  abs(i0 + i) = i0 - abs(i), gcd(abs(i), i0 - abs(i)) ≠ gcd(abs(i0 + i), abs(i0)), i < 0, abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); ⊦ abs(i) = i ↔ 0 ≤ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i - ~ j = i + j; (s) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j → ¬ j < i; (s) Used formulas: abs(i0 + i) = i0 - abs(i)

Proof step 24 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 25:

  gcd(abs(i), i0 - abs(i)) ≠ gcd(i0 - abs(i), abs(i0)), abs(i) < i0, i < 0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Proof step 25 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i)

• Proof step 27:

  gcd(abs(i), i0 - abs(i)) ≠ gcd(abs(i0), abs(i0) - (i0 - abs(i))), i < 0, abs(i) < i0, 0 < i0 - abs(i), i0 - abs(i) < abs(i0), ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

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

Proof step 26 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub-02

Proof step 27 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  abs(i0) - (i0 - abs(i)) = abs(i), gcd(abs(i), i0 - abs(i)) ≠ gcd(abs(i0), abs(i0) - (i0 - abs(i))), i0 - abs(i) < abs(i0), 0 < i0 - abs(i), abs(i) < i0, i < 0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i - ~ j = i + j; (s) ⊦ i - j + i = ~ j; (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 → abs(i) = ~ i; (s) ⊦ ~ i = ~ j ↔ i = j; (s) Used formulas: abs(i0) - (i0 - abs(i)) = abs(i)

Proof step 28 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 29:

  gcd(abs(i), i0 - abs(i)) ≠ gcd(abs(i0), abs(i)), i < 0, abs(i) < i0, 0 < i0 - abs(i), i0 - abs(i) < abs(i0), ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Proof step 29 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  gcd(abs(i), i0 - abs(i)) ≠ gcd(abs(i), abs(i0)), i0 - abs(i) < abs(i0), 0 < i0 - abs(i), abs(i) < i0, i < 0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: abs(i), abs(i0)

Proof step 30 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-com

Proof step 31 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(i, j - i)

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i - ~ j = i + j; (s) ⊦ i + j < j ↔ 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 ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) Used terms: abs(i0), abs(i)

Proof step 32 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub

Proof step 33 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: i0, i0 + i

Proof step 34 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-abs-rew-02

Proof step 35 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 36:

  abs(i0 + i) = abs(i) - abs(i0), gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); ⊦ ~ i - j = ~(i + j); (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ abs(i) + i = 0 ↔ i ≤ 0; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) 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) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) Used formulas: abs(i0 + i) = abs(i) - abs(i0)

Proof step 36 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 37:

  gcd(abs(i), abs(i) - abs(i0)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Proof step 37 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

  gcd(abs(i) - abs(i0), abs(i)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: abs(i) - abs(i0), abs(i)

Proof step 38 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-com

Proof step 39 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i)

• Proof step 41:

  gcd(abs(i) - abs(i0), abs(i)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i, 0 < abs(i) - abs(i0) ∧ abs(i) - abs(i0) < abs(i)

• Proof step 45:

  gcd(abs(i), abs(i) - (abs(i) - abs(i0))) ≠ gcd(abs(i) - abs(i0), abs(i0)), i < 0, 0 < abs(i) - abs(i0), abs(i) - abs(i0) < abs(i), ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: abs(i), abs(i) - abs(i0)

Proof step 40 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub-02

Proof step 41 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 42:

  gcd(abs(i) - abs(i0), abs(i)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i < 0, ¬ abs(i) - abs(i0) < abs(i), ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs 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 ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ ~ i = j ↔ i + j = 0; (s)

Proof step 42 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  i + gcd(i, i) ≠ 0, i < 0 ⊦ 0 < i ∧ i < i

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); 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) ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i + j ≤ i ↔ j ≤ 0; (s) ⊦ ~ j < ~ i ↔ i < j; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ ¬ j < 0 → abs(j) = j; (s)

Proof step 43 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

Rule argument

Additional information

Used simplifier rules: gcd-zero: ⊦ gcd(0, 0) = 0; ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i + 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 Used terms: i

Proof step 44 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-same

Proof step 45 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 46:

  abs(i) - (abs(i) - abs(i0)) = abs(i0), gcd(abs(i), abs(i) - (abs(i) - abs(i0))) ≠ gcd(abs(i) - abs(i0), abs(i0)), abs(i) - abs(i0) < abs(i), 0 < abs(i) - abs(i0), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ ~ i - ~ j = j - i; (s) ⊦ i + j - i = j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ ¬ j < 0 → abs(j) = j; (s) Used formulas: abs(i) - (abs(i) - abs(i0)) = abs(i0)

Proof step 46 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 47:

  gcd(abs(i), abs(i0)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i < 0, 0 < abs(i) - abs(i0), abs(i) - abs(i0) < abs(i), ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Proof step 47 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

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

• Proof step 49:

  gcd(abs(i0), abs(i)) ≠ gcd(abs(i) - abs(i0), abs(i0)), abs(i) - abs(i0) < abs(i), 0 < abs(i) - abs(i0), i < 0, ¬ abs(i) < i0, ¬ i0 < 0 ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used terms: abs(i0), abs(i)

Proof step 48 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-com

Proof step 49 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(i, j - i)

Rule argument

Additional information

Used simplifier rules: gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ ~ j < ~ i ↔ i < j; (s) ⊦ i < i + j ↔ 0 < j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ ~ i - j = ~(i + j); (s) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j → ¬ j < i; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i < ~ j ↔ i + j < 0; (s) Used terms: abs(i), abs(i0)

Proof step 50 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub

Proof step 51 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), 0 ≤ i ⊦ 0 < i ∧ i < i0 + i

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 52 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 53:

  i = 0, gcd(i, i0 + i) ≠ gcd(i0 + i, i0), 0 ≤ i ⊦ 0 < i ∧ i < i0 + i

• Proof step 56:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, 0 ≤ i ⊦ 0 < i ∧ i < i0 + i

Rule argument

Additional information

Used formulas: i = 0

Proof step 53 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  abs(i0) ≠ gcd(i0, i0) ⊦

Rule argument

Additional information

Used simplifier rules: gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, 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)

Proof step 54 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

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

Rule argument

Additional information

Used simplifier rules: gcd-zero: ⊦ gcd(0, 0) = 0; Used terms: i0

Proof step 55 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-same

Proof step 56 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, 0 < i, ¬ i < i0 + i ⊦

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)

Proof step 57 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ i ≥ j ↔ ¬ i < j

• Proof step 59:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, 0 < i, i ≥ i0 + i ⊦

Rule argument

Additional information

Used terms: i0 + i, i

Proof step 58 from proof gcd-rec-sub-03 (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, 0 < i, i0 < i, i0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) 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) ⊦ i ≥ j ↔ ¬ i < j; (s)

Proof step 60 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 61:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, i0 < i, 0 < i, i0 ≤ 0 ⊦

Rule argument

Additional information

Used formulas: i = 0

Proof step 61 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, 0 < i, i0 < i, i0 ≤ 0 ⊦

Rule argument

Additional information

Proof step 62 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 63:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, i0 ≠ 0, i0 < i, 0 < i, i0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: gcd-same: ⊦ i ≠ 0 → gcd(i, i) = abs(i); gcd-zero-03: ⊦ i ≠ 0 → gcd(i, 0) = abs(i); ⊦ 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 formulas: i0 = 0

Proof step 63 from proof gcd-rec-sub-03 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  gcd(i, i0 + i) ≠ gcd(i0 + i, i0), i ≠ 0, i0 ≠ 0, 0 < i, i0 < i, i0 < 0 ⊦

Rule argument

Additional information

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

Proof step 64 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

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

• Proof step 66:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(i0 + i, i0), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i ⊦

Rule argument

Additional information

Used terms: i0 + i, i

Proof step 65 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-abs-rew-02

Proof step 66 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

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

• Proof step 68:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i ≠ 0, i0 ≠ 0, 0 < i, i0 < i, i0 < 0 ⊦

Rule argument

Additional information

Used terms: i0, i0 + i

Proof step 67 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-abs-rew-02

Proof step 68 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 69:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i, abs(i0) < abs(i) ⊦

• Proof step 81:

  gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i, ¬ abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used formulas: abs(i0) < abs(i)

Proof step 69 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 70:

  abs(i0 + i) = abs(i) - abs(i0), gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i ≠ 0, i0 ≠ 0, abs(i0) < abs(i), 0 < i, i0 < i, i0 < 0 ⊦

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ i - ~ j = i + j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ abs(i) = i ↔ 0 ≤ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j → ¬ j < i; (s) Used formulas: abs(i0 + i) = abs(i) - abs(i0)

Proof step 70 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 71:

  gcd(abs(i), abs(i) - abs(i0)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i, abs(i0) < abs(i) ⊦

Rule argument

Additional information

Proof step 71 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  gcd(abs(i) - abs(i0), abs(i)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i ≠ 0, i0 ≠ 0, abs(i0) < abs(i), 0 < i, i0 < i, i0 < 0 ⊦

Rule argument

Additional information

Used terms: abs(i) - abs(i0), abs(i)

Proof step 72 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-com

Proof step 73 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i)

• Proof step 75:

  gcd(abs(i), abs(i) - (abs(i) - abs(i0))) ≠ gcd(abs(i) - abs(i0), abs(i0)), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i, abs(i0) < abs(i), 0 < abs(i) - abs(i0), abs(i) - abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i - ~ j = i + j; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i + j < j ↔ 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 Used terms: abs(i), abs(i) - abs(i0)

Proof step 74 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub-02

Proof step 75 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ i - (i - j) = j

• Proof step 77:

  gcd(abs(i), abs(i0)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i ≠ 0, i0 ≠ 0, abs(i) - abs(i0) < abs(i), 0 < abs(i) - abs(i0), abs(i0) < abs(i), 0 < i, i0 < i, i0 < 0 ⊦

Rule argument

Additional information

Used terms: abs(i0), abs(i)

Proof step 76 from proof gcd-rec-sub-03 (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

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

• Proof step 79:

  gcd(abs(i0), abs(i)) ≠ gcd(abs(i) - abs(i0), abs(i0)), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i, abs(i0) < abs(i), 0 < abs(i) - abs(i0), abs(i) - abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used terms: abs(i0), abs(i)

Proof step 78 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-com

Proof step 79 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(i, j - i)

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ i - ~ j = i + j; (s) ⊦ i + j < j ↔ 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 ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) Used terms: abs(i), abs(i0)

Proof step 80 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub

Proof step 81 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 82:

  abs(i0 + i) = abs(i0) - abs(i), gcd(abs(i), abs(i0 + i)) ≠ gcd(abs(i0 + i), abs(i0)), i ≠ 0, i0 ≠ 0, 0 < i, i0 < i, i0 < 0, ¬ abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ ~ i - j = ~(i + j); (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ abs(i) + i = 0 ↔ i ≤ 0; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) 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) ⊦ 0 < j → abs(j) = j; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) Used formulas: abs(i0 + i) = abs(i0) - abs(i)

Proof step 82 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 83:

  gcd(abs(i), abs(i0) - abs(i)) ≠ gcd(abs(i0) - abs(i), abs(i0)), i ≠ 0, i0 ≠ 0, i0 < 0, i0 < i, 0 < i, ¬ abs(i0) < abs(i) ⊦

Rule argument

Additional information

Proof step 83 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(j, j - i)

• Proof step 85:

  gcd(abs(i), abs(i0) - abs(i)) ≠ gcd(abs(i0), abs(i0) - (abs(i0) - abs(i))), i ≠ 0, i0 ≠ 0, 0 < i, i0 < i, i0 < 0, 0 < abs(i0) - abs(i), abs(i0) - abs(i) < abs(i0), ¬ abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); gcd-zero-03: ⊦ i ≠ 0 → gcd(i, 0) = abs(i); ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ ~ j < ~ i ↔ i < j; (s) ⊦ i + j ≤ i ↔ j ≤ 0; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < 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 < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs ⊦ 0 < j → abs(j) = j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i = j ↔ i + j = 0; (s) Used terms: abs(i0), abs(i0) - abs(i)

Proof step 84 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub-02

Proof step 85 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  ⊦ i - (i - j) = j

• Proof step 87:

  gcd(abs(i), abs(i0) - abs(i)) ≠ gcd(abs(i0), abs(i)), i ≠ 0, i0 ≠ 0, abs(i0) - abs(i) < abs(i0), 0 < abs(i0) - abs(i), i0 < 0, i0 < i, 0 < i, ¬ abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used terms: abs(i), abs(i0)

Proof step 86 from proof gcd-rec-sub-03 (previous step) (back to tree)

A spec-lemma

Proof step 87 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

• Proof step 89:

  gcd(abs(i), abs(i0) - abs(i)) ≠ gcd(abs(i), abs(i0)), i ≠ 0, i0 ≠ 0, 0 < i, i0 < i, i0 < 0, 0 < abs(i0) - abs(i), abs(i0) - abs(i) < abs(i0), ¬ abs(i0) < abs(i) ⊦

Rule argument

Additional information

Used terms: abs(i), abs(i0)

Proof step 88 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-com

Proof step 89 from proof gcd-rec-sub-03 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 90:

  ⊦ 0 < i ∧ i < j → gcd(i, j) = gcd(i, j - i)

Rule argument

Additional information

Used simplifier rules: gcd-neg: ⊦ gcd(~ i, j) = gcd(i, j); gcd-com: ⊦ gcd(i, j) = gcd(j, i); ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ ~ j < ~ i ↔ i < j; (s) ⊦ 0 < i → i1 < i1 + 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 < j ↔ 0 < j + i; (s) ⊦ i < j → ¬ j < i; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i < ~ j ↔ i + j < 0; (s) Used terms: abs(i0), abs(i)

Proof step 90 from proof gcd-rec-sub-03 (previous step) (back to tree)

Lemma gcd-rec-sub