| j0 ≤ 0, i2 * 2 + j0 < 0, ~1 ≤ 2 * (i1 + i2) + j0, 0 ≤ i1, abs(j0) < 2 ⊦ (2 * (i1 + i2) + 1 + j0) / 2 = i2 + i1 |
Used simplifier rules: nummult-le-03: ⊦ 0 < i ∧ j < 0 → ((* j) ≤ (* i) * i0 ↔ j / i ≤ i0);%div-two: ⊦ 0 ≤ i → (2 * i + 1) / 2 = i;%div-mult-num: j ≠ 0, j0 % j = 0 ⊦ (i * (* j0)) / (* j) = i * j0 / j;%lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs%minus-one: ⊦ i < 0 → (~2 < i ↔ i = ~1); from specification int-basic1%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%add-zero: ⊦ i + 0 = i; from specification int-basic2%one: ⊦ 1 * i = i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%add-in: ⊦ i + j = i + i0 ↔ j = i0; from specification int-basic2%zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); from specification int-mult Used formulas: j0 = 0