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