---

Step * 2 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. 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])])
BY
{ (Reduce 0
   THEN RecUnfold `unshuffle` 0
   THEN Reduce 0
   THEN (Subst' unshuffle(map(f;v @ [x])) ~ unshuffle(map(f;v)) 0
         THENA ((D 3 With ⌜m - 1⌝  THENA Auto) THEN BHyp -1 THEN Auto')
         )
   THEN EqCD
   THEN Try (Trivial)) }

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

---

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.  u1  :  \mBbbN{}
6.  v  :  \mBbbN{}  List
7.  x  :  \mBbbN{}
8.  ||[u;  [u1  /  v]]||  =  (2  *  m)
\mvdash{}  unshuffle([f  u  /  map(f;[u1  /  v]  @  [x])])  \msim{}  unshuffle([f  u  /  map(f;[u1  /  v])])


By

---

Latex:
(Reduce  0
  THEN  RecUnfold  `unshuffle`  0
  THEN  Reduce  0
  THEN  (Subst'  unshuffle(map(f;v  @  [x]))  \msim{}  unshuffle(map(f;v))  0
              THENA  ((D  3  With  \mkleeneopen{}m  -  1\mkleeneclose{}    THENA  Auto)  THEN  BHyp  -1  THEN  Auto')
              )
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index