---

Step * of Lemma l-ordered-insert-combine

∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x:T.
  ((∀u,x,y:T.  (R[u;x] ⇒ R[x;y] ⇒ R[u;y]))
  ⇒ (∀u,x,y:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ R[x;y] ⇒ R[u;y]))
  ⇒ (∀u,x,y:T.  (((cmp y u) = 0 ∈ ℤ) ⇒ R[x;y] ⇒ R[x;u]))
  ⇒ (∀u,x:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ)))
  ⇒ (∀x,y:T.  (0 < cmp x y ⇒ R[x;y]))
  ⇒ (∀L:T List. (l-ordered(T;x,y.R[x;y];L) ⇒ l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;L)))))
BY
{ InductionOnList }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. cmp : comparison(T)
4. f : T ⟶ T ⟶ T
5. x : T
6. ∀u,x,y:T.  (R[u;x] ⇒ R[x;y] ⇒ R[u;y])
7. ∀u,x,y:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ R[x;y] ⇒ R[u;y])
8. ∀u,x,y:T.  (((cmp y u) = 0 ∈ ℤ) ⇒ R[x;y] ⇒ R[x;u])
9. ∀u,x:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ))
10. ∀x,y:T.  (0 < cmp x y ⇒ R[x;y])
⊢ l-ordered(T;x,y.R[x;y];[]) ⇒ l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;[]))

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. cmp : comparison(T)
4. f : T ⟶ T ⟶ T
5. x : T
6. ∀u,x,y:T.  (R[u;x] ⇒ R[x;y] ⇒ R[u;y])
7. ∀u,x,y:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ R[x;y] ⇒ R[u;y])
8. ∀u,x,y:T.  (((cmp y u) = 0 ∈ ℤ) ⇒ R[x;y] ⇒ R[x;u])
9. ∀u,x:T.  (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ))
10. ∀x,y:T.  (0 < cmp x y ⇒ R[x;y])
11. u : T
12. v : T List
13. l-ordered(T;x,y.R[x;y];v) ⇒ l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
⊢ l-ordered(T;x,y.R[x;y];[u / v]) ⇒ l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;[u / v]))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}cmp:comparison(T).  \mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T.  \mforall{}x:T.
    ((\mforall{}u,x,y:T.    (R[u;x]  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  R[u;y]))
    {}\mRightarrow{}  (\mforall{}u,x,y:T.    (((cmp  x  u)  =  0)  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  R[u;y]))
    {}\mRightarrow{}  (\mforall{}u,x,y:T.    (((cmp  y  u)  =  0)  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  R[x;u]))
    {}\mRightarrow{}  (\mforall{}u,x:T.    (((cmp  x  u)  =  0)  {}\mRightarrow{}  ((cmp  u  (f  x  u))  =  0)))
    {}\mRightarrow{}  (\mforall{}x,y:T.    (0  <  cmp  x  y  {}\mRightarrow{}  R[x;y]))
    {}\mRightarrow{}  (\mforall{}L:T  List.  (l-ordered(T;x,y.R[x;y];L)  {}\mRightarrow{}  l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;L)))))


By

---

Latex:
InductionOnList

---

Home Index