Proof step 1 from proof gcd-abs-rew-02 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ ¬ i < j → (i = j ↔ ¬ j < i)

• Proof step 4:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)) ⊦

• Proof step 19:

  gcd(abs(i), abs(j)) < gcd(i, j), ¬ gcd(i, j) < gcd(abs(i), abs(j)) ⊦

Rule argument

Additional information

Used terms: gcd(abs(i), abs(j)), gcd(i, j)

Proof step 3 from proof gcd-abs-rew-02 (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)) ⊦

Rule argument

Additional information

Proof step 5 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ i0 | i ∧ i0 | j ∧ (i ≠ 0 ∨ j ≠ 0) → i0 ≤ gcd(i, j)

• Proof step 7:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | i ∧ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0) → gcd(abs(i), abs(j)) ≤ gcd(i, j) ⊦

Rule argument

Additional information

Used terms: gcd(abs(i), abs(j)), i, j

Proof step 6 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma gcd-max

Proof step 7 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)) ⊦ gcd(abs(i), abs(j)) | i ∧ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → ¬ j < i; (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 8 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ i | abs(j) → i | j

• Proof step 10:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), ¬ gcd(abs(i), abs(j)) | abs(i) ⊦ gcd(abs(i), abs(j)) | i ∧ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0)

• Proof step 13:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | abs(i) ⊦ true ∧ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used terms: i, gcd(abs(i), abs(j))

Proof step 9 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma div-abs-01

Proof step 10 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), ¬ gcd(abs(i), abs(j)) | abs(i) ⊦ gcd(abs(i), abs(j)) | i ∧ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Proof step 11 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ gcd(i, j) | i

Rule argument

Additional information

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

Proof step 12 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma gcd-div1

Proof step 13 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | abs(i) ⊦ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Proof step 14 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ i | abs(j) → i | j

• Proof step 16:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | abs(i), ¬ gcd(abs(i), abs(j)) | abs(j) ⊦ gcd(abs(i), abs(j)) | j ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used simplifier rules: gcd-zero: ⊦ gcd(0, 0) = 0; Used terms: j, gcd(abs(i), abs(j))

Proof step 15 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma div-abs-01

Proof step 16 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  gcd(i, j) ≠ gcd(abs(i), abs(j)), gcd(i, j) < gcd(abs(i), abs(j)), gcd(abs(i), abs(j)) | abs(i), ¬ gcd(abs(i), abs(j)) | abs(j), ¬ gcd(abs(i), abs(j)) | j ⊦

Rule argument

Additional information

Proof step 17 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ gcd(i, j) | j

Rule argument

Additional information

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

Proof step 18 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma gcd-div2

Proof step 19 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → ¬ j < i; (s)

Proof step 20 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 21:

  ⊦ i0 | i ∧ i0 | j ∧ (i ≠ 0 ∨ j ≠ 0) → i0 ≤ gcd(i, j)

• Proof step 22:

  gcd(abs(i), abs(j)) < gcd(i, j), gcd(i, j) | abs(i) ∧ gcd(i, j) | abs(j) ∧ (abs(i) ≠ 0 ∨ abs(j) ≠ 0) → gcd(i, j) ≤ gcd(abs(i), abs(j)) ⊦

Rule argument

Additional information

Used terms: gcd(i, j), abs(i), abs(j)

Proof step 21 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma gcd-max

Proof step 22 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  gcd(abs(i), abs(j)) < gcd(i, j) ⊦ gcd(i, j) | abs(i) ∧ gcd(i, j) | abs(j) ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → (j ≤ i ↔ false); (as) ⊦ abs(i) = 0 ↔ i = 0; (s)

Proof step 23 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ i | abs(j) ↔ i | j

• Proof step 25:

  gcd(abs(i), abs(j)) < gcd(i, j) ⊦ gcd(i, j) | i ∧ gcd(i, j) | abs(j) ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used terms: i, gcd(i, j)

Proof step 24 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma div-abs-02

Proof step 25 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ i | abs(j) ↔ i | j

• Proof step 27:

  gcd(abs(i), abs(j)) < gcd(i, j) ⊦ gcd(i, j) | i ∧ gcd(i, j) | j ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used terms: j, gcd(i, j)

Proof step 26 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma div-abs-02

Proof step 27 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ gcd(i, j) | j

• Proof step 29:

  gcd(abs(i), abs(j)) < gcd(i, j) ⊦ gcd(i, j) | i ∧ true ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Used terms: j, i

Proof step 28 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma gcd-div2

Proof step 29 from proof gcd-abs-rew-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  gcd(abs(i), abs(j)) < gcd(i, j) ⊦ gcd(i, j) | i ∧ (i ≠ 0 ∨ j ≠ 0)

Rule argument

Additional information

Proof step 30 from proof gcd-abs-rew-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ gcd(i, j) | i

Rule argument

Additional information

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

Proof step 31 from proof gcd-abs-rew-02 (previous step) (back to tree)

Lemma gcd-div1