| i < j, max(count-i2j(i + 1, j)) ≤ i, max(count-i2j(i + 1, j)) < j, ∀ j0, i0. i→n(j0 - i0) < i→n(j - i) → i0 ≤ j0 → max(count-i2j(i0, j0)) = j0 ⊦ i = j |
Used simplifier rules: forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%transitivity: ⊦ i < i0 ∧ i0 < i1 → i < i1; (forward) from specification oelem[intlista]%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%succ-01: ⊦ i + 1 ≤ j ↔ 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-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%labs: ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); from specification intnat%abssub-02: ⊦ j < i → abs(i - j) = i - j; from specification int-abs%abssub-01: ⊦ j < i → abs(i - j + 1) = i - j + 1; from specification int-abs%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%Sub-def: ⊦ i + (j - i) = j; from specification int-abs%succ-02: ⊦ i < j + 1 ↔ i ≤ j; from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%irreflexivity: ⊦ ¬ i < i; from specification oelem[intlista] Used terms: j, i + 1