---

Step * 1 of Lemma select-unshuffle


1. T : Type
2. n : ℕ
3. as : T List
4. ∀a1:T List. (||a1|| < ||as|| ⇒ (∀i:ℕ||unshuffle(a1)||. (unshuffle(a1)[i] = <a1[2 * i], a1[(2 * i) + 1]> ∈ (T × T))))
5. i : ℕ||unshuffle(as)||
⊢ unshuffle(as)[i] = <as[2 * i], as[(2 * i) + 1]> ∈ (T × T)
BY
{ (DVar `as'
   THEN Try (Complete ((RecUnfold `unshuffle` (-1) THEN Reduce (-1) THEN Auto)))
   THEN (DVar `v'
         THEN Try (Complete ((RecUnfold `unshuffle` (-1) THEN Reduce (-1) THEN Auto)))
         THEN RecUnfold `unshuffle` (-1)
         THEN (SplitOnHypITE -1  THENA Auto)
         THEN Auto
         THEN RecUnfold `unshuffle` 0
         THEN (SplitOnConclITE THENA Auto)
         THEN Auto
         THEN Reduce 0
         THEN InstHyp [⌜v⌝] (-4)⋅
         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 : ℕ||[<hd([u; [u1 / v]]), hd(tl([u; [u1 / v]]))> / unshuffle(tl(tl([u; [u1 / v]])))]||
8. ¬||[u; [u1 / v]]|| < 2
9. 2 ≤ ||[u; [u1 / v]]||
10. ∀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)

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  as  :  T  List
4.  \mforall{}a1:T  List
          (||a1||  <  ||as||  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||unshuffle(a1)||.  (unshuffle(a1)[i]  =  <a1[2  *  i],  a1[(2  *  i)  +  1]>)))
5.  i  :  \mBbbN{}||unshuffle(as)||
\mvdash{}  unshuffle(as)[i]  =  <as[2  *  i],  as[(2  *  i)  +  1]>


By

---

Latex:
(DVar  `as'
  THEN  Try  (Complete  ((RecUnfold  `unshuffle`  (-1)  THEN  Reduce  (-1)  THEN  Auto)))
  THEN  (DVar  `v'
              THEN  Try  (Complete  ((RecUnfold  `unshuffle`  (-1)  THEN  Reduce  (-1)  THEN  Auto)))
              THEN  RecUnfold  `unshuffle`  (-1)
              THEN  (SplitOnHypITE  -1    THENA  Auto)
              THEN  Auto
              THEN  RecUnfold  `unshuffle`  0
              THEN  (SplitOnConclITE  THENA  Auto)
              THEN  Auto
              THEN  Reduce  0
              THEN  InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-4)\mcdot{}
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index