---

Step * of Lemma length-unshuffle

∀[T:Type]. ∀[L:T List].  (||unshuffle(L)|| ~ ||L|| ÷ 2)
BY
{ (InductionOnLength
   THEN RecUnfold `unshuffle` 0
   THEN Auto
   THEN OldAutoSplit
   THEN RWW "-2" 0
   THEN Auto
   THEN (DVar `L' THEN All Reduce THEN Auto)
   THEN DVar `v'
   THEN All Reduce
   THEN Auto'
   THEN (GenConcl ⌜||v|| = m ∈ ℕ⌝⋅ THEN Auto)
   THEN All Thin) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    (||unshuffle(L)||  \msim{}  ||L||  \mdiv{}  2)


By

---

Latex:
(InductionOnLength
  THEN  RecUnfold  `unshuffle`  0
  THEN  Auto
  THEN  OldAutoSplit
  THEN  RWW  "-2"  0
  THEN  Auto
  THEN  (DVar  `L'  THEN  All  Reduce  THEN  Auto)
  THEN  DVar  `v'
  THEN  All  Reduce
  THEN  Auto'
  THEN  (GenConcl  \mkleeneopen{}||v||  =  m\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  All  Thin)

---

Home Index