| i * j = i * j0 + j1, abs(j1) < i, 0 ≤ i ⊦ j * i + 0 = j0 * i + j1 ∧ 0 ≤ 0 ∧ 0 < i ∧ 0 ≤ j1 ∧ j1 < i, j1 = 0 |
i * j = i * j0 + j1, j1 < 0, 0 ≤ i, 0 < i + j1, j1 + 1 < i, 1 < i, 0 < i ⊦
Used simplifier rules: commutativity: ⊦ i * j = j * i;%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%add-less: ⊦ 0 < i → i1 < i1 + i; from specification int-basic2%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%lst-01: ⊦ ¬ i < j → (i ≠ j ↔ j < i); from specification int-basic1%irref: ⊦ ¬ i < i; from specification int-basic1%abs-16: ⊦ 0 < j → abs(j) = j; 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%absls: ⊦ ¬ abs(i) < 0; from specification int-abs%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); 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%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2