---

Step * 1 1 of Lemma uniform-continuity-pi-search-prop2


1. n : ℕ
2. P : ℕ ⟶ ℙ
3. G : ∀m:ℕn. Dec(P[m])
4. x : ℕ
5. ∃n:{x..n + 1-}. P[n]
6. x ≤ n
7. m : ℕ
8. n = (x + m) ∈ ℤ
⊢ uniform-continuity-pi-search(
  G;
  n;x) ∈ {k:{x..n + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..n + 1-}. (P[m] ⇒ (k ≤ m)))} 
BY
{ (MoveToConcl (-6) THEN MoveToConcl (-4) THEN (HypSubst' (-1) 0 THENA Auto) THEN ThinVar `n') }

1
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])) ∧ (∀m:{x..(x + m) + 1-}. (P[m] ⇒ (k ≤ m)))} ))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  G  :  \mforall{}m:\mBbbN{}n.  Dec(P[m])
4.  x  :  \mBbbN{}
5.  \mexists{}n:\{x..n  +  1\msupminus{}\}.  P[n]
6.  x  \mleq{}  n
7.  m  :  \mBbbN{}
8.  n  =  (x  +  m)
\mvdash{}  uniform-continuity-pi-search(
    G;
    n;x)  \mmember{}  \{k:\{x..n  +  1\msupminus{}\}|  P[k]  \mwedge{}  (\mforall{}m:\{x..k\msupminus{}\}.  (\mneg{}P[m]))  \mwedge{}  (\mforall{}m:\{x..n  +  1\msupminus{}\}.  (P[m]  {}\mRightarrow{}  (k  \mleq{}  m)))\} 


By

---

Latex:
(MoveToConcl  (-6)  THEN  MoveToConcl  (-4)  THEN  (HypSubst'  (-1)  0  THENA  Auto)  THEN  ThinVar  `n')

---

Home Index