---

Step * 1 of Lemma uniform-continuity-pi-search-prop2


1. n : ℕ
2. P : ℕ ⟶ ℙ
3. G : ∀m:ℕn. Dec(P[m])
4. x : ℕ
5. ∃n:{x..n + 1-}. P[n]
6. x ≤ n
⊢ uniform-continuity-pi-search(
  G;
  n;x) ∈ {k:{x..n + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..n + 1-}. (P[m] ⇒ (k ≤ m)))} 
BY
{ ((Assert ⌜∃m:ℕ. (n = (x + m) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜n - x⌝]⋅ THEN Auto)) THEN D (-1)) }

1
1. n : ℕ
2. P : ℕ ⟶ ℙ
3. G : ∀m:ℕn. Dec(P[m])
4. x : ℕ
5. ∃n:{x..n + 1-}. P[n]
6. x ≤ n
7. m : ℕ
8. n = (x + m) ∈ ℤ
⊢ uniform-continuity-pi-search(
  G;
  n;x) ∈ {k:{x..n + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..n + 1-}. (P[m] ⇒ (k ≤ m)))} 

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  G  :  \mforall{}m:\mBbbN{}n.  Dec(P[m])
4.  x  :  \mBbbN{}
5.  \mexists{}n:\{x..n  +  1\msupminus{}\}.  P[n]
6.  x  \mleq{}  n
\mvdash{}  uniform-continuity-pi-search(
    G;
    n;x)  \mmember{}  \{k:\{x..n  +  1\msupminus{}\}|  P[k]  \mwedge{}  (\mforall{}m:\{x..k\msupminus{}\}.  (\mneg{}P[m]))  \mwedge{}  (\mforall{}m:\{x..n  +  1\msupminus{}\}.  (P[m]  {}\mRightarrow{}  (k  \mleq{}  m)))\} 


By

---

Latex:
((Assert  \mkleeneopen{}\mexists{}m:\mBbbN{}.  (n  =  (x  +  m))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}n  -  x\mkleeneclose{}]\mcdot{}  THEN  Auto))  THEN  D  (-1))

---

Home Index