---

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


1. P : ℕ ⟶ ℙ
2. m : ℕ
⊢ ∀x:ℕ
    ((∃n:{x..(x + m) + 1-}. P[n])
    ⇒ (∀G:∀m:ℕx + m. Dec(P[m])
          (uniform-continuity-pi-search(
           G;
           x + m;x) ∈ {k:{x..(x + m) + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..(x + m) + 1-}. (P[m] ⇒ (k ≤ m)))} ))\000C)
BY
{ (NatInd (-1) THEN (UnivCD THENA Auto) THEN RecUnfold `uniform-continuity-pi-search` 0 THEN AutoSplit) }

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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index