| i0 * 2 = (i + j) + 1, i0 < i, i ≤ j, i + j < 0, i0 ≤ 0, i0 < j ⊦ |
Used simplifier rules: nummult-ls: ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 < (* j) ↔ i0 < (i + j - 1) / i);%sub-eq: ⊦ i - j = i0 ↔ i = i0 + 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-def: ⊦ i + (j - i) = j; from specification int-abs%eq-pos: ⊦ 0 < i → (i * j = i * j0 ↔ j = j0); from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; from specification int-abs%numls-08: ⊦ i + j < (* i1) * i ↔ j < (i1 - 1) * i; from specification int-mult%one: ⊦ 1 * i = i; from specification int-mult%sub-le: ⊦ i - j ≤ i0 ↔ i ≤ j + i0; from specification int-abs%add-mult-two: ⊦ i + i = 2 * i; from specification int-mult%le-two: ⊦ 2 * i ≤ 2 * j + 1 ↔ i ≤ j; from specification int-mult%sub-add-01: ⊦ i + (j - i0) = i + j - i0; from specification int-abs%sub-add-05: ⊦ i + j - i + 1 = j - 1; from specification int-abs%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%lsone: ⊦ i < 1 ↔ i ≤ 0; from specification int-abs%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%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%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%succ-01: ⊦ i +1 = i + 1; from specification int-basic2%ls: ⊦ i + j < j ↔ i < 0; from specification int-basic2 Used formulas: i = i0 * 2 - j + 1