| j * (i0 + 1) + j0 ≤ 0, i0 * j + j0 < 0, j < 0, 0 ≤ i0, j0 ≤ 0, j < j0 ⊦ 0 < i0 ↔ ~1 = j ∨ ¬ 0 < j * (i0 - 1) + j0, j = 0 |
Used simplifier rules: numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs%mone-06: ⊦ ~1 < i ↔ 0 ≤ i; 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-gr-add-01: ⊦ 0 ≤ i ∧ j < 0 ∧ j0 ≤ 0 → ¬ 0 < i * j + j0; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%numle-02: ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%mone-08: ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%Mult-zero: ⊦ i * 0 = 0; from specification int-mult%add-zero: ⊦ i + 0 = i; from specification int-basic2%one: ⊦ 1 * i = i; from specification int-mult%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%minus-one-01: ⊦ i * ~1 = ~ i; from specification int-mult%neg-15: ⊦ i + ~ j = i - j; from specification int-abs%minus-add: i < 0 ⊦ (* i) + j = j - ~ i; from specification int-abs%sub-le: ⊦ i - j ≤ i0 ↔ i ≤ j + i0; from specification int-abs%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs% ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i0, 1, i