---

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