---

Step * of Lemma mk-general-bounded-dist-lattice_wf

∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[E:T ⟶ T ⟶ ℙ].
  mk-general-bounded-dist-lattice(T;m;j;z;o;E) ∈ GeneralBoundedDistributiveLattice 
  supposing EquivRel(T;x,y.E x y)
  ∧ (∀[a,b:T].  (E m[a;b] m[b;a]))
  ∧ (∀[a,b:T].  (E j[a;b] j[b;a]))
  ∧ (∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c]))
  ∧ (∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c]))
  ∧ (∀[a,b:T].  (E j[a;m[a;b]] a))
  ∧ (∀[a,b:T].  (E m[a;j[a;b]] a))
  ∧ (∀[a:T]. (E m[a;o] a))
  ∧ (∀[a:T]. (E j[a;z] a))
  ∧ (∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]]))
BY
{ ((Auto
    THEN RepUR ``mk-general-bounded-dist-lattice general-bounded-distributive-lattice`` 0
    THEN RepUR ``mk-general-bounded-lattice general-bounded-lattice`` 0)
   THEN MemTypeCD
   ) }

1
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. z : T
5. o : T
6. E : T ⟶ T ⟶ ℙ
7. EquivRel(T;x,y.E x y)
8. ∀[a,b:T].  (E m[a;b] m[b;a])
9. ∀[a,b:T].  (E j[a;b] j[b;a])
10. ∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c])
11. ∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c])
12. ∀[a,b:T].  (E j[a;m[a;b]] a)
13. ∀[a,b:T].  (E m[a;j[a;b]] a)
14. ∀[a:T]. (E m[a;o] a)
15. ∀[a:T]. (E j[a;z] a)
16. ∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]])
⊢ λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E] ∈ GeneralBoundedLatticeStructure

2
.....set predicate..... 
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. z : T
5. o : T
6. E : T ⟶ T ⟶ ℙ
7. EquivRel(T;x,y.E x y)
8. ∀[a,b:T].  (E m[a;b] m[b;a])
9. ∀[a,b:T].  (E j[a;b] j[b;a])
10. ∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c])
11. ∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c])
12. ∀[a,b:T].  (E j[a;m[a;b]] a)
13. ∀[a,b:T].  (E m[a;j[a;b]] a)
14. ∀[a:T]. (E m[a;o] a)
15. ∀[a:T]. (E j[a;z] a)
16. ∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]])
⊢ general-lattice-axioms(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E])
∧ (∀[a,b,c:Point(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E])].
     a ∧ b ∨ c ≡ a ∧ b ∨ a ∧ c)

3
.....wf..... 
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. z : T
5. o : T
6. E : T ⟶ T ⟶ ℙ
7. EquivRel(T;x,y.E x y)
8. ∀[a,b:T].  (E m[a;b] m[b;a])
9. ∀[a,b:T].  (E j[a;b] j[b;a])
10. ∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c])
11. ∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c])
12. ∀[a,b:T].  (E j[a;m[a;b]] a)
13. ∀[a,b:T].  (E m[a;j[a;b]] a)
14. ∀[a:T]. (E m[a;o] a)
15. ∀[a:T]. (E j[a;z] a)
16. ∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]])
17. l : GeneralBoundedLatticeStructure
⊢ general-lattice-axioms(l) ∧ (∀[a,b,c:Point(l)].  a ∧ b ∨ c ≡ a ∧ b ∨ a ∧ c) ∈ Type

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m,j:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[z,o:T].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    mk-general-bounded-dist-lattice(T;m;j;z;o;E)  \mmember{}  GeneralBoundedDistributiveLattice 
    supposing  EquivRel(T;x,y.E  x  y)
    \mwedge{}  (\mforall{}[a,b:T].    (E  m[a;b]  m[b;a]))
    \mwedge{}  (\mforall{}[a,b:T].    (E  j[a;b]  j[b;a]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (E  m[a;m[b;c]]  m[m[a;b];c]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (E  j[a;j[b;c]]  j[j[a;b];c]))
    \mwedge{}  (\mforall{}[a,b:T].    (E  j[a;m[a;b]]  a))
    \mwedge{}  (\mforall{}[a,b:T].    (E  m[a;j[a;b]]  a))
    \mwedge{}  (\mforall{}[a:T].  (E  m[a;o]  a))
    \mwedge{}  (\mforall{}[a:T].  (E  j[a;z]  a))
    \mwedge{}  (\mforall{}[a,b,c:T].    (E  m[a;j[b;c]]  j[m[a;b];m[a;c]]))


By

---

Latex:
((Auto
    THEN  RepUR  ``mk-general-bounded-dist-lattice  general-bounded-distributive-lattice``  0
    THEN  RepUR  ``mk-general-bounded-lattice  general-bounded-lattice``  0)
  THEN  MemTypeCD
  )

---

Home Index