Step
*
1
1
1
1
2
2
of Lemma
uniform-continuity-pi-search-prop1
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]))} )))
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]))}
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]))} )))
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]))} )))
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]))}
⊢ uniform-continuity-pi-search(
G;
x + m;x + 1) ∈ {k:{x..(x + m) + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[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]))\} )))
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]))\}
By
Latex:
(InstHyp [\mkleeneopen{}x + 1\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}] (-7)\mcdot{} THENA Auto)
Home
Index