---

Step * of Lemma seq-max-lower-property

∀[k,n:ℕ]. ∀[f:ℕ+ ⟶ ℤ].
  ∀i:ℕ+n + 1. (((seq-max-lower(k;n;f) * (f i)) - i * (f seq-max-lower(k;n;f))) ≤ ((2 * k) * (seq-max-lower(k;n;f) - i)))
BY
{ (Auto
   THEN (NatInd 2 THEN Auto)
   THEN Unfold `seq-max-lower` 0
   THEN Reduce 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (Subst' n <z 1 ~ ff 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `seq-max-lower` 0
   THEN (Subst' (n - 1) + 1 ~ n 0 THENA Auto)
   THEN (Subst' (n - 1) + 1 ~ n -2 THENA Auto)) }

1
1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. ∀i:ℕ+n
     (((seq-max-lower(k;n - 1;f) * (f i)) - i * (f seq-max-lower(k;n - 1;f))) ≤ ((2 * k)
      * (seq-max-lower(k;n - 1;f) - i)))
6. i : ℕ+n + 1
⊢ ((if (n * (f seq-max-lower(k;n - 1;f))) - (2 * k) * n ≤z (seq-max-lower(k;n - 1;f) * (f n)) - (2 * k)
       * seq-max-lower(k;n - 1;f)
  then n
  else seq-max-lower(k;n - 1;f)
  fi 
  * (f i)) - i
  * (f 
     if (n * (f seq-max-lower(k;n - 1;f))) - (2 * k) * n ≤z (seq-max-lower(k;n - 1;f) * (f n)) - (2 * k)
        * seq-max-lower(k;n - 1;f)
     then n
     else seq-max-lower(k;n - 1;f)
     fi )) ≤ ((2 * k)
  * (if (n * (f seq-max-lower(k;n - 1;f))) - (2 * k) * n ≤z (seq-max-lower(k;n - 1;f) * (f n)) - (2 * k)
        * seq-max-lower(k;n - 1;f)
    then n
    else seq-max-lower(k;n - 1;f)
    fi  - i))

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].
    \mforall{}i:\mBbbN{}\msupplus{}n  +  1
        (((seq-max-lower(k;n;f)  *  (f  i))  -  i  *  (f  seq-max-lower(k;n;f)))  \mleq{}  ((2  *  k)
          *  (seq-max-lower(k;n;f)  -  i)))


By

---

Latex:
(Auto
  THEN  (NatInd  2  THEN  Auto)
  THEN  Unfold  `seq-max-lower`  0
  THEN  Reduce  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (Subst'  n  <z  1  \msim{}  ff  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `seq-max-lower`  0
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  0  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -2  THENA  Auto))

---

Home Index