| ¬((i0 * 2 ^ (i - 1)) % 2 = 0 ∧ (j0 - 1) / 2 < 0 ∧ i0 * 2 ^ (i - 1) < 0 ∧ 0 < 2), 0 < i, (i0 * 2 ^ i) % 2 = 0 ∧ j0 - 1 < 0 ∧ i0 * 2 ^ i < 0 ∧ 0 < 2, 0 ≤ i, i0 < i, i0 ≤ 0, j0 < i, j0 ≤ 0, i0 * 2 ^ i + j0 < 0, abs(j0) < 2 ^ i, 1 < i, 0 < i ⊦ ((j0 - 1) / 2) % 2 = ((j0 - 1) / 2 + i0 * 2 ^ (i - 1)) % 2 |
j0 < i, j0 ≤ 0, i0 * 2 ^ i + j0 < 0, abs(j0) < 2 ^ i, 1 < i, 0 < i, 0 ≤ i, i0 < 0 ⊦ ((j0 - 1) / 2) % 2 = ((j0 - 1) / 2 + i0 * 2 ^ (i - 1)) % 2, i0 = 0, (i0 * 2 ^ (i - 1)) % 2 = 0 ∧ j0 < 0
Used simplifier rules: mod-2pot: ⊦ 0 < i → (j * 2 ^ i) % 2 = 0;%pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i;%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%leone: ⊦ 1 ≤ i ↔ 0 < i; from specification int-abs%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%zero-ls-01: ⊦ i < 0 → (i * j < 0 ↔ 0 < j); from specification int-mult%mone-05: ⊦ i ≤ ~1 ↔ i < 0; from specification int-abs%numle-03: ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; from specification int-abs%numsub: ⊦ (* i) + i0 - (* j) = (i - j) + i0; from specification int-abs%sub-add-01: ⊦ i + (j - i0) = i + j - i0; from specification int-abs%div-ls-zero: 0 < j ⊦ i / (* j) < 0 ↔ i + j ≤ 0; from specification int-div%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%zero-ls-03: ⊦ i ≤ 0 → (i * j < 0 ↔ ¬ ¬(0 < j ∧ i ≠ 0)); from specification int-mult%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%lsone: ⊦ i < 1 ↔ i ≤ 0; 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%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult