---

Step * of Lemma unshuffle-map

∀[f:ℕ ⟶ Top]. ∀[m:ℕ].  (unshuffle(map(f;upto(2 * m))) ~ map(λi.<f (2 * i), f ((2 * i) + 1)>;upto(m)))
BY
{ (Auto
   THEN Subst ⌜map(f;upto(2 * m)) ~ shuffle(map(λi.<f (2 * i), f ((2 * i) + 1)>;upto(m)))⌝ 0⋅
   THEN RWW "unshuffle-shuffle" 0
   THEN Auto'
   THEN Unfold `upto` 0
   THEN Assert ⌜∀d,k:ℕ. ∀i:ℕk + 1.
                  (((k - i) ≤ d) ⇒ (map(f;[2 * i, 2 * k)) ~ shuffle(map(λi.<f (2 * i), f ((2 * i) + 1)>;[i, k)))))⌝⋅
   THEN Try (((InstHyp [⌜m⌝] (-1)⋅ THENA Auto) THEN RWO "-1<" 0 THEN Auto'))
   THEN Thin (-1)
   THEN InductionOnNat
   THEN Auto
   THEN RecUnfold `from-upto` 0
   THEN AutoSplit
   THEN Unfold `shuffle` 0
   THEN Reduce 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
⊢ [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)))])

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  Top].  \mforall{}[m:\mBbbN{}].
    (unshuffle(map(f;upto(2  *  m)))  \msim{}  map(\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>upto(m)))


By

---

Latex:
(Auto
  THEN  Subst  \mkleeneopen{}map(f;upto(2  *  m))  \msim{}  shuffle(map(\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>upto(m)))\mkleeneclose{}  0\mcdot{}
  THEN  RWW  "unshuffle-shuffle"  0
  THEN  Auto'
  THEN  Unfold  `upto`  0
  THEN  Assert  \mkleeneopen{}\mforall{}d,k:\mBbbN{}.  \mforall{}i:\mBbbN{}k  +  1.
                                (((k  -  i)  \mleq{}  d)
                                {}\mRightarrow{}  (map(f;[2  *  i,  2  *  k))  \msim{}  shuffle(map(\mlambda{}i.<f  (2  *  i),  f  ((2  *  i)  +  1)>[i,  k)))))\mkleeneclose{}\mcdot{}
  THEN  Try  (((InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  RWO  "-1<"  0  THEN  Auto'))
  THEN  Thin  (-1)
  THEN  InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `from-upto`  0
  THEN  AutoSplit
  THEN  Unfold  `shuffle`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index