---

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


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. ∀f,g:ℕ ⟶ T.  ((∃n:ℕ. (A map(f;upto(n)))) ∨ (∃n:ℕ. (B map(g;upto(n)))))
10. f : ℕ ⟶ T
11. n : ℕ
12. A map(λn.(f (2 * n));upto(n))
⊢ firstn(n;map(λp.(fst(p));unshuffle(map(f;upto(2 * (n + 1)))))) ~ map(λn.(f (2 * n));upto(n))
BY
{ ((RWW "unshuffle-map map-map firstn_map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN EqCD
   THEN Auto'
   THEN RWO "firstn_upto" 0
   THEN Auto
   THEN AutoSplit)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T
3.  size  :  \mBbbN{}
4.  T  \msim{}  \mBbbN{}size
5.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
6.  B  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
7.  Decidable(A)
8.  Decidable(B)
9.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  T.    ((\mexists{}n:\mBbbN{}.  (A  map(f;upto(n))))  \mvee{}  (\mexists{}n:\mBbbN{}.  (B  map(g;upto(n)))))
10.  f  :  \mBbbN{}  {}\mrightarrow{}  T
11.  n  :  \mBbbN{}
12.  A  map(\mlambda{}n.(f  (2  *  n));upto(n))
\mvdash{}  firstn(n;map(\mlambda{}p.(fst(p));unshuffle(map(f;upto(2  *  (n  +  1))))))  \msim{}  map(\mlambda{}n.(f  (2  *  n));upto(n))


By

---

Latex:
((RWW  "unshuffle-map  map-map  firstn\_map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  EqCD
  THEN  Auto'
  THEN  RWO  "firstn\_upto"  0
  THEN  Auto
  THEN  AutoSplit)\mcdot{}

---

Home Index