---

Step * 1 1 1 1 of Lemma fan-implies-PFan

.....antecedent..... 
1. ∀A:(𝔹 List) ⟶ ℙ
     ((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
2. n : ℕ@i
3. ss : ((𝔹 × 𝔹) List) ⟶ ℙ@i'
4. ∀bc:(𝔹 × 𝔹) List. Dec(ss bc)
5. ∀bc,bc':(𝔹 × 𝔹) List.  (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc'))
6. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
     ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (∃m:ℕ. (ss map(gh;upto(m)))))
7. f : ℕ ⟶ 𝔹@i
8. ∃i:ℕn. (¬f (2 * i) = f ((2 * i) + 1))
⊢ ¬(map(λi.(fst(((λi.<f (2 * i), f ((2 * i) + 1)>) i)));upto(n))
= map(λi.(snd(((λi.<f (2 * i), f ((2 * i) + 1)>) i)));upto(n))
∈ (𝔹 List))
BY
{ (Reduce 0
   THEN D 0
   THEN Auto'
   THEN ExRepD
   THEN (ApFunToHypEquands `Z' ⌜if i <z ||Z|| then Z[i] else tt fi ⌝ ⌜𝔹⌝ (-1)⋅ THENA (Try (AutoSplit) THEN Auto))
   THEN (RWW "map-length length_upto" (-1) THENA Auto')
   THEN SplitOnHypITE -1 
   THEN Auto
   THEN RWW "select-map select-upto" (-2)⋅
   THEN Auto'
   THEN (RWW "length_upto" 0 THEN Auto')⋅) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  \mforall{}A:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}as:\mBbbB{}  List.  Dec(A  as))
          {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}.  (A  map(f;upto(n))))
          {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  (A  map(f;upto(n)))))
2.  n  :  \mBbbN{}@i
3.  ss  :  ((\mBbbB{}  \mtimes{}  \mBbbB{})  List)  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mforall{}bc:(\mBbbB{}  \mtimes{}  \mBbbB{})  List.  Dec(ss  bc)
5.  \mforall{}bc,bc':(\mBbbB{}  \mtimes{}  \mBbbB{})  List.    (bc  \mleq{}  bc'  {}\mRightarrow{}  (ss  bc)  {}\mRightarrow{}  (ss  bc'))
6.  \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)))))
7.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
8.  \mexists{}i:\mBbbN{}n.  (\mneg{}f  (2  *  i)  =  f  ((2  *  i)  +  1))
\mvdash{}  \mneg{}(map(\mlambda{}i.(fst(((\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>)  i)));upto(n))
=  map(\mlambda{}i.(snd(((\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>)  i)));upto(n)))


By

---

Latex:
(Reduce  0
  THEN  D  0
  THEN  Auto'
  THEN  ExRepD
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}if  i  <z  ||Z||  then  Z[i]  else  tt  fi  \mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}
              THENA  (Try  (AutoSplit)  THEN  Auto)
              )
  THEN  (RWW  "map-length  length\_upto"  (-1)  THENA  Auto')
  THEN  SplitOnHypITE  -1 
  THEN  Auto
  THEN  RWW  "select-map  select-upto"  (-2)\mcdot{}
  THEN  Auto'
  THEN  (RWW  "length\_upto"  0  THEN  Auto')\mcdot{})

---

Home Index