---

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

∀[T:Type]
  ∀cmp:comparison(T)
    ((∀u,x,z:T.  ((0 ≤ (cmp x u)) ⇒ (0 ≤ (cmp u z)) ⇒ (0 ≤ (cmp x z))))
    ⇒ (∀L:T List. ∀x:T.  (sorted-by(λx,y. (0 ≤ (cmp x y));L) ⇒ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x\000C;L)))))
BY
{ xxxInductionOnListxxx }

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)))
⊢ ∀x:T. (sorted-by(λx,y. (0 ≤ (cmp x y));[]) ⇒ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x;[])))

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)))
⊢ ∀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])))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}cmp:comparison(T)
        ((\mforall{}u,x,z:T.    ((0  \mleq{}  (cmp  x  u))  {}\mRightarrow{}  (0  \mleq{}  (cmp  u  z))  {}\mRightarrow{}  (0  \mleq{}  (cmp  x  z))))
        {}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}x:T.
                    (sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));L)
                    {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));insert-no-combine(cmp;x;L)))))


By

---

Latex:
xxxInductionOnListxxx

---

Home Index