---

Step * of Lemma unshuffle-shuffle

∀[T:Type]. ∀[ps:(T × T) List].  (unshuffle(shuffle(ps)) ~ ps)
BY
{ (InductionOnList
   THEN Unfold `shuffle` 0
   THEN Reduce 0
   THEN RecUnfold `unshuffle` 0
   THEN Reduce 0
   THEN Try (Trivial)
   THEN (Unfold `concat` 0 THEN Reduce 0 THEN Fold `concat` 0 THEN Fold `shuffle` 0)
   THEN AutoSplit
   THEN Auto'
   THEN DVar `u'
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ps:(T  \mtimes{}  T)  List].    (unshuffle(shuffle(ps))  \msim{}  ps)


By

---

Latex:
(InductionOnList
  THEN  Unfold  `shuffle`  0
  THEN  Reduce  0
  THEN  RecUnfold  `unshuffle`  0
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  (Unfold  `concat`  0  THEN  Reduce  0  THEN  Fold  `concat`  0  THEN  Fold  `shuffle`  0)
  THEN  AutoSplit
  THEN  Auto'
  THEN  DVar  `u'
  THEN  Reduce  0
  THEN  Auto)

---

Home Index