---

Step * of Lemma mk-bounded-distributive-lattice_wf

∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T].
  {points=T;
   meet=m;
   join=j;
   0=z;
   1=o} ∈ BoundedDistributiveLattice 
  supposing (∀[a,b:T].  (m[a;b] = m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] = j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] = a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] = a ∈ T))
  ∧ (∀[a:T]. (m[a;o] = a ∈ T))
  ∧ (∀[a:T]. (j[a;z] = a ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;j[b;c]] = j[m[a;b];m[a;c]] ∈ T))
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``mk-bounded-lattice lattice-axioms bounded-lattice-axioms`` 0
   THEN RepUR ``lattice-meet lattice-join lattice-point lattice-0 lattice-1`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m,j:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[z,o:T].
    \{points=T;
      meet=m;
      join=j;
      0=z;
      1=o\}  \mmember{}  BoundedDistributiveLattice 
    supposing  (\mforall{}[a,b:T].    (m[a;b]  =  m[b;a]))
    \mwedge{}  (\mforall{}[a,b:T].    (j[a;b]  =  j[b;a]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (m[a;m[b;c]]  =  m[m[a;b];c]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (j[a;j[b;c]]  =  j[j[a;b];c]))
    \mwedge{}  (\mforall{}[a,b:T].    (j[a;m[a;b]]  =  a))
    \mwedge{}  (\mforall{}[a,b:T].    (m[a;j[a;b]]  =  a))
    \mwedge{}  (\mforall{}[a:T].  (m[a;o]  =  a))
    \mwedge{}  (\mforall{}[a:T].  (j[a;z]  =  a))
    \mwedge{}  (\mforall{}[a,b,c:T].    (m[a;j[b;c]]  =  j[m[a;b];m[a;c]]))


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``mk-bounded-lattice  lattice-axioms  bounded-lattice-axioms``  0
  THEN  RepUR  ``lattice-meet  lattice-join  lattice-point  lattice-0  lattice-1``  0
  THEN  Auto)

---

Home Index