---

Step * 1 1 of Lemma uniform-continuity-pi-search_wf


1. n : ℕ
2. G : ∀m:ℕn. (Top + Top)
3. x : ℕ
4. x < n
5. m : ℕ
6. n = (x + m) ∈ ℤ
⊢ uniform-continuity-pi-search(
  G;
  n;x) ∈ ℕ
BY
{ (MoveToConcl (-5) THEN (HypSubst' (-1) 0 THENA Auto) THEN ThinVar `n' THEN MoveToConcl (-2)) }

1
1. m : ℕ
⊢ ∀x:ℕ. ∀G:∀m:ℕx + m. (Top + Top).  (uniform-continuity-pi-search(G;x + m;x) ∈ ℕ)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  G  :  \mforall{}m:\mBbbN{}n.  (Top  +  Top)
3.  x  :  \mBbbN{}
4.  x  <  n
5.  m  :  \mBbbN{}
6.  n  =  (x  +  m)
\mvdash{}  uniform-continuity-pi-search(
    G;
    n;x)  \mmember{}  \mBbbN{}


By

---

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

---

Home Index