---

Step * 2 3 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 
⊢ snd([u / v][i ÷ 2]) ~ snd(v[(i - 2) ÷ 2])
BY
{ Subst ⌜(i - 2) ÷ 2 ~ (i ÷ 2) - 1⌝ 0⋅ }

1
.....equality..... 
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 - 2) ÷ 2 ~ (i ÷ 2) - 1

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

---

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{}  snd([u  /  v][i  \mdiv{}  2])  \msim{}  snd(v[(i  -  2)  \mdiv{}  2])


By

---

Latex:
Subst  \mkleeneopen{}(i  -  2)  \mdiv{}  2  \msim{}  (i  \mdiv{}  2)  -  1\mkleeneclose{}  0\mcdot{}

---

Home Index