---

Step * 2 1 of Lemma insert-no-combine-sorted-by


1. [T] : Type
2. cmp : comparison(T)
3. ∀u,x,z:T.  ((0 ≤ (cmp x u)) ⇒ (0 ≤ (cmp u z)) ⇒ (0 ≤ (cmp x z)))
4. u : T
5. v : T List
6. ∀x:T. (sorted-by(λx,y. (0 ≤ (cmp x y));v) ⇒ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x;v)))
7. x : T
8. sorted-by(λx,y. (0 ≤ (cmp x y));[u / v])
9. 0 ≤ (cmp x u)
10. sorted-by(λx,y. (0 ≤ (cmp x y));[u / v])
⊢ (∀z∈[u / v].0 ≤ (cmp x z))
BY
{ (((BLemma `l_all_cons` THEN Auto) THEN Thin (-1))
   THEN (RWO "sorted-by-cons" (-1) THEN Auto)⋅
   THEN Reduce (-1)
   THEN RepeatFor 2 (ParallelOp (-1))
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  cmp  :  comparison(T)
3.  \mforall{}u,x,z:T.    ((0  \mleq{}  (cmp  x  u))  {}\mRightarrow{}  (0  \mleq{}  (cmp  u  z))  {}\mRightarrow{}  (0  \mleq{}  (cmp  x  z)))
4.  u  :  T
5.  v  :  T  List
6.  \mforall{}x:T.  (sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));v)  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));insert-no-combine(cm\000Cp;x;v)))
7.  x  :  T
8.  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));[u  /  v])
9.  0  \mleq{}  (cmp  x  u)
10.  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));[u  /  v])
\mvdash{}  (\mforall{}z\mmember{}[u  /  v].0  \mleq{}  (cmp  x  z))


By

---

Latex:
(((BLemma  `l\_all\_cons`  THEN  Auto)  THEN  Thin  (-1))
  THEN  (RWO  "sorted-by-cons"  (-1)  THEN  Auto)\mcdot{}
  THEN  Reduce  (-1)
  THEN  RepeatFor  2  (ParallelOp  (-1))
  THEN  Auto)

---

Home Index