| j + 1 - 2 ^ i = i0 * 2 ^ i + j0 ∧ j0 ≤ 0 ∧ abs(j0) < 2 ^ i ∧ i0 ≤ 0 ∧ 0 < 2 ^ i ∧ j + 1 - 2 ^ i < 0, j < 0, 0 < i ⊦ (i0 - 1) / 2 = (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1) |
j + 1 = 2 ^ i * (i0 + 1) + j0, 0 ≤ i, i0 < i, i0 ≤ 0, j0 < i, j0 ≤ 0, j + 1 < 2 ^ i, abs(j0) < 2 ^ i, 0 < i, j < 0 ⊦ (i0 - 1) / 2 = (j + 1 - 2 ^ i * 2) / (2 ^ i * 2)
Used simplifier rules: pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i;%succ: ⊦ 0 ≤ i → j ^ (i + 1) = j ^ i * j;%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (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-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%add-zero: ⊦ i + 0 = i; from specification int-basic2%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; 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%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%succ-rmerge: ⊦ i * j + i = i * (j + 1); from specification int-mult%sub-eq: ⊦ i - j = i0 ↔ i = i0 + j; from specification int-abs