---

Step * 2 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)))
⊢ ∀x:T. (sorted-by(λx,y. (0 ≤ (cmp x y));[u / v]) ⇒ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x;[u / v])))
BY
{ (Unfold `insert-no-combine` 0
   THEN Reduce 0
   THEN Try (Fold `insert-no-combine` 0)
   THEN Auto
   THEN AutoSplit
   THEN (RWO "sorted-by-cons" 0 THEN Auto THEN Reduce 0)⋅)⋅ }

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

2
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));[u / v])
⊢ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x;v))

3
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));[u / v])
10. sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x;v))
⊢ (∀z∈insert-no-combine(cmp;x;v).0 ≤ (cmp u z))

---

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)))
\mvdash{}  \mforall{}x:T
        (sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));[u  /  v])
        {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));insert-no-combine(cmp;x;[u  /  v])))


By

---

Latex:
(Unfold  `insert-no-combine`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `insert-no-combine`  0)
  THEN  Auto
  THEN  AutoSplit
  THEN  (RWO  "sorted-by-cons"  0  THEN  Auto  THEN  Reduce  0)\mcdot{})\mcdot{}

---

Home Index