---

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


1. [T] : Type
2. Fan_d(T)
3. T
4. size : ℕ
5. T ~ ℕsize
6. A : (T List) ⟶ ℙ
7. B : (T List) ⟶ ℙ
8. Decidable(A)
9. Decidable(B)
10. jbar(T;T;A;B)
⊢ tbar(T;A) ∨ tbar(T;B)
BY
{ ((With ⌜λL.((∃n:ℕ||unshuffle(L)||. (A firstn(n;map(λp.(fst(p));unshuffle(L)))))
             ∨ (∃n:ℕ||unshuffle(L)||. (B firstn(n;map(λp.(snd(p));unshuffle(L))))))⌝ (D 2)⋅
    THENA Auto
    )
   THEN RepUR ``dbar ubar dec-predicate`` -1
   THEN D -1) }

1
.....antecedent..... 
1. [T] : Type
2. T
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
⊢ (∀t:T List
     Dec((∃n:ℕ||unshuffle(t)||. (A firstn(n;map(λp.(fst(p));unshuffle(t)))))
     ∨ (∃n:ℕ||unshuffle(t)||. (B firstn(n;map(λp.(snd(p));unshuffle(t)))))))
∧ tbar(T;λL.((∃n:ℕ||unshuffle(L)||. (A firstn(n;map(λp.(fst(p));unshuffle(L)))))
            ∨ (∃n:ℕ||unshuffle(L)||. (B firstn(n;map(λp.(snd(p));unshuffle(L)))))))

2
1. [T] : Type
2. T
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. ∃k:ℕ
     ∀f:ℕ ⟶ T
       ∃n:ℕk
        ((∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (A firstn(n@0;map(λp.(fst(p));unshuffle(map(f;upto(n)))))))
        ∨ (∃n@0:ℕ||unshuffle(map(f;upto(n)))||. (B firstn(n@0;map(λp.(snd(p));unshuffle(map(f;upto(n))))))))
⊢ tbar(T;A) ∨ tbar(T;B)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  Fan\_d(T)
3.  T
4.  size  :  \mBbbN{}
5.  T  \msim{}  \mBbbN{}size
6.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
7.  B  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
8.  Decidable(A)
9.  Decidable(B)
10.  jbar(T;T;A;B)
\mvdash{}  tbar(T;A)  \mvee{}  tbar(T;B)


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}L.((\mexists{}n:\mBbbN{}||unshuffle(L)||.  (A  firstn(n;map(\mlambda{}p.(fst(p));unshuffle(L)))))
                      \mvee{}  (\mexists{}n:\mBbbN{}||unshuffle(L)||.  (B  firstn(n;map(\mlambda{}p.(snd(p));unshuffle(L))))))\mkleeneclose{}  (D  2)\mcdot{}
    THENA  Auto
    )
  THEN  RepUR  ``dbar  ubar  dec-predicate``  -1
  THEN  D  -1)

---

Home Index