---

Step * of Lemma mk-bounded-lattice_wf

∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T].
  mk-bounded-lattice(T;m;j;z;o) ∈ BoundedLattice 
  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))
BY
{ ((Auto THEN RepUR ``mk-bounded-lattice bdd-lattice`` 0) THEN MemTypeCD THEN Auto) }

1
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] ∈ BoundedLatticeStructure

2
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)
⊢ lattice-axioms(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o])

3
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)
14. lattice-axioms(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o])
⊢ bounded-lattice-axioms(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m,j:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[z,o:T].
    mk-bounded-lattice(T;m;j;z;o)  \mmember{}  BoundedLattice 
    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))


By

---

Latex:
((Auto  THEN  RepUR  ``mk-bounded-lattice  bdd-lattice``  0)  THEN  MemTypeCD  THEN  Auto)

---

Home Index