---

Step * 1 of Lemma seq-min-upper-le


1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. seq-min-upper(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 r
                       else i + 1
                       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-min-upper` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  seq-min-upper(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  r
                                              else  i  +  1
                                              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-min-upper`  0
  THEN  AutoSplit)

---

Home Index