---

Step * 1 of Lemma quotient-dl_wf


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])
⊢ l//x,y.eq[x;y] ∈ BoundedDistributiveLattice
BY
{ ((Assert l."meet" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) BY
          (RepeatFor 2 ((FunExt THENA Auto))
           THEN Fold `lattice-meet` 0
           THEN (newQuotientElim (-2) THENA Auto)
           THEN (newQuotientElim (-5) THENA Auto)
           THEN EqTypeCD
           THEN Auto))
   THEN (Assert l."join" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) BY
               (RepeatFor 2 ((FunExt THENA Auto))
                THEN Fold `lattice-join` 0
                THEN (newQuotientElim (-2) THENA Auto)
                THEN (newQuotientElim (-5) THENA Auto)
                THEN EqTypeCD
                THEN Auto))
   THEN Unfold `quotient-dl` 0
   THEN MemCD
   THEN Try (Trivial)
   THEN Try ((Folds ``lattice-1 lattice-0`` 0 THEN SubsumeC ⌜Point(l)⌝⋅ THEN Auto))) }

1
.....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

2
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])
⊢ (∀[a,b:x,y:Point(l)//eq[x;y]].  (l."meet"[a;b] = l."meet"[b;a] ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a,b:x,y:Point(l)//eq[x;y]].  (l."join"[a;b] = l."join"[b;a] ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a,b,c:x,y:Point(l)//eq[x;y]].  (l."meet"[a;l."meet"[b;c]] = l."meet"[l."meet"[a;b];c] ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a,b,c:x,y:Point(l)//eq[x;y]].  (l."join"[a;l."join"[b;c]] = l."join"[l."join"[a;b];c] ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a,b:x,y:Point(l)//eq[x;y]].  (l."join"[a;l."meet"[a;b]] = a ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a,b:x,y:Point(l)//eq[x;y]].  (l."meet"[a;l."join"[a;b]] = a ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a:x,y:Point(l)//eq[x;y]]. (l."meet"[a;l."1"] = a ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a:x,y:Point(l)//eq[x;y]]. (l."join"[a;l."0"] = a ∈ (x,y:Point(l)//eq[x;y])))
∧ (∀[a,b,c:x,y:Point(l)//eq[x;y]].
     (l."meet"[a;l."join"[b;c]] = l."join"[l."meet"[a;b];l."meet"[a;c]] ∈ (x,y:Point(l)//eq[x;y])))

---

Latex:

---

Latex:

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])
\mvdash{}  l//x,y.eq[x;y]  \mmember{}  BoundedDistributiveLattice


By

---

Latex:
((Assert  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])  BY
                (RepeatFor  2  ((FunExt  THENA  Auto))
                  THEN  Fold  `lattice-meet`  0
                  THEN  (newQuotientElim  (-2)  THENA  Auto)
                  THEN  (newQuotientElim  (-5)  THENA  Auto)
                  THEN  EqTypeCD
                  THEN  Auto))
  THEN  (Assert  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])  BY
                          (RepeatFor  2  ((FunExt  THENA  Auto))
                            THEN  Fold  `lattice-join`  0
                            THEN  (newQuotientElim  (-2)  THENA  Auto)
                            THEN  (newQuotientElim  (-5)  THENA  Auto)
                            THEN  EqTypeCD
                            THEN  Auto))
  THEN  Unfold  `quotient-dl`  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Try  ((Folds  ``lattice-1  lattice-0``  0  THEN  SubsumeC  \mkleeneopen{}Point(l)\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index