---

Step * of Lemma quick-find_wf

∀[n:ℕ+]. ∀[p:{n...} ⟶ 𝔹].  quick-find(p;n) ∈ {m:{n...}| ↑(p m)}  supposing ∃N:{n...}. ∀m:{N...}. (↑(p m))
BY
{ ((UnivCD THENA Auto) THEN ExRepD) }

1
1. n : ℕ+
2. p : {n...} ⟶ 𝔹
3. N : {n...}
4. ∀m:{N...}. (↑(p m))
⊢ quick-find(p;n) ∈ {m:{n...}| ↑(p m)} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[p:\{n...\}  {}\mrightarrow{}  \mBbbB{}].    quick-find(p;n)  \mmember{}  \{m:\{n...\}|  \muparrow{}(p  m)\}    supposing  \mexists{}N:\{n...\}.  \mforall{}m:\{N...\}.  (\muparrow{}\000C(p  m))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  ExRepD)

---

Home Index