---

Step * of Lemma uniform-continuity-pi-search_wf

∀[n:ℕ]. ∀[G:∀m:ℕn. (Top + Top)]. ∀[x:ℕ].  (uniform-continuity-pi-search(G;n;x) ∈ ℕ)
BY
{ ((UnivCD THENA Auto) THEN (Decide ⌜x < n⌝⋅ THENA Auto)) }

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

2
1. n : ℕ
2. G : ∀m:ℕn. (Top + Top)
3. x : ℕ
4. ¬x < n
⊢ uniform-continuity-pi-search(
  G;
  n;x) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[G:\mforall{}m:\mBbbN{}n.  (Top  +  Top)].  \mforall{}[x:\mBbbN{}].    (uniform-continuity-pi-search(G;n;x)  \mmember{}  \mBbbN{})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Decide  \mkleeneopen{}x  <  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index