Proof step 47 from proof max_exp-fac-gen (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  max_exp(i, fac(i1)) = Σ countFun(1, i0 - 1, λ j1. i1 / i ^ j1), (i1 * i + j2) / i = i1, i0 < n→i(n) + 2, 0 < i0, 1 < i ^ i0, j2 < i, n + 1 < i→n(i0), 2 ≤ i0, 0 < i1, 0 < i1 * i + j2, 0 < i, 0 ≤ j2, prime(i), i1 * i + j2 < i ^ i0, 0 < i ^ i0, ∀ j0, i2, i0. i→n(j0) < i→n(i1 * i + j2) → prime(i2) ∧ j0 < i2 ^ i0 ∧ 0 < j0 ∧ 0 < i2 ^ i0 ∧ 0 ≤ i0 ∧ 1 < i2 ^ i0 → max_exp(i2, fac(j0)) = Σ countFun(1, i0, λ j1. j0 / i2 ^ j1) ⊦ i0 = 0, max_exp(i, fac(i1)) = Σ countFun(2, i0, λ j0. (i1 * i + j2) / i ^ j0), countFun(1, i0 - 1, λ j1. i1 / i ^ j1)[n] = countFun(2, i0, λ j0. (i1 * i + j2) / i ^ j0)[n], n = 0

Rule argument

Additional information

Used simplifier rules: zero: ⊦ 0 < m ↔ m ≠ 0; from specification nat-basic1%num-n2i-ls-02: 0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n; from specification intnat%num-n2i-ls-03: i < 0 ⊦ (* i) < n→i(n); from specification intnat%nat2int: ⊦ 0 ≤ n→i(n); from specification intnat%mone-06: ⊦ ~1 < i ↔ 0 ≤ i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; 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]%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%numlsledel-01: i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j; from specification int-abs%sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; from specification int-abs%leone: ⊦ 1 ≤ i ↔ 0 < i; from specification int-abs%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%sub-sub: ⊦ i - j - i0 = i - j + i0; from specification int-abs