---

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


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])
9. y : ¬P[x]
10. (G x) = (inr y ) ∈ Dec(P[x])
⊢ uniform-continuity-pi-search(
  G;
  x + m;x + 1) ∈ {k:{x..(x + m) + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..(x + m) + 1-}. (P[m] ⇒ (k ≤ m)))} 
BY
{ (InstHyp [⌜x + 1⌝;⌜G⌝] (-7)⋅ THENA Auto) }

1
.....antecedent..... 
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])
9. y : ¬P[x]
10. (G x) = (inr y ) ∈ Dec(P[x])
⊢ ∃n:{x + 1..((x + 1) + (m - 1)) + 1-}. P[n]

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])
9. y : ¬P[x]
10. (G x) = (inr y ) ∈ Dec(P[x])
11. uniform-continuity-pi-search(
    G;
    (x + 1) + (m - 1);x + 1) ∈ {k:{x + 1..((x + 1) + (m - 1)) + 1-}| 
                                P[k]
                                ∧ (∀m:{x + 1..k-}. (¬P[m]))
                                ∧ (∀m:{x + 1..((x + 1) + (m - 1)) + 1-}. (P[m] ⇒ (k ≤ m)))} 
⊢ uniform-continuity-pi-search(
  G;
  x + m;x + 1) ∈ {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  :  \mBbbZ{}
3.  0  <  m
4.  \mforall{}x:\mBbbN{}
          ((\mexists{}n:\{x..(x  +  (m  -  1))  +  1\msupminus{}\}.  P[n])
          {}\mRightarrow{}  (\mforall{}G:\mforall{}m:\mBbbN{}x  +  (m  -  1).  Dec(P[m])
                      (uniform-continuity-pi-search(
                        G;
                        x  +  (m  -  1);x)  \mmember{}  \{k:\{x..(x  +  (m  -  1))  +  1\msupminus{}\}| 
                                                            P[k]
                                                            \mwedge{}  (\mforall{}m:\{x..k\msupminus{}\}.  (\mneg{}P[m]))
                                                            \mwedge{}  (\mforall{}m:\{x..(x  +  (m  -  1))  +  1\msupminus{}\}.  (P[m]  {}\mRightarrow{}  (k  \mleq{}  m)))\}  )))
5.  x  :  \mBbbN{}
6.  \mneg{}((x  +  m)  \mleq{}  x)
7.  \mexists{}n:\{x..(x  +  m)  +  1\msupminus{}\}.  P[n]
8.  G  :  \mforall{}m:\mBbbN{}x  +  m.  Dec(P[m])
9.  y  :  \mneg{}P[x]
10.  (G  x)  =  (inr  y  )
\mvdash{}  uniform-continuity-pi-search(
    G;
    x  +  m;x  +  1)  \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:
(InstHyp  [\mkleeneopen{}x  +  1\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto)

---

Home Index