---

Step * 2 of Lemma fan-bar-sep


1. [T] : Type
2. Fan(T)
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. ¬(size = 0 ∈ ℤ)
⊢ bar(A) ∨ bar(B)
BY
{ ((Assert ⌜T⌝⋅ BY
          (D 4 THEN D 5 THEN With ⌜0⌝ (D 6)⋅ THEN ExRepD THEN Auto))
   THEN Thin (-2)
   THEN PromoteHyp (-1) 3
   THEN (With ⌜λn,f. ((∃i<n ÷ 2.A i (λk.(f (2 * k))))_b ∨b(∃i<n ÷ 2.B i (λk.(f ((2 * k) + 1))))_b)⌝ (D 2)⋅
         THENA (Auto
                THEN (InstLemma `div_rem_sum` [⌜n⌝;⌜2⌝]⋅ THENA Auto)
                THEN InstLemma `rem_bounds_1` [⌜n⌝;⌜2⌝]⋅
                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. bar(λn,f. ((∃i<n ÷ 2.A i (λk.(f (2 * k))))_b ∨b(∃i<n ÷ 2.B i (λk.(f ((2 * k) + 1))))_b))
⇒ uniformBar(λn,f. ((∃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)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  Fan(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.  \mneg{}(size  =  0)
\mvdash{}  bar(A)  \mvee{}  bar(B)


By

---

Latex:
((Assert  \mkleeneopen{}T\mkleeneclose{}\mcdot{}  BY
                (D  4  THEN  D  5  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  6)\mcdot{}  THEN  ExRepD  THEN  Auto))
  THEN  Thin  (-2)
  THEN  PromoteHyp  (-1)  3
  THEN  (With  \mkleeneopen{}\mlambda{}n,f.  ((\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)\mkleeneclose{}  (D\000C  2)\mcdot{}
              THENA  (Auto
                            THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
                            THEN  Auto)
              ))\mcdot{}

---

Home Index