| j0 - 2 ^ i < 0, 2 ^ i * 2 * i1 + j0 < 0, 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0, 2 * i1 < i, 0 ≤ i, 2 ^ i * 2 ≤ 0 - (j0 - 2 ^ i), j0 ≤ 2 ^ i, j0 < 2 ^ i + i, 0 < i, abs(j0) < 2 ^ i, i1 ≤ 0, i1 < i, j0 ≤ 0, j0 < i ⊦ i1 = (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2) |
2 ^ i + j0 < i, 2 ^ i + j0 ≤ 0, 0 ≤ i, 2 * i1 < i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0, 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, 2 ^ i * 2 * i1 + j0 < 0, j0 < 2 ^ i, j0 < i, j0 ≤ 0, i1 < i, i1 ≤ 0, abs(j0) < 2 ^ i, 0 < i, j0 < 2 ^ i + i, j0 ≤ 2 ^ i ⊦ i1 = (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2)
Used simplifier rules: zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; 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%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%numle-13: ⊦ (* i1) * j + i ≤ j ↔ (i1 - 1) * j + i ≤ 0; from specification int-mult%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%minus-sub: ⊦ ~(i - j) = j - i; from specification int-abs%neg-06: ⊦ 0 - i = ~ 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%add-zero: ⊦ i + 0 = i; from specification int-basic2%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs