---

Step * 1 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)
7. ¬↑isl(G x)
⊢ uniform-continuity-pi-search(
  G;
  x + m;x + 1) ∈ ℕ
BY
{ (InstHyp [⌜x + 1⌝;⌜G⌝] (-5)⋅ THENA Auto) }

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)
8. uniform-continuity-pi-search(
   G;
   (x + 1) + (m - 1);x + 1) ∈ ℕ
⊢ 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)
7.  \mneg{}\muparrow{}isl(G  x)
\mvdash{}  uniform-continuity-pi-search(
    G;
    x  +  m;x  +  1)  \mmember{}  \mBbbN{}


By

---

Latex:
(InstHyp  [\mkleeneopen{}x  +  1\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)

---

Home Index