---

Step * of Lemma select-shuffle

∀[T:Type]. ∀[ps:(T × T) List].
  ∀i:ℕ||shuffle(ps)||. (shuffle(ps)[i] ~ if (i rem 2 =z 0) then fst(ps[i ÷ 2]) else snd(ps[i ÷ 2]) fi )
BY
{ (InductionOnList
   THEN RepUR ``shuffle concat`` 0
   THEN Try (Complete (Auto))
   THEN Fold `concat` 0
   THEN Fold `shuffle` 0
   THEN Auto
   THEN (CaseNat 0 `i' THEN Reduce 0 THEN Try (Trivial))
   THEN CaseNat 1 `i'
   THEN Reduce 0
   THEN Try (Trivial)
   THEN (InstHyp [⌜i - 2⌝] (-4)⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN 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 
⊢ [fst(u); [snd(u) / shuffle(v)]][i] ~ shuffle(v)[i - 2]

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 
⊢ 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 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ps:(T  \mtimes{}  T)  List].
    \mforall{}i:\mBbbN{}||shuffle(ps)||
        (shuffle(ps)[i]  \msim{}  if  (i  rem  2  =\msubz{}  0)  then  fst(ps[i  \mdiv{}  2])  else  snd(ps[i  \mdiv{}  2])  fi  )


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``shuffle  concat``  0
  THEN  Try  (Complete  (Auto))
  THEN  Fold  `concat`  0
  THEN  Fold  `shuffle`  0
  THEN  Auto
  THEN  (CaseNat  0  `i'  THEN  Reduce  0  THEN  Try  (Trivial))
  THEN  CaseNat  1  `i'
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  (InstHyp  [\mkleeneopen{}i  -  2\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  NthHypSq  (-1)
  THEN  EqCD)

---

Home Index