Proof step 1 from proof div2-neg-odd (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (j * 2 - 1) / 2 ≠ j, j < 0 ⊦

Rule argument

Additional information

Proof step 2 from proof div2-neg-odd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (j * 2 - 1) / 2 ≠ j, j < 0 ⊦

Rule argument

Additional information

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

Proof step 3 from proof div2-neg-odd (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  (j * 2 - 1) / 2 ≠ ~((~ j * 2 + 1) / 2), (j * 2 - 1) / 2 ≠ j, j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: div2-odd-01: ⊦ i < 0 → (1 - i * 2) / 2 = ~ i; ⊦ ~ i * j = ~(i * j); (s) ⊦ i + ~ j = i - j; (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 = i; (s) Used formulas: (j * 2 - 1) / 2 = ~((~ j * 2 + 1) / 2)

Proof step 4 from proof div2-neg-odd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ j ≠ 0 → ~ i / j = ~(i / j)

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) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ ~(i - j) = j - i; (s) Used terms: 2, ~ j * 2 + 1

Proof step 5 from proof div2-neg-odd (previous step) (back to tree)

Lemma Div-left