Step
*
1
1
of Lemma
fan-implies-nwkl!-using-PFan
.....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))))))
⊢ ∀n:ℕ
∃k:ℕ
((n ≤ k)
∧ (∀b,c:𝔹 List. ((||b|| = k ∈ ℤ) ⇒ (||c|| = k ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
BY
{ (ParallelLast
THEN InstHyp [⌜λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))⌝] (-1)⋅
THEN Reduce 0
THEN Auto) }
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. bc : (𝔹 × 𝔹) List
10. bc' : (𝔹 × 𝔹) List
11. bc ≤ bc'
12. ¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc)))
⊢ ¬((t map(λp.(fst(p));bc')) ∧ (t map(λp.(snd(p));bc')))
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))
⊢ ∃m:ℕ. (¬((t map(λp.(fst(p));map(gh;upto(m)))) ∧ (t map(λp.(snd(p));map(gh;upto(m))))))
3
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:ℕ
∀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))))
⊢ ∃k:ℕ
((n ≤ k)
∧ (∀b,c:𝔹 List. ((||b|| = k ∈ ℤ) ⇒ (||c|| = k ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
Latex:
Latex:
.....assertion.....
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))))))
\mvdash{} \mforall{}n:\mBbbN{}
\mexists{}k:\mBbbN{}
((n \mleq{} k)
\mwedge{} (\mforall{}b,c:\mBbbB{} List.
((||b|| = k) {}\mRightarrow{} (||c|| = k) {}\mRightarrow{} (t b) {}\mRightarrow{} (t c) {}\mRightarrow{} (firstn(n;b) = firstn(n;c)))))
By
Latex:
(ParallelLast
THEN InstHyp [\mkleeneopen{}\mlambda{}bc.(\mneg{}((t map(\mlambda{}p.(fst(p));bc)) \mwedge{} (t map(\mlambda{}p.(snd(p));bc))))\mkleeneclose{}] (-1)\mcdot{}
THEN Reduce 0
THEN Auto)
Home
Index