---

Step * 2 2 2 of Lemma unshuffle-map'


1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. ¬(r = 0 ∈ ℤ)
⊢ unshuffle(map(f;upto(2 * m) @ [2 * m])) ~ unshuffle(map(f;upto(2 * m)))
BY
{ (Reduce 0
   THEN (InstLemma `unshuffle-odd-length` [⌜f⌝;⌜m⌝]⋅ THENA Auto)
   THEN BHyp (-1)
   THEN Auto'
   THEN RWO "length_upto" 0
   THEN Auto') }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  Top
2.  m  :  \mBbbN{}
3.  r  :  \mBbbN{}2
4.  \mneg{}(r  =  0)
\mvdash{}  unshuffle(map(f;upto(2  *  m)  @  [2  *  m]))  \msim{}  unshuffle(map(f;upto(2  *  m)))


By

---

Latex:
(Reduce  0
  THEN  (InstLemma  `unshuffle-odd-length`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  (-1)
  THEN  Auto'
  THEN  RWO  "length\_upto"  0
  THEN  Auto')

---

Home Index