---

Step * 2 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)))
⊢ ∀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])))
BY
{ (Unfold `insert-combine` 0
   THEN Reduce 0
   THEN Try (Fold `insert-combine` 0)
   THEN Auto
   THEN ((CallByValueReduce 0 THENA Auto) THEN Repeat (AutoSplit))
   THEN (RWO "sorted-by-cons" 0 THEN Auto THEN (All (RWO "sorted-by-cons")) THEN Auto THEN All Reduce)⋅)⋅ }

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. sorted-by(λx,y. 0 < cmp x y;v)
11. (∀z∈v.0 < cmp u z)
12. (cmp x u) = 0 ∈ ℤ
13. sorted-by(λx,y. 0 < cmp x y;v)
⊢ (∀z∈v.0 < cmp (f x 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. cmp x u ≠ 0
11. sorted-by(λx,y. 0 < cmp x y;v)
12. (∀z∈v.0 < cmp u z)
13. 0 < cmp x u
14. sorted-by(λx,y. 0 < cmp x y;v)
15. (∀z∈v.0 < cmp u z)
⊢ (∀z∈[u / v].0 < cmp x 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∈v.0 < cmp u z)
14. sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;v))
⊢ (∀z∈insert-combine(cmp;f;x;v).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)))
\mvdash{}  \mforall{}x:T
        (sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;[u  /  v])  {}\mRightarrow{}  sorted-by(\mlambda{}x,y.  0  <  cmp  x  y;insert-combine(cmp;f;x;[u  /\000C  v])))


By

---

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

---

Home Index