| i→n(j) = m + 1, 0 ≤ i, i ≤ j, 0 < j, m < (m - i→n(i)) + i→n(i), ∀ i1. i ≤ i1 ∧ i1 ≤ j → intfun(i1) = i0, ∀ j0, i1, intfun, i0. i→n(j0) - i→n(i1) < m + 1 - i→n(i) → (∀ i2. i1 ≤ i2 ∧ i2 ≤ j0 → intfun(i2) = i0) ∧ i1 ≤ j0 ∧ 0 ≤ i1 → Σ countFun(i1, j0, intfun) = (1 + j0 - i1) * i0 ⊦ j = 0, j = 1, Σ countFun(i, j - 1, intfun) + intfun(j) = (1 + j - i) * i0 |
Used simplifier rules: countFun-base-02: ⊦ countFun(j, j - 1, intfun) = [];%sum-empty: ⊦ Σ [] = 0;%lep: ⊦ m ≤ m + n; from specification nat%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2%l: ⊦ m + n < m + n0 ↔ n < n0; from specification nat-basic2%labs: ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j); from specification intnat%absle: ⊦ 0 ≤ i → abs(i) = i; from specification int-abs%irreflexivity: ⊦ ¬ i < i; from specification oelem[intlista]%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; from specification intnat%labs-01: ⊦ i→n(i) ≤ i→n(j) ↔ abs(i) ≤ abs(j); from specification intnat%abs-16: ⊦ 0 < j → abs(j) = j; from specification int-abs%anti: ⊦ i ≤ j → (j ≤ i ↔ i = j); from specification int-abs%lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%ax-04: ⊦ i + 0 = i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%sub-add: ⊦ i + j - i = j; from specification int-abs%one: ⊦ 1 * i = i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%ler: ⊦ i ≤ i; from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m, i→n(i), n