---

Step * 1 of Lemma unshuffle-odd-length


1. f : ℕ ⟶ Top
2. m : ℕ
3. ∀m:ℕm. ∀[L:ℕ List]. ∀[x:ℕ].  unshuffle(map(f;L @ [x])) ~ unshuffle(map(f;L)) supposing ||L|| = (2 * m) ∈ ℤ
4. u : ℕ
5. x : ℕ
6. ||[u]|| = (2 * m) ∈ ℤ
⊢ unshuffle([f u / map(f;[] @ [x])]) ~ unshuffle([f u / map(f;[])])
BY
{ (Reduce -1 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  Top
2.  m  :  \mBbbN{}
3.  \mforall{}m:\mBbbN{}m
          \mforall{}[L:\mBbbN{}  List].  \mforall{}[x:\mBbbN{}].    unshuffle(map(f;L  @  [x]))  \msim{}  unshuffle(map(f;L))  supposing  ||L||  =  (2  *  m)
4.  u  :  \mBbbN{}
5.  x  :  \mBbbN{}
6.  ||[u]||  =  (2  *  m)
\mvdash{}  unshuffle([f  u  /  map(f;[]  @  [x])])  \msim{}  unshuffle([f  u  /  map(f;[])])


By

---

Latex:
(Reduce  -1  THEN  Auto)

---

Home Index