| j % 2 = 0, i % 2 = 0, j < i, j < 0, j ≤ ~2, i / 2 < j / 2, j ≤ i, 0 < i, j + 1 < i ⊦ |
⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0)
Used simplifier rules: nummult-le-01: ⊦ 0 < i ∧ j < 0 → ((* i) * i0 ≤ (* j) ↔ i0 ≤ (j + 1 - i) / i);%div-ls-mone: 0 < j ⊦ i / (* j) < ~1 ↔ i + 2 * j ≤ 0;%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%mone-05: ⊦ i ≤ ~1 ↔ i < 0; from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%ls-two-03: ⊦ i < 0 ∧ 0 < j → 2 * i ≤ j; from specification int-mult%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%ls-two-02: ⊦ i < 0 ∧ 0 < j → 2 * i < j; from specification int-mult%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%numls-03: ⊦ i + (* j) < (* j0) ↔ i < j0 - j; from specification int-abs%numle-03: ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; from specification int-abs%zero-gels-02: ⊦ i < 0 ∧ 0 < j → ¬ j ≤ i; from specification int-abs Used terms: j, 2, i0, j0