---

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


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))
⊢ bar(A) ∨ bar(B)
BY
{ (Assert ⌜(∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(A n f))) ∨ (∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(B n f)))⌝⋅
THENM (ParallelLast THEN UnfoldTopAb 0 THEN RepeatFor 2 (ParallelLast))
) }

1
.....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)))

---

Latex:

---

Latex:

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{}  bar(A)  \mvee{}  bar(B)


By

---

Latex:
(Assert  \mkleeneopen{}(\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)))\mkleeneclose{}\mcdot{}
THENM  (ParallelLast  THEN  UnfoldTopAb  0  THEN  RepeatFor  2  (ParallelLast))
)

---

Home Index