| i0 * j + j0 = (i2 * j + j1) + 1, j1 < j, j1 < 0, i2 * j + j1 < j, i2 * j + j1 < 0, i0 < j + j1, j0 < j + j1, i2 < j + j1, i2 < j, i2 ≤ 0, i2 * j + j1 < ~1, 2 + i2 * j + j1 < j, i0 < j, i0 ≤ 0, j0 < j, j0 ≤ 0, abs(j0) < j, 0 < j + j1, j1 + 1 < j, 1 < j, 0 < j ⊦ j0 = j1 + 1, j1 = 0 |
i * j + j0 = i0 * j + j1, 0 ≤ j0, j0 < j, 0 ≤ j1, j1 < j ⊦ i = i0 ∧ j0 = j1
Used simplifier rules: neg-12: ⊦ ~ i = ~ j ↔ i = j; from specification int-abs%neg-15: ⊦ i + ~ j = i - j; 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%sub-eq: ⊦ i - j = i0 ↔ i = i0 + j; from specification int-abs%sub-add-01: ⊦ i + (j - i0) = i + j - i0; from specification int-abs%negle-07: ⊦ i ≤ ~ j ↔ i + j ≤ 0; from specification int-abs%numle-03: ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; from specification int-abs%mone-05: ⊦ i ≤ ~1 ↔ i < 0; from specification int-abs%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%zero-02: ⊦ 0 < i ∧ 0 < j → 0 < i + j; from specification int-basic2%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%ls: ⊦ i + j < j ↔ i < 0; from specification int-basic2%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%lenls: ⊦ i ≤ j → ¬ j < i; from specification int-abs Used terms: i0, j, ~(j1 + 1), i2, ~ j0