---

Step * 2 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 
⊢ if (i rem 2 =z 0) then fst([u / v][i ÷ 2]) else snd([u / v][i ÷ 2]) fi  ~ if (i - 2 rem 2 =z 0)
then fst(v[(i - 2) ÷ 2])
else snd(v[(i - 2) ÷ 2])
fi 
BY
{ EqCD }

1
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 
⊢ (i rem 2 =z 0) ~ (i - 2 rem 2 =z 0)

2
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 / v][i ÷ 2]) ~ fst(v[(i - 2) ÷ 2])

3
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 
⊢ snd([u / v][i ÷ 2]) ~ snd(v[(i - 2) ÷ 2])

---

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{}  if  (i  rem  2  =\msubz{}  0)  then  fst([u  /  v][i  \mdiv{}  2])  else  snd([u  /  v][i  \mdiv{}  2])  fi    \msim{}  if  (i  -  2  rem  2  =\msubz{}  0)
then  fst(v[(i  -  2)  \mdiv{}  2])
else  snd(v[(i  -  2)  \mdiv{}  2])
fi 


By

---

Latex:
EqCD

---

Home Index