---

Step * 1 1 1 of Lemma select-unshuffle


1. T : Type
2. n : ℕ
3. u : T
4. u1 : T
5. v : T List
6. ∀a1:T List
     (||a1|| < ||[u; [u1 / v]]||
     ⇒ (∀i:ℕ||unshuffle(a1)||. (unshuffle(a1)[i] = <a1[2 * i], a1[(2 * i) + 1]> ∈ (T × T))))
7. i : ℤ
8. 0 ≤ i < ||[<hd([u; [u1 / v]]), hd(tl([u; [u1 / v]]))> / unshuffle(tl(tl([u; [u1 / v]])))]||
9. ¬||[u; [u1 / v]]|| < 2
10. 2 ≤ ||[u; [u1 / v]]||
11. ∀i:ℕ||unshuffle(v)||. (unshuffle(v)[i] = <v[2 * i], v[(2 * i) + 1]> ∈ (T × T))
⊢ [<u, u1> / unshuffle(v)][i] = <[u; [u1 / v]][2 * i], [u; [u1 / v]][(2 * i) + 1]> ∈ (T × T)
BY
{ (CaseNat 0 `i' THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. n : ℕ
3. u : T
4. u1 : T
5. v : T List
6. ∀a1:T List
     (||a1|| < ||[u; [u1 / v]]||
     ⇒ (∀i:ℕ||unshuffle(a1)||. (unshuffle(a1)[i] = <a1[2 * i], a1[(2 * i) + 1]> ∈ (T × T))))
7. i : ℤ
8. 0 ≤ i
9. i < ||[<hd([u; [u1 / v]]), hd(tl([u; [u1 / v]]))> / unshuffle(tl(tl([u; [u1 / v]])))]||
10. ¬||[u; [u1 / v]]|| < 2
11. 2 ≤ ||[u; [u1 / v]]||
12. ∀i:ℕ||unshuffle(v)||. (unshuffle(v)[i] = <v[2 * i], v[(2 * i) + 1]> ∈ (T × T))
13. ¬(i = 0 ∈ ℤ)
⊢ [<u, u1> / unshuffle(v)][i] = <[u; [u1 / v]][2 * i], [u; [u1 / v]][(2 * i) + 1]> ∈ (T × T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  u  :  T
4.  u1  :  T
5.  v  :  T  List
6.  \mforall{}a1:T  List
          (||a1||  <  ||[u;  [u1  /  v]]||
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||unshuffle(a1)||.  (unshuffle(a1)[i]  =  <a1[2  *  i],  a1[(2  *  i)  +  1]>)))
7.  i  :  \mBbbZ{}
8.  0  \mleq{}  i  <  ||[<hd([u;  [u1  /  v]]),  hd(tl([u;  [u1  /  v]]))>  /  unshuffle(tl(tl([u;  [u1  /  v]])))]||
9.  \mneg{}||[u;  [u1  /  v]]||  <  2
10.  2  \mleq{}  ||[u;  [u1  /  v]]||
11.  \mforall{}i:\mBbbN{}||unshuffle(v)||.  (unshuffle(v)[i]  =  <v[2  *  i],  v[(2  *  i)  +  1]>)
\mvdash{}  [<u,  u1>  /  unshuffle(v)][i]  =  <[u;  [u1  /  v]][2  *  i],  [u;  [u1  /  v]][(2  *  i)  +  1]>


By

---

Latex:
(CaseNat  0  `i'  THEN  Reduce  0  THEN  Auto)

---

Home Index