---

Step * 2 of Lemma select-shuffle2


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])
BY
{ (((InstLemma `rem_invariant` [⌜1⌝;⌜i⌝;⌜2⌝]⋅ THENA Auto) THEN Reduce (-1)) THEN AutoSplit) }

1
1. T : Type
2. ps : (T × T) List
3. i : ℕ||ps||
4. shuffle(ps)[2 * i] ~ fst(ps[i])
5. (1 + (i * 2) rem 2) = 1 ∈ ℤ
6. ((2 * i) + 1 rem 2) = 0 ∈ ℤ
⊢ fst(ps[((2 * i) + 1) ÷ 2]) ~ snd(ps[i])

---

Latex:

---

Latex:

1.  T  :  Type
2.  ps  :  (T  \mtimes{}  T)  List
3.  i  :  \mBbbN{}||ps||
4.  shuffle(ps)[2  *  i]  \msim{}  fst(ps[i])
\mvdash{}  if  ((2  *  i)  +  1  rem  2  =\msubz{}  0)  then  fst(ps[((2  *  i)  +  1)  \mdiv{}  2])  else  snd(ps[((2  *  i)  +  1)  \mdiv{}  2])  fi   
\msim{}  snd(ps[i])


By

---

Latex:
(((InstLemma  `rem\_invariant`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))  THEN  AutoSplit)

---

Home Index