---

Step * 2 1 2 1 1 of Lemma fan-bar-sep

.....assertion..... 
1. [T] : Type
2. T
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. k : ℕ
9. ∀f:ℕ ⟶ T. ∃n:ℕk. (↑((∃i<n ÷ 2.A i (λk.(f (2 * k))))_b ∨b(∃i<n ÷ 2.B i (λk.(f ((2 * k) + 1))))_b))
⊢ (∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(A n f))) ∨ (∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(B n f)))
BY
{ (Assert ℕ(k ÷ 2) + 1 ⟶ T ~ ℕsize^((k ÷ 2) + 1) BY
         ((Assert ℕ(k ÷ 2) + 1 ⟶ ℕsize ~ ℕsize^((k ÷ 2) + 1) BY
                 Auto)
          THEN (RWO "-1<" 0 THENA Auto)
          THEN RWO "4" 0
          THEN Auto)) }

1
1. [T] : Type
2. T
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. k : ℕ
9. ∀f:ℕ ⟶ T. ∃n:ℕk. (↑((∃i<n ÷ 2.A i (λk.(f (2 * k))))_b ∨b(∃i<n ÷ 2.B i (λk.(f ((2 * k) + 1))))_b))
10. ℕ(k ÷ 2) + 1 ⟶ T ~ ℕsize^((k ÷ 2) + 1)
⊢ (∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(A n f))) ∨ (∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(B n f)))

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  T
3.  size  :  \mBbbN{}
4.  T  \msim{}  \mBbbN{}size
5.  A  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}
6.  B  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}
7.  jbar(A;B)
8.  k  :  \mBbbN{}
9.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
          \mexists{}n:\mBbbN{}k.  (\muparrow{}((\mexists{}i<n  \mdiv{}  2.A  i  (\mlambda{}k.(f  (2  *  k))))\_b  \mvee{}\msubb{}(\mexists{}i<n  \mdiv{}  2.B  i  (\mlambda{}k.(f  ((2  *  k)  +  1))))\_b))
\mvdash{}  (\mforall{}f:\mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}(k  \mdiv{}  2)  +  1.  (\muparrow{}(A  n  f)))
\mvee{}  (\mforall{}f:\mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}(k  \mdiv{}  2)  +  1.  (\muparrow{}(B  n  f)))


By

---

Latex:
(Assert  \mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T  \msim{}  \mBbbN{}size\^{}((k  \mdiv{}  2)  +  1)  BY
              ((Assert  \mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  \mBbbN{}size  \msim{}  \mBbbN{}size\^{}((k  \mdiv{}  2)  +  1)  BY
                              Auto)
                THEN  (RWO  "-1<"  0  THENA  Auto)
                THEN  RWO  "4"  0
                THEN  Auto))

---

Home Index