---

Step * 1 of Lemma seq-max-lower-le


1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. seq-max-lower(k;n;f) ≤ n
⊢ primrec(n + 1;1;λi,r. if ((i + 1) * (f r)) - (2 * k) * (i + 1) ≤z (r * (f (i + 1))) - (2 * k) * r
                       then i + 1
                       else r
                       fi ) ≤ (n + 1)
BY
{ ((RWO "primrec-unroll" 0 THENA Auto)
   THEN (Subst' (n + 1 =z 0) ~ ff 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `seq-max-lower` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  seq-max-lower(k;n;f)  \mleq{}  n
\mvdash{}  primrec(n  +  1;1;\mlambda{}i,r.  if  ((i  +  1)  *  (f  r))  -  (2  *  k)  *  (i  +  1)  \mleq{}z  (r  *  (f  (i  +  1)))  -  (2  *  k)  *  r
                                              then  i  +  1
                                              else  r
                                              fi  )  \mleq{}  (n  +  1)


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (Subst'  (n  +  1  =\msubz{}  0)  \msim{}  ff  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `seq-max-lower`  0
  THEN  AutoSplit)

---

Home Index