---

Step * 2 1 2 1 1 1 1 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))
10. ℕ(k ÷ 2) + 1 ⟶ T ~ ℕsize^((k ÷ 2) + 1)
11. ∃f:ℕ(k ÷ 2) + 1 ⟶ T. (¬(∃n:ℕ(k ÷ 2) + 1. (↑(A n f))))
12. ∃f:ℕ(k ÷ 2) + 1 ⟶ T. (¬(∃n:ℕ(k ÷ 2) + 1. (↑(B n f))))
⊢ (∀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 ⌜False⌝⋅ THEN Auto) THEN ExRepD) }

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)
11. f1 : ℕ(k ÷ 2) + 1 ⟶ T
12. ¬(∃n:ℕ(k ÷ 2) + 1. (↑(A n f1)))
13. f : ℕ(k ÷ 2) + 1 ⟶ T
14. ¬(∃n:ℕ(k ÷ 2) + 1. (↑(B n f)))
⊢ False

---

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))
10.  \mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T  \msim{}  \mBbbN{}size\^{}((k  \mdiv{}  2)  +  1)
11.  \mexists{}f:\mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T.  (\mneg{}(\mexists{}n:\mBbbN{}(k  \mdiv{}  2)  +  1.  (\muparrow{}(A  n  f))))
12.  \mexists{}f:\mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T.  (\mneg{}(\mexists{}n:\mBbbN{}(k  \mdiv{}  2)  +  1.  (\muparrow{}(B  n  f))))
\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  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  ExRepD)

---

Home Index