Proof step 1 from proof divides-prime (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i | j ↔ abs(i) = j ∨ abs(i) = 1), prime(j) ⊦

Rule argument

Additional information

Proof step 2 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(i | j ↔ abs(i) = j ∨ abs(i) = 1), prime(j) ⊦

Rule argument

Additional information

Proof step 3 from proof divides-prime (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  abs(i) ≠ j, abs(i) ≠ 1, prime(j), i | j ⊦

• Proof step 24:

  prime(j), ¬ i | j, abs(i) = j ∨ abs(i) = 1 ⊦

Rule argument

Additional information

Proof step 4 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  abs(i) ≠ j, abs(i) ≠ 1, prime(j), i | j ⊦

Rule argument

Additional information

Proof step 5 from proof divides-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ prime(j) ↔ 2 ≤ j ∧ (∀ i. 1 < i ∧ i < j → ¬ i | j)

• Proof step 7:

  abs(i) ≠ j, abs(i) ≠ 1, i | j, 2 ≤ j, ∀ i. 1 < i ∧ i < j → ¬ i | j ⊦

Rule argument

Additional information

Used terms: j

Proof step 6 from proof divides-prime (previous step) (back to tree)

Lemma prime-def

Proof step 7 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  abs(i) ≠ j, abs(i) ≠ 1, 0 < j, i | j, 2 ≤ j, 0 ≤ j, ∀ i. 1 < i ∧ i < j → ¬ i | j ⊦

Rule argument

Additional information

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

Proof step 8 from proof divides-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ i | j ↔ (∃ i0. i * i0 = j)

• Proof step 10:

  abs(i) ≠ j, abs(i) ≠ 1, 0 < j, 0 ≤ j, 2 ≤ j, ∀ i. 1 < i ∧ i < j → ¬ i | j, ∃ i0. i * i0 = j ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 9 from proof divides-prime (previous step) (back to tree)

Lemma divides

Proof step 10 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  abs(i) ≠ i * i0, abs(i) ≠ 1, 0 < i * i0, 2 ≤ i * i0, 0 ≤ i * i0, ∀ i1. 1 < i1 ∧ i1 < i * i0 → ¬ i1 | i * i0 ⊦

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 11 from proof divides-prime (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  abs(i) ≠ i * i0, abs(i) ≠ 1, 0 < i * i0, 0 ≤ i * i0, 2 ≤ i * i0, 1 < i0 ∧ i0 < i * i0 → ¬ i0 | i * i0, ∀ i1. 1 < i1 ∧ i1 < i * i0 → ¬ i1 | i * i0 ⊦

Rule argument

Additional information

Used terms: i0

Proof step 12 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  abs(i) ≠ 1, abs(i) ≠ i * i0, 0 < i * i0, i0 < i * i0, 0 ≤ i * i0, 2 ≤ i * i0, i0 ≤ 1, ∀ i1. 1 < i1 ∧ i1 < i * i0 → ¬ i1 | i * i0 ⊦

Rule argument

Additional information

Used simplifier rules: div-mult: ⊦ i | i * j; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) ⊦ i * j = i ↔ i = 0 ∨ j = 1; (ws) ⊦ 0 < j → abs(j) = j; (s) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ 0 < i → (i * j ≤ i ↔ j ≤ 1); (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs

Proof step 13 from proof divides-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ i * j = j * i

• Proof step 15:

  abs(i) ≠ 1, abs(i) ≠ i0 * i, i0 < i0 * i, 0 < i0 * i, i0 ≤ 1, 2 ≤ i0 * i, 0 ≤ i0 * i, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦

Rule argument

Additional information

Used terms: i0, i

Proof step 14 from proof divides-prime (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof divides-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ 0 < i → (i < i * j ↔ 1 < j)

• Proof step 17:

  abs(i) ≠ 1, abs(i) ≠ i0 * i, 0 < i0 * i, i0 < i0 * i, 0 ≤ i0 * i, 2 ≤ i0 * i, i0 ≤ 1, ¬ 0 < i0, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 1 < i → abs(i) = i; (s) ⊦ i * j = i ↔ i = 0 ∨ j = 1; (ws) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) Used terms: i, i0

Proof step 16 from proof divides-prime (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ~1 ≠ i0, ~1 ≠ i, i ≠ 0, i0 ≠ 0, i < 0, i0 < 0, 2 ≤ i0 * i, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i < 0 → (i < i * j ↔ j < 1); (s) ⊦ i < 0 → (0 ≤ i * j ↔ j ≤ 0); (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; (ws) ⊦ i * j + i = i * (j + 1); (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i ≤ 0 → (0 < i * j ↔ j < 0 ∧ i ≠ 0); (s) j0 ≠ 0, j ≤ j0 ⊦ i ≤ (* j) → i ≤ (* j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 18 from proof divides-prime (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  ~1 ≠ i0, ~1 ≠ i, i ≠ 0, i0 ≠ 0, i0 < 0, i < 0, 2 ≤ i0 * i, 1 < abs(i0) ∧ abs(i0) < i0 * i → ¬ abs(i0) | i0 * i, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦

Rule argument

Additional information

Used terms: abs(i0)

Proof step 19 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  ~1 ≠ i0, ~1 ≠ i, i ≠ 0, i0 ≠ 0, i < 0, i0 < 0, 2 ≤ i0 * i, 1 < ~ i0 ∧ ~ i0 < i0 * i → ¬ ~ i0 | i0 * i, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦

Rule argument

Additional information

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

Proof step 20 from proof divides-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ ~ i | j ↔ i | j

• Proof step 22:

  ~1 ≠ i0, ~1 ≠ i, i ≠ 0, i0 ≠ 0, i0 < 0, i < 0, 2 ≤ i0 * i, 1 < ~ i0 ∧ ~ i0 < i0 * i → ¬ i0 | i * i0, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: i * i0, i0

Proof step 21 from proof divides-prime (previous step) (back to tree)

Lemma divides-neg

Proof step 22 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ~1 ≠ i0, ~1 ≠ i, i ≠ 0, i0 ≠ 0, i < 0, i0 < 0, 2 ≤ i0 * i, ∀ i1. 1 < i1 ∧ i1 < i0 * i → ¬ i1 | i0 * i ⊦ 1 < ~ i0 ∧ ~ i0 < i0 * i

Rule argument

Additional information

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

Proof step 23 from proof divides-prime (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i * j + i = i * (j + 1); (s) ⊦ i < 0 → (0 < i * j ↔ j < 0); (s) ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i < ~ j ↔ i + j < 0; (s)

Proof step 24 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  abs(i) = 1, 1 ≠ j, prime(j), ¬ i | j ⊦

Rule argument

Additional information

Used simplifier rules: div-abs-03: ⊦ i | abs(i);

Proof step 25 from proof divides-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  abs(i) = 1, 1 ≠ j, i < 0, prime(j), ¬ i | j ⊦

Rule argument

Additional information

Used simplifier rules: div-one: ⊦ 1 | i; Used terms: i

Proof step 26 from proof divides-prime (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof divides-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: divides-mone: ⊦ ~1 | j; forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (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 ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s)