---

Step * of Lemma unshuffle-map'

∀[f:ℕ ⟶ Top]. ∀[m:ℕ]. ∀[r:ℕ2].  (unshuffle(map(f;upto((2 * m) + r))) ~ map(λi.<f (2 * i), f ((2 * i) + 1)>;upto(m)))
BY
{ (Auto THEN (RWO "unshuffle-map<" 0 THENA Auto) THEN CaseNat 0 `r') }

1
1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. r = 0 ∈ ℤ
⊢ unshuffle(map(f;upto((2 * m) + 0))) ~ unshuffle(map(f;upto(2 * m)))

2
1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. ¬(r = 0 ∈ ℤ)
⊢ unshuffle(map(f;upto((2 * m) + r))) ~ unshuffle(map(f;upto(2 * m)))

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[r:\mBbbN{}2].
    (unshuffle(map(f;upto((2  *  m)  +  r)))  \msim{}  map(\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>upto(m)))


By

---

Latex:
(Auto  THEN  (RWO  "unshuffle-map<"  0  THENA  Auto)  THEN  CaseNat  0  `r')

---

Home Index