---

Step * 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)))
⊢ ∀x:T. (sorted-by(λx,y. (0 ≤ (cmp x y));[]) ⇒ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x;[])))
BY
{ (RepUR ``sorted-by insert-no-combine`` 0 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)))
\mvdash{}  \mforall{}x:T
        (sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));[])  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));insert-no-combine(cmp;x;\000C[])))


By

---

Latex:
(RepUR  ``sorted-by  insert-no-combine``  0  THEN  Auto)

---

Home Index