---

Step * 1 2 of Lemma fan-implies-PFan


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. ∃k:ℕ
    ∀f:ℕ ⟶ 𝔹
      ∃n@0:ℕk
       (((2 * n) ≤ ||map(f;upto(n@0))||)
       ∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))
⊢ ∃k:ℕ
   ∀gh:ℕ ⟶ (𝔹 × 𝔹)
     ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))
BY
{ Assert ⌜∃k:ℕ
           ((n ≤ k)
           ∧ (∀f:ℕ ⟶ 𝔹
                ∃m:ℕ2 * k
                 (((2 * n) ≤ ||map(f;upto(m))||)
                 ∧ (∀i:ℕn
                      ((¬map(f;upto(m))[2 * i] = map(f;upto(m))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(m)))))))))⌝⋅ }

1
.....assertion..... 
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. ∃k:ℕ
    ∀f:ℕ ⟶ 𝔹
      ∃n@0:ℕk
       (((2 * n) ≤ ||map(f;upto(n@0))||)
       ∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))
⊢ ∃k:ℕ
   ((n ≤ k)
   ∧ (∀f:ℕ ⟶ 𝔹
        ∃m:ℕ2 * k
         (((2 * n) ≤ ||map(f;upto(m))||)
         ∧ (∀i:ℕn. ((¬map(f;upto(m))[2 * i] = map(f;upto(m))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(m)))))))))

2
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. ∃k:ℕ
    ∀f:ℕ ⟶ 𝔹
      ∃n@0:ℕk
       (((2 * n) ≤ ||map(f;upto(n@0))||)
       ∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))
8. ∃k:ℕ
    ((n ≤ k)
    ∧ (∀f:ℕ ⟶ 𝔹
         ∃m:ℕ2 * k
          (((2 * n) ≤ ||map(f;upto(m))||)
          ∧ (∀i:ℕn. ((¬map(f;upto(m))[2 * i] = map(f;upto(m))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(m)))))))))
⊢ ∃k:ℕ
   ∀gh:ℕ ⟶ (𝔹 × 𝔹)
     ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))

---

Latex:

---

Latex:

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.  \mexists{}k:\mBbbN{}
        \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}
            \mexists{}n@0:\mBbbN{}k
              (((2  *  n)  \mleq{}  ||map(f;upto(n@0))||)
              \mwedge{}  (\mforall{}i:\mBbbN{}n
                        ((\mneg{}map(f;upto(n@0))[2  *  i]  =  map(f;upto(n@0))[(2  *  i)  +  1])
                        {}\mRightarrow{}  (ss  unshuffle(map(f;upto(n@0)))))))
\mvdash{}  \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))))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}
                  ((n  \mleq{}  k)
                  \mwedge{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}
                            \mexists{}m:\mBbbN{}2  *  k
                              (((2  *  n)  \mleq{}  ||map(f;upto(m))||)
                              \mwedge{}  (\mforall{}i:\mBbbN{}n
                                        ((\mneg{}map(f;upto(m))[2  *  i]  =  map(f;upto(m))[(2  *  i)  +  1])
                                        {}\mRightarrow{}  (ss  unshuffle(map(f;upto(m)))))))))\mkleeneclose{}\mcdot{}

---

Home Index