---

Step * 1 of Lemma select-shuffle


1. T : Type
2. u : T × T
3. v : (T × T) List
4. ∀i:ℕ||shuffle(v)||. (shuffle(v)[i] ~ if (i rem 2 =z 0) then fst(v[i ÷ 2]) else snd(v[i ÷ 2]) fi )
5. i : ℕ(||shuffle(v)|| + 1) + 1
6. ¬(i = 0 ∈ ℤ)
7. ¬(i = 1 ∈ ℤ)
8. shuffle(v)[i - 2] ~ if (i - 2 rem 2 =z 0) then fst(v[(i - 2) ÷ 2]) else snd(v[(i - 2) ÷ 2]) fi 
⊢ [fst(u); [snd(u) / shuffle(v)]][i] ~ shuffle(v)[i - 2]
BY
{ ((RWW "select-cons" 0 THENA Auto) THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T  \mtimes{}  T
3.  v  :  (T  \mtimes{}  T)  List
4.  \mforall{}i:\mBbbN{}||shuffle(v)||.  (shuffle(v)[i]  \msim{}  if  (i  rem  2  =\msubz{}  0)  then  fst(v[i  \mdiv{}  2])  else  snd(v[i  \mdiv{}  2])  fi  )
5.  i  :  \mBbbN{}(||shuffle(v)||  +  1)  +  1
6.  \mneg{}(i  =  0)
7.  \mneg{}(i  =  1)
8.  shuffle(v)[i  -  2]  \msim{}  if  (i  -  2  rem  2  =\msubz{}  0)  then  fst(v[(i  -  2)  \mdiv{}  2])  else  snd(v[(i  -  2)  \mdiv{}  2])  fi 
\mvdash{}  [fst(u);  [snd(u)  /  shuffle(v)]][i]  \msim{}  shuffle(v)[i  -  2]


By

---

Latex:
((RWW  "select-cons"  0  THENA  Auto)  THEN  RepeatFor  2  (AutoSplit))

---

Home Index