---

Step * of Lemma seq-min-upper-le

∀[k:ℕ]. ∀[n:ℕ+]. ∀[f:ℕ+ ⟶ ℤ].  (seq-min-upper(k;n;f) ≤ n)
BY
{ (Auto THEN (NatPlusInd 2⋅ THENA Auto) THEN Unfold `seq-min-upper` 0 THEN Reduce 0 THEN Auto) }

1
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)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (NatPlusInd  2\mcdot{}  THENA  Auto)  THEN  Unfold  `seq-min-upper`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index