Step
*
1
1
2
of Lemma
fan-implies-nwkl!-using-PFan
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. gh : ℕ ⟶ (𝔹 × 𝔹)
10. ¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))
⊢ ∃m:ℕ. (¬((t map(λp.(fst(p));map(gh;upto(m)))) ∧ (t map(λp.(snd(p));map(gh;upto(m))))))
BY
{ Assert ⌜∃i:ℕn. (¬fst((gh i)) = snd((gh i)))⌝⋅ }
1
.....assertion.....
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. gh : ℕ ⟶ (𝔹 × 𝔹)
10. ¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))
⊢ ∃i:ℕn. (¬fst((gh i)) = snd((gh i)))
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. gh : ℕ ⟶ (𝔹 × 𝔹)
10. ¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))
11. ∃i:ℕn. (¬fst((gh i)) = snd((gh i)))
⊢ ∃m:ℕ. (¬((t map(λp.(fst(p));map(gh;upto(m)))) ∧ (t map(λp.(snd(p));map(gh;upto(m))))))
Latex:
Latex:
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. gh : \mBbbN{} {}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbB{})
10. \mneg{}(map(\mlambda{}i.(fst((gh i)));upto(n)) = map(\mlambda{}i.(snd((gh i)));upto(n)))
\mvdash{} \mexists{}m:\mBbbN{}. (\mneg{}((t map(\mlambda{}p.(fst(p));map(gh;upto(m)))) \mwedge{} (t map(\mlambda{}p.(snd(p));map(gh;upto(m))))))
By
Latex:
Assert \mkleeneopen{}\mexists{}i:\mBbbN{}n. (\mneg{}fst((gh i)) = snd((gh i)))\mkleeneclose{}\mcdot{}
Home
Index