| 2 ≤ i ^ ~ j0, j0 < i0, j0 < 0, ~1 ≤ i0, 0 ≤ i0, ~2 < i0, 1 < i, 2 ≤ i, j0 ≤ i0, 1 < i ^ ~ j0, ∀ j1, i, j0. i→n(j1) < i→n(i0 +1) → 2 ≤ i ∧ 0 ≤ j1 ∧ 1 < i → (i ^ j1 ≤ i ^ j0 ↔ j1 ≤ j0) ⊦ i ^ i0 * i ≤ 0 ↔ i0 + 1 ≤ j0, j0 = 0 |
Used simplifier rules: notneg-01: ⊦ 0 < i ∧ 0 ≤ j → ¬ i ^ j ≤ 0;%succ-01: ⊦ i + 1 ≤ j ↔ i < j; from specification int-abs%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%numleledel-01: i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; from specification int-abs%numlsledel-01: i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; from specification int-abs%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%zero-le: ⊦ 0 < i → (i * j ≤ 0 ↔ j ≤ 0); from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult