---

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


1. m : ℕ
⊢ ∀x:ℕ. ∀G:∀m:ℕx + m. (Top + Top).  (uniform-continuity-pi-search(G;x + m;x) ∈ ℕ)
BY
{ (NatInd (-1) THEN (UnivCD THENA Auto) THEN RecUnfold `uniform-continuity-pi-search` 0 THEN AutoSplit) }

1
1. m : ℤ
2. 0 < m
3. ∀x:ℕ. ∀G:∀m:ℕx + (m - 1). (Top + Top).  (uniform-continuity-pi-search(G;x + (m - 1);x) ∈ ℕ)
4. x : ℕ
5. ¬((x + m) ≤ x)
6. G : ∀m:ℕx + m. (Top + Top)
⊢ if isl(G x) then x else uniform-continuity-pi-search(G;x + m;x + 1) fi  ∈ ℕ

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
\mvdash{}  \mforall{}x:\mBbbN{}.  \mforall{}G:\mforall{}m:\mBbbN{}x  +  m.  (Top  +  Top).    (uniform-continuity-pi-search(G;x  +  m;x)  \mmember{}  \mBbbN{})


By

---

Latex:
(NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `uniform-continuity-pi-search`  0
  THEN  AutoSplit)

---

Home Index