---

Step * of Lemma seq-min-upper-property

∀[k,n:ℕ]. ∀[f:ℕ+ ⟶ ℤ].
  ∀i:ℕ+n + 1. (((i * (f seq-min-upper(k;n;f))) - seq-min-upper(k;n;f) * (f i)) ≤ ((2 * k) * (seq-min-upper(k;n;f) - i)))
BY
{ (Auto
   THEN (NatInd 2 THEN Auto)
   THEN Unfold `seq-min-upper` 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-min-upper` 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
     (((i * (f seq-min-upper(k;n - 1;f))) - seq-min-upper(k;n - 1;f) * (f i)) ≤ ((2 * k)
      * (seq-min-upper(k;n - 1;f) - i)))
6. i : ℕ+n + 1
⊢ ((i
  * (f 
     if (n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n) ≤z (seq-min-upper(k;n - 1;f) * (f n))
        + ((2 * k) * seq-min-upper(k;n - 1;f))
     then seq-min-upper(k;n - 1;f)
     else n
     fi )) - if (n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n) ≤z (seq-min-upper(k;n - 1;f) * (f n))
                + ((2 * k) * seq-min-upper(k;n - 1;f))
  then seq-min-upper(k;n - 1;f)
  else n
  fi 
  * (f i)) ≤ ((2 * k)
  * (if (n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n) ≤z (seq-min-upper(k;n - 1;f) * (f n))
        + ((2 * k) * seq-min-upper(k;n - 1;f))
    then seq-min-upper(k;n - 1;f)
    else n
    fi  - i))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (NatInd  2  THEN  Auto)
  THEN  Unfold  `seq-min-upper`  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-min-upper`  0
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  0  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -2  THENA  Auto))

---

Home Index