---

Step * 1 1 of Lemma unshuffle-iseg


1. [T] : Type
2. n : ℕ
3. u : T
4. u2 : T
5. v : T List
6. ∀a1:T List. (||a1|| < ||[u; [u2 / v]]|| ⇒ (∀bs:T List. (a1 ≤ bs ⇒ unshuffle(a1) ≤ unshuffle(bs))))
7. u1 : T
8. u3 : T
9. v2 : T List
10. (u = u1 ∈ T) ∧ (u2 = u3 ∈ T) ∧ v ≤ v2
⊢ unshuffle([u; [u2 / v]]) ≤ unshuffle([u1; [u3 / v2]])
BY
{ (RecUnfold `unshuffle` 0
   THEN Reduce 0
   THEN RepeatFor 2 ((AutoSplit THEN Auto'))
   THEN BLemma `cons_iseg`
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto') }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}
3.  u  :  T
4.  u2  :  T
5.  v  :  T  List
6.  \mforall{}a1:T  List
          (||a1||  <  ||[u;  [u2  /  v]]||  {}\mRightarrow{}  (\mforall{}bs:T  List.  (a1  \mleq{}  bs  {}\mRightarrow{}  unshuffle(a1)  \mleq{}  unshuffle(bs))))
7.  u1  :  T
8.  u3  :  T
9.  v2  :  T  List
10.  (u  =  u1)  \mwedge{}  (u2  =  u3)  \mwedge{}  v  \mleq{}  v2
\mvdash{}  unshuffle([u;  [u2  /  v]])  \mleq{}  unshuffle([u1;  [u3  /  v2]])


By

---

Latex:
(RecUnfold  `unshuffle`  0
  THEN  Reduce  0
  THEN  RepeatFor  2  ((AutoSplit  THEN  Auto'))
  THEN  BLemma  `cons\_iseg`
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto')

---

Home Index