---

Step * 2 1 2 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)
⊢ (∀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 Dec(∀f:ℕ(k ÷ 2) + 1 ⟶ T. ∃n:ℕ(k ÷ 2) + 1. (↑(A n f))) BY
          (BLemma `decidable__all_fun`⋅ THEN Auto THEN D 0 With ⌜(k ÷ 2) + 1⌝  THEN Auto))
   THEN D -1
   THEN Try (Complete (Auto))
   THEN (RWO "not-all-finite" (-1) THENA 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)
11. ∃f:ℕ(k ÷ 2) + 1 ⟶ T. (¬(∃n:ℕ(k ÷ 2) + 1. (↑(A 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)))

---

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)
\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  Dec(\mforall{}f:\mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}(k  \mdiv{}  2)  +  1.  (\muparrow{}(A  n  f)))  BY
                (BLemma  `decidable\_\_all\_fun`\mcdot{}  THEN  Auto  THEN  D  0  With  \mkleeneopen{}(k  \mdiv{}  2)  +  1\mkleeneclose{}    THEN  Auto))
  THEN  D  -1
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "not-all-finite"  (-1)  THENA  Auto))

---

Home Index