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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i = j ↔ true), i | j, j | i, i ≤ 0, j ≤ 0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i ≠ j, j | i, i | j, j ≤ 0, i ≤ 0 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  i ≠ j, j | i, i ≤ 0, j ≤ 0, ∃ i0. i * i0 = j ⊦

Rule argument

Additional information

Used terms: j, i

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

Lemma divides

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  i ≠ 0, i0 ≠ 1, i < 0, i * i0 | i, 0 ≤ i0 ⊦

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 forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (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 < 0 → (i * j ≤ 0 ↔ 0 ≤ j); (s) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i * j = i ↔ i = 0 ∨ j = 1; (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

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

Lemma divides