---

Step * 2 2 1 of Lemma unshuffle-map'

.....equality..... 
1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. ¬(r = 0 ∈ ℤ)
⊢ upto((2 * m) + 1) ~ upto(2 * m) @ [2 * m]
BY
{ (RW (AddrC [1] (LemmaC `upto_decomp1`)) 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  f  :  \mBbbN{}  {}\mrightarrow{}  Top
2.  m  :  \mBbbN{}
3.  r  :  \mBbbN{}2
4.  \mneg{}(r  =  0)
\mvdash{}  upto((2  *  m)  +  1)  \msim{}  upto(2  *  m)  @  [2  *  m]


By

---

Latex:
(RW  (AddrC  [1]  (LemmaC  `upto\_decomp1`))  0  THEN  Auto)

---

Home Index