---

Step * of Lemma find-ge-val_wf

∀[T:Type]
  ∀[test:T ⟶ 𝔹]. ∀[n:ℤ]. ∀[f:{n...} ⟶ T].
    find-ge-val(test;f;n) ∈ v:T × {n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt}  
    supposing ∃m:{n...}. ∀k:{m...}. test (f k) = tt 
  supposing value-type(T)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[test:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbZ{}].  \mforall{}[f:\{n...\}  {}\mrightarrow{}  T].
        find-ge-val(test;f;n)  \mmember{}  v:T  \mtimes{}  \{n':\mBbbZ{}|  (n  \mleq{}  n')  \mwedge{}  (v  =  (f  n'))  \mwedge{}  test  v  =  tt\}   
        supposing  \mexists{}m:\{n...\}.  \mforall{}k:\{m...\}.  test  (f  k)  =  tt 
    supposing  value-type(T)


By

---

Latex:
ProveWfLemma

---

Home Index