---

Step * 1 1 3 2 1 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. k : ℕ
10. n < k
11. ∀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))))
12. n ≤ k
13. b : 𝔹 List
14. c : 𝔹 List
15. ||b|| = k ∈ ℤ
16. ||c|| = k ∈ ℤ
17. t b
18. t c
19. ¬(firstn(n;b) = firstn(n;c) ∈ (𝔹 List))
⊢ firstn(n;b) = firstn(n;c) ∈ (𝔹 List)
BY
{ OnMaybeHyp 11 (\h. (InstHyp [⌜λi.if i <z k then <b[i], c[i]> else <tt, tt> fi ⌝] h⋅ THEN Auto)) }

1
.....antecedent..... 
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. n < k
11. ∀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))))
12. n ≤ k
13. b : 𝔹 List
14. c : 𝔹 List
15. ||b|| = k ∈ ℤ
16. ||c|| = k ∈ ℤ
17. t b
18. t c
19. ¬(firstn(n;b) = firstn(n;c) ∈ (𝔹 List))
⊢ ¬(map(λi.(fst(((λi.if i <z k then <b[i], c[i]> else <tt, tt> fi ) i)));upto(n))
= map(λi.(snd(((λi.if i <z k then <b[i], c[i]> else <tt, tt> fi ) i)));upto(n))
∈ (𝔹 List))

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. n < k
11. ∀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))))
12. n ≤ k
13. b : 𝔹 List
14. c : 𝔹 List
15. ||b|| = k ∈ ℤ
16. ||c|| = k ∈ ℤ
17. t b
18. t c
19. ¬(firstn(n;b) = firstn(n;c) ∈ (𝔹 List))
20. (λbc.(¬((t map(λp.(fst(p));bc)) ∧ (t map(λp.(snd(p));bc))))) 
    map(λi.if i <z k then <b[i], c[i]> else <tt, tt> fi ;upto(k))
⊢ firstn(n;b) = firstn(n;c) ∈ (𝔹 List)

---

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.  k  :  \mBbbN{}
10.  n  <  k
11.  \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))))
12.  n  \mleq{}  k
13.  b  :  \mBbbB{}  List
14.  c  :  \mBbbB{}  List
15.  ||b||  =  k
16.  ||c||  =  k
17.  t  b
18.  t  c
19.  \mneg{}(firstn(n;b)  =  firstn(n;c))
\mvdash{}  firstn(n;b)  =  firstn(n;c)


By

---

Latex:
OnMaybeHyp  11  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}\mlambda{}i.if  i  <z  k  then  <b[i],  c[i]>  else  <tt,  tt>  fi  \mkleeneclose{}]  h\mcdot{}  THEN  Auto))

---

Home Index