---

Step * 1 of Lemma least-upper-bound-assoc


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Order(T;x,y.R[x;y])
4. a : T
5. b : T
6. c : T
7. x : T
8. y : T
9. u1 : T
10. u2 : T
11. least-upper-bound(T;x,y.R[x;y];a;y;u2)
12. least-upper-bound(T;x,y.R[x;y];b;c;y)
13. least-upper-bound(T;x,y.R[x;y];x;c;u1)
14. least-upper-bound(T;x,y.R[x;y];a;b;x)
⊢ u1 = u2 ∈ T
BY
{ (Assert ⌜least-upper-bound(T;x,y.R[x;y];x;c;u2)⌝⋅ THEN Auto) }

1
.....assertion..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Order(T;x,y.R[x;y])
4. a : T
5. b : T
6. c : T
7. x : T
8. y : T
9. u1 : T
10. u2 : T
11. least-upper-bound(T;x,y.R[x;y];a;y;u2)
12. least-upper-bound(T;x,y.R[x;y];b;c;y)
13. least-upper-bound(T;x,y.R[x;y];x;c;u1)
14. least-upper-bound(T;x,y.R[x;y];a;b;x)
⊢ least-upper-bound(T;x,y.R[x;y];x;c;u2)

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  Order(T;x,y.R[x;y])
4.  a  :  T
5.  b  :  T
6.  c  :  T
7.  x  :  T
8.  y  :  T
9.  u1  :  T
10.  u2  :  T
11.  least-upper-bound(T;x,y.R[x;y];a;y;u2)
12.  least-upper-bound(T;x,y.R[x;y];b;c;y)
13.  least-upper-bound(T;x,y.R[x;y];x;c;u1)
14.  least-upper-bound(T;x,y.R[x;y];a;b;x)
\mvdash{}  u1  =  u2


By

---

Latex:
(Assert  \mkleeneopen{}least-upper-bound(T;x,y.R[x;y];x;c;u2)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index