---

Step * 1 1 1 of Lemma greatest-lower-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. greatest-lower-bound(T;x,y.R[x;y];a;y;u2)
12. greatest-lower-bound(T;x,y.R[x;y];b;c;y)
13. greatest-lower-bound(T;x,y.R[x;y];x;c;u1)
14. greatest-lower-bound(T;x,y.R[x;y];a;b;x)
⊢ R[u2;x]
BY
{ (Assert ⌜R[u2;a] ∧ R[u2;b]⌝⋅ 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. greatest-lower-bound(T;x,y.R[x;y];a;y;u2)
12. greatest-lower-bound(T;x,y.R[x;y];b;c;y)
13. greatest-lower-bound(T;x,y.R[x;y];x;c;u1)
14. greatest-lower-bound(T;x,y.R[x;y];a;b;x)
15. R[u2;a]
⊢ R[u2;b]

---

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.  greatest-lower-bound(T;x,y.R[x;y];a;y;u2)
12.  greatest-lower-bound(T;x,y.R[x;y];b;c;y)
13.  greatest-lower-bound(T;x,y.R[x;y];x;c;u1)
14.  greatest-lower-bound(T;x,y.R[x;y];a;b;x)
\mvdash{}  R[u2;x]


By

---

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

---

Home Index