---

Step * 1 1 1 1 1 1 of Lemma select-unshuffle

.....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||
BY
{ ((RWO "length-unshuffle" (-5) THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜||v||⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜||v||⌝;⌜2⌝]⋅ THENA Auto)
   THEN Auto') }

---

Latex:

---

Latex:
.....assertion..... 
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{}  (2  *  i)  \mleq{}  ||v||


By

---

Latex:
((RWO  "length-unshuffle"  (-5)  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}||v||\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}||v||\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Auto')

---

Home Index