---

Step * 1 1 of Lemma mk-bounded-lattice_wf


1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. z : T
5. o : T
6. ∀[a,b:T].  (m[a;b] = m[b;a] ∈ T)
7. ∀[a,b:T].  (j[a;b] = j[b;a] ∈ T)
8. ∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T)
9. ∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T)
10. ∀[a,b:T].  (j[a;m[a;b]] = a ∈ T)
11. ∀[a,b:T].  (m[a;j[a;b]] = a ∈ T)
12. ∀[a:T]. (m[a;o] = a ∈ T)
13. ∀[a:T]. (j[a;z] = a ∈ T)
⊢ λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o] ∈ "Point":Type
  "meet":self."Point" ⟶ self."Point" ⟶ self."Point"
  "join":self."Point" ⟶ self."Point" ⟶ self."Point"
  "1":self."Point"
  "0":self."Point"
BY
{ (RepeatFor 5 ((RecordPlusTypeCD THEN Reduce 0 THEN Try (Trivial))) THEN RepUR ``record record-update`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  j  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  z  :  T
5.  o  :  T
6.  \mforall{}[a,b:T].    (m[a;b]  =  m[b;a])
7.  \mforall{}[a,b:T].    (j[a;b]  =  j[b;a])
8.  \mforall{}[a,b,c:T].    (m[a;m[b;c]]  =  m[m[a;b];c])
9.  \mforall{}[a,b,c:T].    (j[a;j[b;c]]  =  j[j[a;b];c])
10.  \mforall{}[a,b:T].    (j[a;m[a;b]]  =  a)
11.  \mforall{}[a,b:T].    (m[a;j[a;b]]  =  a)
12.  \mforall{}[a:T].  (m[a;o]  =  a)
13.  \mforall{}[a:T].  (j[a;z]  =  a)
\mvdash{}  \mlambda{}x.x["Point"  :=  T]["meet"  :=  m]["join"  :=  j]["0"  :=  z]["1"  :=  o]  \mmember{}  "Point":Type
    "meet":self."Point"  {}\mrightarrow{}  self."Point"  {}\mrightarrow{}  self."Point"
    "join":self."Point"  {}\mrightarrow{}  self."Point"  {}\mrightarrow{}  self."Point"
    "1":self."Point"
    "0":self."Point"


By

---

Latex:
(RepeatFor  5  ((RecordPlusTypeCD  THEN  Reduce  0  THEN  Try  (Trivial)))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index