| 0 = i1 * i0 + j0, i0 + 1 < i1, j0 < i1, 0 < i1, i0 ≤ i1, j0 ≤ i1, j0 ≤ 0, abs(j0) ≤ i1, i0 < 0, i0 < i1 ⊦ 0 = i1, ~1 = i1 |
Used simplifier rules: lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%negle-13: ⊦ ~ i ≤ j ↔ 0 ≤ i + j; from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%ls-02: ⊦ i < i + j ↔ 0 < j; from specification int-basic2%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%zero-gels: ⊦ i < 0 ∧ 0 ≤ j → ¬ j < i; from specification int-abs%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%zero-eq: ⊦ i * j = 0 ↔ i = 0 ∨ j = 0; from specification int-mult%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs Used formulas: j0 = 0