---

Step * of Lemma insert-combine-sorted-by

∀T:Type. ∀cmp:comparison(T).
  ((∀u,x,z:T.  (0 < cmp x u ⇒ 0 < cmp u z ⇒ 0 < cmp x z))
  ⇒ (∀f:T ⟶ T ⟶ T
        ((∀u,x:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ)))
        ⇒ (∀L:T List. ∀x:T.  (sorted-by(λx,y. 0 < cmp x y;L) ⇒ sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;L)))\000C))))
BY
{ InductionOnList }

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. f : T ⟶ T ⟶ T
5. ∀u,x:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ))
⊢ ∀x:T. (sorted-by(λx,y. 0 < cmp x y;[]) ⇒ sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;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. f : T ⟶ T ⟶ T
5. ∀u,x:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ))
6. u : T
7. v : T List
8. ∀x:T. (sorted-by(λx,y. 0 < cmp x y;v) ⇒ sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;v)))
⊢ ∀x:T. (sorted-by(λx,y. 0 < cmp x y;[u / v]) ⇒ sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;[u / v])))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}cmp:comparison(T).
    ((\mforall{}u,x,z:T.    (0  <  cmp  x  u  {}\mRightarrow{}  0  <  cmp  u  z  {}\mRightarrow{}  0  <  cmp  x  z))
    {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
                ((\mforall{}u,x:T.    (((cmp  x  u)  =  0)  {}\mRightarrow{}  ((cmp  u  (f  x  u))  =  0)))
                {}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}x:T.
                            (sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;L)  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;insert-combine(cmp;f;x;\000CL)))))))


By

---

Latex:
InductionOnList

---

Home Index