---

Step * 2 of Lemma unshuffle-map'


1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. ¬(r = 0 ∈ ℤ)
⊢ unshuffle(map(f;upto((2 * m) + r))) ~ unshuffle(map(f;upto(2 * m)))
BY
{ Subst ⌜r ~ 1⌝ 0⋅ }

1
.....equality..... 
1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. ¬(r = 0 ∈ ℤ)
⊢ r ~ 1

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

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  Top
2.  m  :  \mBbbN{}
3.  r  :  \mBbbN{}2
4.  \mneg{}(r  =  0)
\mvdash{}  unshuffle(map(f;upto((2  *  m)  +  r)))  \msim{}  unshuffle(map(f;upto(2  *  m)))


By

---

Latex:
Subst  \mkleeneopen{}r  \msim{}  1\mkleeneclose{}  0\mcdot{}

---

Home Index