| 0 < ~ j → (∃ i. 0 ≤ i ∧ 2 ^ i ≤ ~ j ∧ ~ j < 2 ^ (i + 1)), j < 0 ⊦ ∃ i. ~1 ≤ i ∧ j + 2 ^ i < 0 ∧ 0 ≤ 2 ^ (i + 1) + j |
0 < 2 ^ i * 2 + j, 2 ^ i + j ≤ 0, 0 ≤ i, j < 0 ⊦ ∃ i. ~1 ≤ i ∧ j + 2 ^ i < 0 ∧ 0 ≤ 2 ^ (i + 1) + j
Used simplifier rules: succ: ⊦ 0 ≤ i → j ^ (i + 1) = j ^ i * j;%pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i;%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%nummult-ls-02: ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0); from specification int-div%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%ls-02: ⊦ i < i + j ↔ 0 < j; from specification int-basic2%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%one: ⊦ 1 * i = i; from specification int-mult%numls-04: ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0; from specification int-mult%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; 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%negle-07: ⊦ i ≤ ~ j ↔ i + j ≤ 0; from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%neg: ⊦ 0 < ~ i ↔ i < 0; from specification int-abs