---

Step * of Lemma select-shuffle2

∀[T:Type]. ∀[ps:(T × T) List].
  ∀i:ℕ||ps||. ((shuffle(ps)[2 * i] ~ fst(ps[i])) ∧ (shuffle(ps)[(2 * i) + 1] ~ snd(ps[i])))
BY
{ (Auto THEN RWO "select-shuffle" 0 THEN Auto' THEN Try ((RWO "length-shuffle" 0 THEN Auto THEN Auto')⋅)) }

1
1. T : Type
2. ps : (T × T) List
3. i : ℕ||ps||
⊢ if (2 * i rem 2 =z 0) then fst(ps[(2 * i) ÷ 2]) else snd(ps[(2 * i) ÷ 2]) fi  ~ fst(ps[i])

2
1. T : Type
2. ps : (T × T) List
3. i : ℕ||ps||
4. shuffle(ps)[2 * i] ~ fst(ps[i])
⊢ if ((2 * i) + 1 rem 2 =z 0) then fst(ps[((2 * i) + 1) ÷ 2]) else snd(ps[((2 * i) + 1) ÷ 2]) fi  ~ snd(ps[i])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ps:(T  \mtimes{}  T)  List].
    \mforall{}i:\mBbbN{}||ps||.  ((shuffle(ps)[2  *  i]  \msim{}  fst(ps[i]))  \mwedge{}  (shuffle(ps)[(2  *  i)  +  1]  \msim{}  snd(ps[i])))


By

---

Latex:
(Auto
  THEN  RWO  "select-shuffle"  0
  THEN  Auto'
  THEN  Try  ((RWO  "length-shuffle"  0  THEN  Auto  THEN  Auto')\mcdot{}))

---

Home Index