---

Step * 2 3 1 of Lemma insert-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. 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)))
9. x : T
10. ¬0 < cmp x u
11. cmp x u ≠ 0
12. sorted-by(λx,y. 0 < cmp x y;v)
13. ∀z:T. ((z ∈ v) ⇒ 0 < cmp u z)
14. sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;v))
15. 0 < cmp u x
16. z : T
17. (z ∈ insert-combine(cmp;f;x;v))
18. (z ∈ v) ∨ (z = x ∈ T) ∨ (∃y∈v. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T))
⊢ 0 < cmp u z
BY
{ SplitOrHyps }

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 ∈ ℤ))
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)))
9. x : T
10. ¬0 < cmp x u
11. cmp x u ≠ 0
12. sorted-by(λx,y. 0 < cmp x y;v)
13. ∀z:T. ((z ∈ v) ⇒ 0 < cmp u z)
14. sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;v))
15. 0 < cmp u x
16. z : T
17. (z ∈ insert-combine(cmp;f;x;v))
18. (z ∈ v)
⊢ 0 < cmp u 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. 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)))
9. x : T
10. ¬0 < cmp x u
11. cmp x u ≠ 0
12. sorted-by(λx,y. 0 < cmp x y;v)
13. ∀z:T. ((z ∈ v) ⇒ 0 < cmp u z)
14. sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;v))
15. 0 < cmp u x
16. z : T
17. (z ∈ insert-combine(cmp;f;x;v))
18. z = x ∈ T
⊢ 0 < cmp u z

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. 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)))
9. x : T
10. ¬0 < cmp x u
11. cmp x u ≠ 0
12. sorted-by(λx,y. 0 < cmp x y;v)
13. ∀z:T. ((z ∈ v) ⇒ 0 < cmp u z)
14. sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;v))
15. 0 < cmp u x
16. z : T
17. (z ∈ insert-combine(cmp;f;x;v))
18. (∃y∈v. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T))
⊢ 0 < cmp u z

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  \mforall{}u,x,z:T.    (0  <  cmp  x  u  {}\mRightarrow{}  0  <  cmp  u  z  {}\mRightarrow{}  0  <  cmp  x  z)
4.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
5.  \mforall{}u,x:T.    (((cmp  x  u)  =  0)  {}\mRightarrow{}  ((cmp  u  (f  x  u))  =  0))
6.  u  :  T
7.  v  :  T  List
8.  \mforall{}x:T.  (sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;v)  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;insert-combine(cmp;f;x;v)))
9.  x  :  T
10.  \mneg{}0  <  cmp  x  u
11.  cmp  x  u  \mneq{}  0
12.  sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;v)
13.  \mforall{}z:T.  ((z  \mmember{}  v)  {}\mRightarrow{}  0  <  cmp  u  z)
14.  sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;insert-combine(cmp;f;x;v))
15.  0  <  cmp  u  x
16.  z  :  T
17.  (z  \mmember{}  insert-combine(cmp;f;x;v))
18.  (z  \mmember{}  v)  \mvee{}  (z  =  x)  \mvee{}  (\mexists{}y\mmember{}v.  ((cmp  x  y)  =  0)  \mwedge{}  (z  =  (f  x  y)))
\mvdash{}  0  <  cmp  u  z


By

---

Latex:
SplitOrHyps

---

Home Index