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


1. Type
2. T ⟶ T ⟶ ℙ
3. cmp comparison(T)
4. T ⟶ T ⟶ T
5. T
6. ∀u,x,y:T.  (R[u;x]  R[x;y]  R[u;y])
7. ∀u,x,y:T.  (((cmp u) 0 ∈ ℤ R[x;y]  R[u;y])
8. ∀u,x,y:T.  (((cmp u) 0 ∈ ℤ R[x;y]  R[x;u])
9. ∀u,x:T.  (((cmp u) 0 ∈ ℤ ((cmp (f u)) 0 ∈ ℤ))
10. ∀x,y:T.  (0 < cmp  R[x;y])
11. T
12. List
13. (cmp 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. T
18. (y ∈ v)
19. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
⊢ R[f u;y]
BY
xxx(FHyp (-11) [-7] THENA Auto)xxx }

1
1. Type
2. T ⟶ T ⟶ ℙ
3. cmp comparison(T)
4. T ⟶ T ⟶ T
5. T
6. ∀u,x,y:T.  (R[u;x]  R[x;y]  R[u;y])
7. ∀u,x,y:T.  (((cmp u) 0 ∈ ℤ R[x;y]  R[u;y])
8. ∀u,x,y:T.  (((cmp u) 0 ∈ ℤ R[x;y]  R[x;u])
9. ∀u,x:T.  (((cmp u) 0 ∈ ℤ ((cmp (f u)) 0 ∈ ℤ))
10. ∀x,y:T.  (0 < cmp  R[x;y])
11. T
12. List
13. (cmp 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. T
18. (y ∈ v)
19. l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
20. (cmp (f u)) 0 ∈ ℤ
⊢ R[f 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.  (cmp  x  u)  =  0
14.  l-ordered(T;x,y.R[x;y];v)
15.  \mforall{}y:T.  ((y  \mmember{}  v)  {}\mRightarrow{}  R[u;y])
16.  l-ordered(T;x,y.R[x;y];v)
17.  y  :  T
18.  (y  \mmember{}  v)
19.  l-ordered(T;x,y.R[x;y];insert-combine(cmp;f;x;v))
\mvdash{}  R[f  x  u;y]


By


Latex:
xxx(FHyp  (-11)  [-7]  THENA  Auto)xxx




Home Index