---

Step * 1 of Lemma unshuffle-iseg


1. [T] : Type
2. n : ℕ
3. as : T List
4. ∀a1:T List. (||a1|| < ||as|| ⇒ (∀bs:T List. (a1 ≤ bs ⇒ unshuffle(a1) ≤ unshuffle(bs))))
5. bs : T List
6. as ≤ bs
⊢ unshuffle(as) ≤ unshuffle(bs)
BY
{ (DVar `as'
   THEN Try ((RW (AddrC [2] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN BLemma `nil_iseg` THEN Auto))
   THEN DVar `bs'
   THEN Try (((RWO "iseg_nil" (-1) THENM Reduce (-1)) THEN Auto))
   THEN (RWO "cons_iseg" (-1) THENA Auto)
   THEN (DVar `v'
         THEN Try ((RW (AddrC [2] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN BLemma `nil_iseg` THEN Auto))
         THEN DVar `v1'
         THEN Try (((RWO "iseg_nil" (-1) THENM Reduce (-1)) THEN Auto))
         THEN (RWO "cons_iseg" (-1) THENA Auto))⋅) }

1
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]])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}
3.  as  :  T  List
4.  \mforall{}a1:T  List.  (||a1||  <  ||as||  {}\mRightarrow{}  (\mforall{}bs:T  List.  (a1  \mleq{}  bs  {}\mRightarrow{}  unshuffle(a1)  \mleq{}  unshuffle(bs))))
5.  bs  :  T  List
6.  as  \mleq{}  bs
\mvdash{}  unshuffle(as)  \mleq{}  unshuffle(bs)


By

---

Latex:
(DVar  `as'
  THEN  Try  ((RW  (AddrC  [2]  RecUnfoldTopAbC)  0  THEN  Reduce  0  THEN  BLemma  `nil\_iseg`  THEN  Auto))
  THEN  DVar  `bs'
  THEN  Try  (((RWO  "iseg\_nil"  (-1)  THENM  Reduce  (-1))  THEN  Auto))
  THEN  (RWO  "cons\_iseg"  (-1)  THENA  Auto)
  THEN  (DVar  `v'
              THEN  Try  ((RW  (AddrC  [2]  RecUnfoldTopAbC)  0  THEN  Reduce  0  THEN  BLemma  `nil\_iseg`  THEN  Auto))
              THEN  DVar  `v1'
              THEN  Try  (((RWO  "iseg\_nil"  (-1)  THENM  Reduce  (-1))  THEN  Auto))
              THEN  (RWO  "cons\_iseg"  (-1)  THENA  Auto))\mcdot{})

---

Home Index