| 2 * 2 ^ i = 2 * 2 ^ i, 1 = 1, i1 * 2 + j1 < 0, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, (i1 * 2 + j1) + 1 < i, 0 ≤ i, (2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, abs(j0) < 2 ^ i, j1 ≤ 0, j1 < i, i1 ≤ 0, i1 < i, abs(j1) < 2, j0 ≤ 0, j0 < i ⊦ i1 = (j0 + 2 ^ i * i1 * 2 + 0 + 2 ^ i * j1) / (2 * 2 ^ i) |
2 ^ i * (j1 + 2 * (i1 + 1)) + j0 < i, 2 ^ i * (j1 + 2 * (i1 + 1)) + j0 ≤ 0, 0 ≤ i, (i1 * 2 + j1) + 1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, i1 * 2 + j1 < 0, j0 < i, j0 ≤ 0, abs(j1) < 2, i1 < i, i1 ≤ 0, j1 < i, j1 ≤ 0, abs(j0) < 2 ^ i, 0 < i ⊦ i1 = (2 ^ i * (j1 + i1 * 2) + j0) / (2 * 2 ^ i)
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%lsone: ⊦ i < 1 ↔ i ≤ 0; from specification int-abs%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%sub-add-01: ⊦ i + (j - i0) = i + j - i0; from specification int-abs%succ-rmerge: ⊦ i * j + i = i * (j + 1); from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%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%dist-rmerge: ⊦ i * j + i * j0 = i * (j + j0); from specification int-mult