---

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


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  ∈ ℕ
BY
{ 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)
7. ¬↑isl(G x)
⊢ uniform-continuity-pi-search(
  G;
  x + m;x + 1) ∈ ℕ

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  0  <  m
3.  \mforall{}x:\mBbbN{}.  \mforall{}G:\mforall{}m:\mBbbN{}x  +  (m  -  1).  (Top  +  Top).    (uniform-continuity-pi-search(G;x  +  (m  -  1);x)  \mmember{}  \mBbbN{})
4.  x  :  \mBbbN{}
5.  \mneg{}((x  +  m)  \mleq{}  x)
6.  G  :  \mforall{}m:\mBbbN{}x  +  m.  (Top  +  Top)
\mvdash{}  if  isl(G  x)  then  x  else  uniform-continuity-pi-search(G;x  +  m;x  +  1)  fi    \mmember{}  \mBbbN{}


By

---

Latex:
AutoSplit

---

Home Index