---

Step * 2 3 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. ¬(0 ≤ (cmp x u))
9. sorted-by(λx,y. (0 ≤ (cmp x y));v)
10. ∀z:T. ((z ∈ v) ⇒ (0 ≤ (cmp u z)))
11. z : T
12. (z ∈ insert-no-combine(cmp;x;v))
13. z = x ∈ T
⊢ 0 ≤ (cmp u z)
BY
{ (HypSubst (-1) 0 THEN D 2 THEN Unhide THEN Auto THEN RWO "3" 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)))
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.  \mneg{}(0  \mleq{}  (cmp  x  u))
9.  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));v)
10.  \mforall{}z:T.  ((z  \mmember{}  v)  {}\mRightarrow{}  (0  \mleq{}  (cmp  u  z)))
11.  z  :  T
12.  (z  \mmember{}  insert-no-combine(cmp;x;v))
13.  z  =  x
\mvdash{}  0  \mleq{}  (cmp  u  z)


By

---

Latex:
(HypSubst  (-1)  0  THEN  D  2  THEN  Unhide  THEN  Auto  THEN  RWO  "3"  0  THEN  Auto')\mcdot{}

---

Home Index