Step
*
1
1
3
1
of Lemma
fan-implies-nwkl!-using-PFan
.....aux.....
1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. ∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
7. n : ℕ
8. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
9. k : ℕ
10. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ ((λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))) map(gh;upto(k))))
⊢ n < imax(k;n + 1)
∧ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ ((λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))) map(gh;upto(imax(k;n + 1))))))
BY
{ D 0 }
1
1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. ∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
7. n : ℕ
8. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
9. k : ℕ
10. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ ((λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))) map(gh;upto(k))))
⊢ n < imax(k;n + 1)
2
1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. ∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
7. n : ℕ
8. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
9. k : ℕ
10. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ ((λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))) map(gh;upto(k))))
⊢ ∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ ((λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))) map(gh;upto(imax(k;n + 1)))))
Latex:
Latex:
.....aux.....
1. Fan
2. t : (\mBbbB{} List) {}\mrightarrow{} \mBbbP{}
3. \mforall{}as:\mBbbB{} List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. \mforall{}n:\mBbbN{}. \mforall{}ss:((\mBbbB{} \mtimes{} \mBbbB{}) List) {}\mrightarrow{} \mBbbP{}.
((\mforall{}bc:(\mBbbB{} \mtimes{} \mBbbB{}) List. Dec(ss bc))
{}\mRightarrow{} (\mforall{}bc,bc':(\mBbbB{} \mtimes{} \mBbbB{}) List. (bc \mleq{} bc' {}\mRightarrow{} (ss bc) {}\mRightarrow{} (ss bc')))
{}\mRightarrow{} (\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (\mexists{}m:\mBbbN{}. (ss map(gh;upto(m))))))
{}\mRightarrow{} (\mexists{}k:\mBbbN{}
\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (ss map(gh;upto(k))))))
7. n : \mBbbN{}
8. \mforall{}ss:((\mBbbB{} \mtimes{} \mBbbB{}) List) {}\mrightarrow{} \mBbbP{}
((\mforall{}bc:(\mBbbB{} \mtimes{} \mBbbB{}) List. Dec(ss bc))
{}\mRightarrow{} (\mforall{}bc,bc':(\mBbbB{} \mtimes{} \mBbbB{}) List. (bc \mleq{} bc' {}\mRightarrow{} (ss bc) {}\mRightarrow{} (ss bc')))
{}\mRightarrow{} (\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (\mexists{}m:\mBbbN{}. (ss map(gh;upto(m))))))
{}\mRightarrow{} (\mexists{}k:\mBbbN{}
\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} (ss map(gh;upto(k))))))
9. k : \mBbbN{}
10. \mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} ((\mlambda{}bc.(\mneg{}((t map(\mlambda{}p.(fst(p));bc)) \mwedge{} (t map(\mlambda{}p.(snd(p));bc))))) map(gh;upto(k))))
\mvdash{} n < imax(k;n + 1)
\mwedge{} (\mforall{}gh:\mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
((\mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n))))
{}\mRightarrow{} ((\mlambda{}bc.(\mneg{}((t map(\mlambda{}p.(fst(p));bc)) \mwedge{} (t map(\mlambda{}p.(snd(p));bc))))) map(gh;upto(imax(k;n + 1))))))
By
Latex:
D 0
Home
Index