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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i | abs(j) * j0 ↔ i | j * j0) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

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

Rule argument

Additional information

Used terms: abs(j) * j0, i

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

Lemma divides

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  ⊦ (∃ i0. i * i0 = abs(j) * j0) ↔ (∃ i0. i * i0 = j * j0)

Rule argument

Additional information

Used terms: j * j0, i

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

Lemma divides

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ∃ i0. i * i0 = abs(j) * j0 ⊦ ∃ i0. i * i0 = j * j0

• Proof step 14:

  ∃ i0. i * i0 = j * j0 ⊦ ∃ i0. i * i0 = abs(j) * j0

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  i * i0 = abs(j) * j0 ⊦ ∃ i0. i * i0 = j * j0

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  i * i0 = abs(j) * j0, i * i0 ≠ j * j0 ⊦ ∃ i0. i * i0 = j * j0

Rule argument

Additional information

Used terms: i0

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

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  i * i0 = abs(j) * j0, i * ~ i0 ≠ j * j0, i * i0 ≠ j * j0 ⊦

Rule argument

Additional information

Used terms: ~ i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  i * i0 = abs(j) * j0, i * i0 ≠ j * j0, i0 * i + j * j0 ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i = j ↔ i + j = 0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ ~ i * j = ~(i * j); (s)

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

User applied rule subst equation

And obtained the following new goals

• Proof step 12:

  i * i0 = abs(j) * j0, abs(j) * j0 ≠ j * j0, abs(j) * j0 + j * j0 ≠ 0 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ i ≠ 0 → (j * i = j0 * i ↔ j = j0)

Rule argument

Additional information

Used simplifier rules: ⊦ abs(i) = i ↔ 0 ≤ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i * j = ~(i * j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ ~ 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 ⊦ i * 0 = 0; (s) Used terms: j, j0, abs(j)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  i * i0 = j * j0 ⊦ ∃ i0. i * i0 = abs(j) * j0

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 16:

  i * i0 = j * j0, i * i0 ≠ abs(j) * j0 ⊦ ∃ i0. i * i0 = abs(j) * j0

Rule argument

Additional information

Used terms: i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  i * i0 = j * j0, j0 ≠ 0, j < 0 ⊦ ∃ i1. j * j0 + i * i1 = 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 = 0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ ~ i * j = ~(i * j); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ abs(i) = i ↔ 0 ≤ i; (s) ⊦ i ≠ 0 → (i * j = i * j0 ↔ j = j0); (s) neq-not-zero: ⊦ i * j ≠ i * j0 → i ≠ 0; (forward) from specification int-mult

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i * j = ~(i * j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + ~ j = i - j; (s) ⊦ i = j → i - j = 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: ~ i0