---

Step * 1 1 of Lemma unshuffle-map


1. f : ℕ ⟶ Top
2. d : ℤ
3. 0 < d
4. ∀k:ℕ. ∀i:ℕk + 1.
     (((k - i) ≤ (d - 1)) ⇒ (map(f;[2 * i, 2 * k)) ~ shuffle(map(λi.<f (2 * i), f ((2 * i) + 1)>;[i, k)))))
5. k : ℕ
6. i : ℕk + 1
7. (k - i) ≤ d
8. 2 * i < 2 * k
⊢ map(f;[(2 * i) + 1, 2 * k)) ~ [f ((2 * i) + 1) / map(f;[2 * (i + 1), 2 * k))]
BY
{ (RW (AddrC [1] (RecUnfoldC `from-upto`)) 0
   THEN AutoSplit
   THEN Auto'
   THEN (CallByValueReduce 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  Top
2.  d  :  \mBbbZ{}
3.  0  <  d
4.  \mforall{}k:\mBbbN{}.  \mforall{}i:\mBbbN{}k  +  1.
          (((k  -  i)  \mleq{}  (d  -  1))
          {}\mRightarrow{}  (map(f;[2  *  i,  2  *  k))  \msim{}  shuffle(map(\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>[i,  k)))))
5.  k  :  \mBbbN{}
6.  i  :  \mBbbN{}k  +  1
7.  (k  -  i)  \mleq{}  d
8.  2  *  i  <  2  *  k
\mvdash{}  map(f;[(2  *  i)  +  1,  2  *  k))  \msim{}  [f  ((2  *  i)  +  1)  /  map(f;[2  *  (i  +  1),  2  *  k))]


By

---

Latex:
(RW  (AddrC  [1]  (RecUnfoldC  `from-upto`))  0
  THEN  AutoSplit
  THEN  Auto'
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index