---

Step * of Lemma unshuffle-odd-length

∀[f:ℕ ⟶ Top]. ∀[m:ℕ]. ∀[L:ℕ List]. ∀[x:ℕ].
  unshuffle(map(f;L @ [x])) ~ unshuffle(map(f;L)) supposing ||L|| = (2 * m) ∈ ℤ
BY
{ TACTIC:(CompleteInductionOnNat
          THEN (UnivCD THENA Auto)
          THEN DVar
          `L'⋅
          THEN Reduce 0
          THEN Try ((RecUnfold `unshuffle` 0 THEN Reduce 0 THEN Trivial))
          THEN DVar `v') }

1
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;[])])

2
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. u1 : ℕ
6. v : ℕ List
7. x : ℕ
8. ||[u; [u1 / v]]|| = (2 * m) ∈ ℤ
⊢ unshuffle([f u / map(f;[u1 / v] @ [x])]) ~ unshuffle([f u / map(f;[u1 / v])])

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[L:\mBbbN{}  List].  \mforall{}[x:\mBbbN{}].
    unshuffle(map(f;L  @  [x]))  \msim{}  unshuffle(map(f;L))  supposing  ||L||  =  (2  *  m)


By

---

Latex:
TACTIC:(CompleteInductionOnNat
                THEN  (UnivCD  THENA  Auto)
                THEN  DVar
                `L'\mcdot{}
                THEN  Reduce  0
                THEN  Try  ((RecUnfold  `unshuffle`  0  THEN  Reduce  0  THEN  Trivial))
                THEN  DVar  `v')

---

Home Index