---

Step * 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
⊢ [f (2 * i) / map(f;eval n' = (2 * i) + 1 in [n', 2 * k))] ~ concat([[f (2 * i); f ((2 * i) + 1)] / 
                                                                    map(λp.[fst(p); snd(p)];map(λi.<f (2 * i)
                                                                                                   , f ((2 * i) + 1)
                                                                                                   >;eval n' = i + 1 in
                                                                                                     [n', k)))])
BY
{ (Unfold `concat` 0
   THEN Reduce 0
   THEN Fold `concat` 0
   THEN Auto
   THEN Fold `shuffle` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RWO "4<" 0
   THEN Auto') }

1
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))]

---

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{}  [f  (2  *  i)  /  map(f;eval  n'  =  (2  *  i)  +  1  in  [n',  2  *  k))]  \msim{}  concat([[f  (2  *  i);  f  ((2  *  i)  +  1)]  /\000C 
                                                                                                                                        map(\mlambda{}p.[fst(p);  snd(p)];
                                                                                                                                                map(\mlambda{}i.<f  (2  *  i)
                                                                                                                                                              ,  f  ((2  *  i)  +  1)
                                                                                                                                                              >eval  n'  =  i  +  1  in
                                                                                                                                                                  [n',  k)))])


By

---

Latex:
(Unfold  `concat`  0
  THEN  Reduce  0
  THEN  Fold  `concat`  0
  THEN  Auto
  THEN  Fold  `shuffle`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RWO  "4<"  0
  THEN  Auto')

---

Home Index