Proof step 1 from proof gcd-one (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ gcd(i, j) = 1 ↔ ¬(∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j)

Rule argument

Additional information

Used simplifier rules: ⊦ i > j ↔ j < i; (s)

Proof step 2 from proof gcd-one (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  gcd(i, j) = 1, ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j ⊦

• Proof step 9:

  gcd(i, j) ≠ 1 ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

Rule argument

Additional information

Proof step 3 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  gcd(i, j) = 1, 0 < i1, 1 < i1, i1 | i, i1 | j ⊦

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

Proof step 4 from proof gcd-one (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  gcd(i, j) = 1, 1 < i1, 0 < i1, i1 | j, i1 | i, i1 | i ∧ i1 | j ∧ 0 ≠ i → i1 ≤ gcd(i, j) ⊦

Rule argument

Additional information

Used terms: i1, i, j

Proof step 5 from proof gcd-one (previous step) (back to tree)

Lemma gcd-less

Proof step 6 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  abs(j) = 1, i1 ≠ 1, 0 < i1, 1 < i1, i1 | j ⊦

Rule argument

Additional information

Used simplifier rules: div-one: ⊦ 1 | i; gcd-zero-04: ⊦ gcd(i, 0) = abs(i); gcd-com: ⊦ gcd(i, j) = gcd(j, i); div-zero: ⊦ i | 0; ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s)

Proof step 7 from proof gcd-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: div-one-one: ⊦ i | 1 ↔ i = 1 ∨ i = ~1; div-one-neg-pos: ⊦ 0 < i → (i | ~1 ↔ i = 1); ⊦ 0 - i = ~ i; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs Used terms: j

Proof step 8 from proof gcd-one (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  gcd(i, j) ≠ 1 ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

Rule argument

Additional information

Proof step 10 from proof gcd-one (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  gcd(i, j) ≠ 1 ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j, 1 < gcd(i, j) ∧ gcd(i, j) | i ∧ gcd(i, j) | j

Rule argument

Additional information

Used terms: gcd(i, j)

Proof step 11 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  gcd(i, j) ≠ 1 ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j, 1 < gcd(i, j) ∧ gcd(i, j) | i ∧ gcd(i, j) | j

Rule argument

Additional information

Proof step 12 from proof gcd-one (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  gcd(i, j) ≠ 1, ¬ 1 < gcd(i, j) ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

• Proof step 15:

  gcd(i, j) ≠ 1, ¬ gcd(i, j) | i ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

• Proof step 18:

  gcd(i, j) ≠ 1, ¬ gcd(i, j) | j ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

Rule argument

Additional information

Proof step 13 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ⊦ ∃ i1. 1 < i1

Rule argument

Additional information

Used simplifier rules: gcd-less-eq-zero: ⊦ gcd(i, j) ≤ 0 ↔ gcd(i, j) = 0; gcd-zero-zero: ⊦ gcd(i, j) = 0 ↔ i = 0 ∧ j = 0; gcd-zero: ⊦ gcd(0, 0) = 0; div-zero: ⊦ i | 0; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss)

Proof step 14 from proof gcd-one (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: 1 +1

Proof step 15 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  gcd(i, j) ≠ 1, ¬ gcd(i, j) | i ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

Rule argument

Additional information

Proof step 16 from proof gcd-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ gcd(i, j) | i

Rule argument

Additional information

Used terms: j, i

Proof step 17 from proof gcd-one (previous step) (back to tree)

Lemma gcd-div1

Proof step 18 from proof gcd-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  gcd(i, j) ≠ 1, ¬ gcd(i, j) | j ⊦ ∃ i1. 1 < i1 ∧ i1 | i ∧ i1 | j

Rule argument

Additional information

Proof step 19 from proof gcd-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ gcd(i, j) | j

Rule argument

Additional information

Used terms: j, i

Proof step 20 from proof gcd-one (previous step) (back to tree)

Lemma gcd-div2