---

Step * of Lemma select-unshuffle

∀[T:Type]. ∀as:T List. ∀i:ℕ||unshuffle(as)||.  (unshuffle(as)[i] = <as[2 * i], as[(2 * i) + 1]> ∈ (T × T))
BY
{ TACTIC:(TACTIC:TACTIC:InductionOnLength THEN Auto) }

1
1. T : Type
2. n : ℕ
3. as : T List
4. ∀a1:T List. (||a1|| < ||as|| ⇒ (∀i:ℕ||unshuffle(a1)||. (unshuffle(a1)[i] = <a1[2 * i], a1[(2 * i) + 1]> ∈ (T × T))))
5. i : ℕ||unshuffle(as)||
⊢ unshuffle(as)[i] = <as[2 * i], as[(2 * i) + 1]> ∈ (T × T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as:T  List.  \mforall{}i:\mBbbN{}||unshuffle(as)||.    (unshuffle(as)[i]  =  <as[2  *  i],  as[(2  *  i)  +  1]>)


By

---

Latex:
TACTIC:(TACTIC:TACTIC:InductionOnLength  THEN  Auto)

---

Home Index