| abs(j1) < 4, abs(j0) < 2, i1 * 4 + j1 < 0, i1 * 4 + j1 ≤ ~3, j0 ≤ 0, 8 * i1 + j0 + j1 * 2 < 0, 8 * i1 + j0 + j1 * 2 < ~7, j1 ≤ 0, 0 ≤ j0 + j1 * 2, i1 < 0, i1 * 4 < j1 + j0 ⊦ i1 = (8 * i1 + j0 + j1 * 2) / 8, i1 = 0, j0 < 0 ∧ j1 < 0 |
Used simplifier rules: nummult-le-01: ⊦ 0 < i ∧ j < 0 → ((* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i);%div-mult-num-01: j % j0 = 0, j ≠ 0, j0 ≠ 0 ⊦ (i * (* j0)) / (* j) = i / j / j0;%one: ⊦ i / 1 = i;%lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%Abs-pos: ⊦ ¬ j < 0 → abs(j) = j; from specification int-abs%numlsledel: j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%ls-same-03: ⊦ i < 0 → (i < i * j ↔ j < 1); from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); from specification int-mult%mone-05: ⊦ i ≤ ~1 ↔ i < 0; from specification int-abs%numlsf: ⊦ i < (* j) ∧ j < 0 → i < 0; (forward) from specification int-basic1 Used formulas: j1 = 0