---

Step * 2 of Lemma l-ordered-insert-combine


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]))
BY
{ (RW ListC 0
   THEN Try ((CallByValueReduce 0 THENA ProveHasValue))
   THEN Try (Complete (Auto))
   THEN Repeat (AutoSplit)
   THEN RW ListC 0
   THEN Auto) }

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])
11. u : T
12. v : T List
13. (cmp x u) = 0 ∈ ℤ
14. l-ordered(T;x,y.R[x;y];v)
15. ∀y:T. ((y ∈ v) ⇒ R[u;y])
16. l-ordered(T;x,y.R[x;y];v)
17. y : T
18. (y ∈ v)
19. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
⊢ R[f x u;y]

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. cmp x u ≠ 0
13. v : T List
14. 0 < cmp x u
15. l-ordered(T;x,y.R[x;y];v)
16. ∀y:T. ((y ∈ v) ⇒ R[u;y])
17. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
⊢ l-ordered(T;x,y.R[x;y];[u / v])

3
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. cmp x u ≠ 0
13. v : T List
14. 0 < cmp x u
15. l-ordered(T;x,y.R[x;y];v)
16. ∀y:T. ((y ∈ v) ⇒ R[u;y])
17. l-ordered(T;x,y.R[x;y];[u / v])
18. y : T
19. (y ∈ [u / v])
20. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
⊢ R[x;y]

4
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. ¬0 < cmp x u
13. cmp x u ≠ 0
14. v : T List
15. l-ordered(T;x,y.R[x;y];v)
16. ∀y:T. ((y ∈ v) ⇒ R[u;y])
17. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
18. y : T
19. (y ∈ insert-combine(cmp;f;x;v))
20. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
⊢ R[u;y]

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  cmp  :  comparison(T)
4.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
5.  x  :  T
6.  \mforall{}u,x,y:T.    (R[u;x]  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  R[u;y])
7.  \mforall{}u,x,y:T.    (((cmp  x  u)  =  0)  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  R[u;y])
8.  \mforall{}u,x,y:T.    (((cmp  y  u)  =  0)  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  R[x;u])
9.  \mforall{}u,x:T.    (((cmp  x  u)  =  0)  {}\mRightarrow{}  ((cmp  u  (f  x  u))  =  0))
10.  \mforall{}x,y:T.    (0  <  cmp  x  y  {}\mRightarrow{}  R[x;y])
11.  u  :  T
12.  v  :  T  List
13.  l-ordered(T;x,y.R[x;y];v)  {}\mRightarrow{}  l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
\mvdash{}  l-ordered(T;x,y.R[x;y];[u  /  v])  {}\mRightarrow{}  l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;[u  /  v]))


By

---

Latex:
(RW  ListC  0
  THEN  Try  ((CallByValueReduce  0  THENA  ProveHasValue))
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (AutoSplit)
  THEN  RW  ListC  0
  THEN  Auto)

---

Home Index