Step
*
1
1
1
of Lemma
uniform-continuity-pi-search-prop1
1. P : ℕ ⟶ ℙ
2. x : ℕ
3. m : ℕ
⊢ (∃n:{x..(x + m) + 1-}. P[n])
⇒ (∀G:∀m:ℕx + m. Dec(P[m])
(uniform-continuity-pi-search(
G;
x + m;x) ∈ {k:{x..(x + m) + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m]))} ))
BY
{ MoveToConcl (-2) }
1
1. P : ℕ ⟶ ℙ
2. m : ℕ
⊢ ∀x:ℕ
((∃n:{x..(x + m) + 1-}. P[n])
⇒ (∀G:∀m:ℕx + m. Dec(P[m])
(uniform-continuity-pi-search(
G;
x + m;x) ∈ {k:{x..(x + m) + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m]))} )))
Latex:
Latex:
1. P : \mBbbN{} {}\mrightarrow{} \mBbbP{}
2. x : \mBbbN{}
3. m : \mBbbN{}
\mvdash{} (\mexists{}n:\{x..(x + m) + 1\msupminus{}\}. P[n])
{}\mRightarrow{} (\mforall{}G:\mforall{}m:\mBbbN{}x + m. Dec(P[m])
(uniform-continuity-pi-search(
G;
x + m;x) \mmember{} \{k:\{x..(x + m) + 1\msupminus{}\}| P[k] \mwedge{} (\mforall{}m:\{x..k\msupminus{}\}. (\mneg{}P[m]))\} ))
By
Latex:
MoveToConcl (-2)
Home
Index