---

Step * 2 3 2 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 
9. (i ÷ 2) ≤ 0
⊢ u ~ v[(i ÷ 2) - 1]
BY
{ ((InstLemma `div_rem_sum` [⌜i⌝;⌜2⌝]⋅ THEN Auto') THEN InstLemma `rem_bounds_1` [⌜i⌝;⌜2⌝]⋅ THEN Auto')⋅ }

---

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 
9.  (i  \mdiv{}  2)  \mleq{}  0
\mvdash{}  u  \msim{}  v[(i  \mdiv{}  2)  -  1]


By

---

Latex:
((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto')
  THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
  THEN  Auto')\mcdot{}

---

Home Index