---

Step * 1 1 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)
⊢ R[x;u2]
BY
{ (Assert ⌜R[a;u2] ∧ R[b;u2]⌝⋅ THEN Auto) }

1
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)
15. R[a;u2]
⊢ R[b;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{}  R[x;u2]


By

---

Latex:
(Assert  \mkleeneopen{}R[a;u2]  \mwedge{}  R[b;u2]\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index