---

Step * 2 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. f : ℕ ⟶ T
⊢ ∃n:ℕ. (↑((∃i<n ÷ 2.A i (λk.(f (2 * k))))_b ∨b(∃i<n ÷ 2.B i (λk.(f ((2 * k) + 1))))_b))
BY
{ (UnfoldTopAb (-2)
   THEN (InstHyp [⌜λn.(f (2 * n))⌝;⌜λn.(f ((2 * n) + 1))⌝] (-2) ⋅ THENA Auto')
   THEN ((RepeatFor 2 (D -1)
          THEN (D 0 With ⌜(2 * (n + 1)) + 1⌝  THENA Auto)
          THEN (Subst' ((2 * (n + 1)) + 1) ÷ 2 ~ n + 1 0 THENA Auto)
          THEN (RW assert_pushdownC 0 THENA Auto))
         THENL [(OrLeft THENA Auto); (OrRight THENA Auto)]
   )
   THEN RWO "assert-b-exists" 0
   THEN Auto) }

---

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.  f  :  \mBbbN{}  {}\mrightarrow{}  T
\mvdash{}  \mexists{}n:\mBbbN{}.  (\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))


By

---

Latex:
(UnfoldTopAb  (-2)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}n.(f  (2  *  n))\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(f  ((2  *  n)  +  1))\mkleeneclose{}]  (-2)  \mcdot{}  THENA  Auto')
  THEN  ((RepeatFor  2  (D  -1)
                THEN  (D  0  With  \mkleeneopen{}(2  *  (n  +  1))  +  1\mkleeneclose{}    THENA  Auto)
                THEN  (Subst'  ((2  *  (n  +  1))  +  1)  \mdiv{}  2  \msim{}  n  +  1  0  THENA  Auto)
                THEN  (RW  assert\_pushdownC  0  THENA  Auto))
              THENL  [(OrLeft  THENA  Auto);  (OrRight  THENA  Auto)]
  )
  THEN  RWO  "assert-b-exists"  0
  THEN  Auto)

---

Home Index