---

Step * 1 1 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|| < (||v|| + 1) + 1 ⇒ (∀i:ℕ||unshuffle(a1)||. (unshuffle(a1)[i] = <a1[2 * i], a1[(2 * i) + 1]> ∈ (T × T))))
7. i : ℤ
8. 0 ≤ i
9. i < ||unshuffle(v)|| + 1
10. ¬(||v|| + 1) + 1 < 2
11. 2 ≤ ((||v|| + 1) + 1)
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)
BY
{ Assert ⌜(2 * i) ≤ ||v||⌝⋅ }

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

2
1. T : Type
2. n : ℕ
3. u : T
4. u1 : T
5. v : T List
6. ∀a1:T List
     (||a1|| < (||v|| + 1) + 1 ⇒ (∀i:ℕ||unshuffle(a1)||. (unshuffle(a1)[i] = <a1[2 * i], a1[(2 * i) + 1]> ∈ (T × T))))
7. i : ℤ
8. 0 ≤ i
9. i < ||unshuffle(v)|| + 1
10. ¬(||v|| + 1) + 1 < 2
11. 2 ≤ ((||v|| + 1) + 1)
12. ∀i:ℕ||unshuffle(v)||. (unshuffle(v)[i] = <v[2 * i], v[(2 * i) + 1]> ∈ (T × T))
13. ¬(i = 0 ∈ ℤ)
14. (2 * i) ≤ ||v||
⊢ [<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||  <  (||v||  +  1)  +  1
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||unshuffle(a1)||.  (unshuffle(a1)[i]  =  <a1[2  *  i],  a1[(2  *  i)  +  1]>)))
7.  i  :  \mBbbZ{}
8.  0  \mleq{}  i
9.  i  <  ||unshuffle(v)||  +  1
10.  \mneg{}(||v||  +  1)  +  1  <  2
11.  2  \mleq{}  ((||v||  +  1)  +  1)
12.  \mforall{}i:\mBbbN{}||unshuffle(v)||.  (unshuffle(v)[i]  =  <v[2  *  i],  v[(2  *  i)  +  1]>)
13.  \mneg{}(i  =  0)
\mvdash{}  [<u,  u1>  /  unshuffle(v)][i]  =  <[u;  [u1  /  v]][2  *  i],  [u;  [u1  /  v]][(2  *  i)  +  1]>


By

---

Latex:
Assert  \mkleeneopen{}(2  *  i)  \mleq{}  ||v||\mkleeneclose{}\mcdot{}

---

Home Index