---

Step * 2 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. 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
BY
{ (GenConclTerms Auto [⌜||map(f;v @ [x])||⌝;⌜||map(f;v)||⌝]⋅ THEN All Thin) }

1
1. v1 : ℕ
2. v2 : ℕ
⊢ (v1 + 1) + 1 <z 2 ~ (v2 + 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{}  (||map(f;v  @  [x])||  +  1)  +  1  <z  2  \msim{}  (||map(f;v)||  +  1)  +  1  <z  2


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}||map(f;v  @  [x])||\mkleeneclose{};\mkleeneopen{}||map(f;v)||\mkleeneclose{}]\mcdot{}  THEN  All  Thin)

---

Home Index