---

Step * 2 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))
⊢ ∃n:ℕ
   ((∃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))))))))
BY
{ (With ⌜2 * (n + 1)⌝ (D 0)⋅
   THEN Auto'
   THEN (OrLeft THEN Auto)
   THEN (With ⌜n⌝ (D 0)⋅
         THENA (Auto
                THEN (RWW "length-unshuffle map-length length_upto" 0 THENA Auto')
                THEN (RWO "mul_com" 0 THENA Auto)
                THEN RWO "div_mul_cancel" 0⋅
                THEN Auto)
         )
   THEN NthHypSq (-1)
   THEN Auto)⋅ }

1
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))

---

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{}  \mexists{}n:\mBbbN{}
      ((\mexists{}n@0:\mBbbN{}||unshuffle(map(f;upto(n)))||
            (A  firstn(n@0;map(\mlambda{}p.(fst(p));unshuffle(map(f;upto(n)))))))
      \mvee{}  (\mexists{}n@0:\mBbbN{}||unshuffle(map(f;upto(n)))||
              (B  firstn(n@0;map(\mlambda{}p.(snd(p));unshuffle(map(f;upto(n))))))))


By

---

Latex:
(With  \mkleeneopen{}2  *  (n  +  1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto'
  THEN  (OrLeft  THEN  Auto)
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
              THENA  (Auto
                            THEN  (RWW  "length-unshuffle  map-length  length\_upto"  0  THENA  Auto')
                            THEN  (RWO  "mul\_com"  0  THENA  Auto)
                            THEN  RWO  "div\_mul\_cancel"  0\mcdot{}
                            THEN  Auto)
              )
  THEN  NthHypSq  (-1)
  THEN  Auto)\mcdot{}

---

Home Index