| i0 - 1 = i1 * 2 + j1 ∧ j1 ≤ 0 ∧ abs(j1) < 2 ∧ i1 ≤ 0 ∧ 0 < 2 ∧ i0 - 1 < 0, j + 1 = 2 ^ i * (i0 + 1) + j0, 2 ^ i * i0 + j0 < 0, j0 ≤ 0, j0 < i, i0 ≤ 0, i0 < i, 0 ≤ i, j < 0, 0 < i, abs(j0) < 2 ^ i ⊦ i1 = (j + 1 - 2 ^ i * 2) / (2 ^ i * 2) |
j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, i1 * 2 + j1 < 0, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, (i1 * 2 + j1) + 1 < i, 0 ≤ i, j < 0, 0 < i, abs(j0) < 2 ^ i, j1 ≤ 0, j1 < i, i1 ≤ 0, i1 < i, abs(j1) < 2, j0 ≤ 0, j0 < i ⊦ i1 = (j + 1 - 2 ^ i * 2) / (2 ^ i * 2)
Used simplifier rules: zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%mone-05: ⊦ i ≤ ~1 ↔ i < 0; from specification int-abs%numle-03: ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; from specification int-abs%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%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%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%sub-eq: ⊦ i - j = i0 ↔ i = i0 + j; from specification int-abs