---

Step * of Lemma length-shuffle

∀[T:Type]. ∀[ps:(T × T) List].  (||shuffle(ps)|| ~ 2 * ||ps||)
BY
{ (InductionOnList
   THEN RepUR
   ``shuffle concat`` 0⋅
   THEN Try (Trivial)
   THEN Fold `concat` 0
   THEN Fold `shuffle` 0
   THEN HypSubst' -1 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  RepUR
  ``shuffle  concat``  0\mcdot{}
  THEN  Try  (Trivial)
  THEN  Fold  `concat`  0
  THEN  Fold  `shuffle`  0
  THEN  HypSubst'  -1  0
  THEN  Auto)

---

Home Index