| j1 < 0, i * j + j0 = i0 * j + j1, j < j0, j < j1, j0 ≤ 0, j1 ≤ 0, j < 0 ⊦ i = i0 ∧ j0 = j1, (0 - j1) + j < 0 ∧ abs(j0) + j < 0 |
i * j + j0 = i0 * j + j1, j1 < 0, j < 0, j0 ≤ 0, j < j1, j < j0, 0 ≤ abs(j0) + j, j < ~1 ⊦ j0 = j1
Used simplifier rules: eq-neg: ⊦ i < 0 → (i * j = i * j0 ↔ j = j0);%associativity: ⊦ i * j * j0 = (i * j) * j0;%commutativity: ⊦ i * j = j * i;%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%add-in: ⊦ i + j = i + i0 ↔ j = i0; from specification int-basic2%numls-03: ⊦ i + (* j) < (* j0) ↔ i < j0 - j; from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%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%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; 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%neg-15: ⊦ i + ~ j = i - j; from specification int-abs%neg-06: ⊦ 0 - i = ~ i; from specification int-abs%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs