---

Step * 1 1 of Lemma quotient-dl_wf

.....subterm..... T:t
1:n
1. l : BoundedDistributiveLattice
2. eq : Point(l) ⟶ Point(l) ⟶ ℙ
3. EquivRel(Point(l);x,y.eq[x;y])
4. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])
5. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])
6. l."meet" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
7. l."join" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
⊢ x,y:Point(l)//eq[x;y] ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  l  :  BoundedDistributiveLattice
2.  eq  :  Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(Point(l);x,y.eq[x;y])
4.  \mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mwedge{}  b;c  \mwedge{}  d])
5.  \mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mvee{}  b;c  \mvee{}  d])
6.  l."meet"  \mmember{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])
7.  l."join"  \mmember{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])
\mvdash{}  x,y:Point(l)//eq[x;y]  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index