Step
*
1
2
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])
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])
8. (lattice-axioms(l) ∧ bounded-lattice-axioms(l)) ∧ (∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l)))
⊢ (∀[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])))
BY
{ (RepUR ``so_apply`` 0
THEN Folds ``lattice-meet lattice-join`` 0
THEN Folds ``lattice-0 lattice-1`` 0
THEN RepUR ``lattice-axioms bounded-lattice-axioms`` -1
THEN ExRepD) }
1
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])
8. ∀[a,b:Point(l)]. (a ∧ b = b ∧ a ∈ Point(l))
9. ∀[a,b:Point(l)]. (a ∨ b = b ∨ a ∈ Point(l))
10. ∀[a,b,c:Point(l)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
11. ∀[a,b,c:Point(l)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
12. ∀[a,b:Point(l)]. (a ∨ a ∧ b = a ∈ Point(l))
13. ∀[a,b:Point(l)]. (a ∧ a ∨ b = a ∈ Point(l))
14. ∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))
15. ∀[a:Point(l)]. (a ∧ 1 = a ∈ Point(l))
16. ∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))
⊢ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∧ b = b ∧ a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∨ b = b ∨ a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b,c:x,y:Point(l)//(eq x y)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b,c:x,y:Point(l)//(eq x y)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∨ a ∧ b = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∧ a ∨ b = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a:x,y:Point(l)//(eq x y)]. (a ∧ 1 = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a:x,y:Point(l)//(eq x y)]. (a ∨ 0 = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b,c:x,y:Point(l)//(eq x y)]. (a ∧ b ∨ c = a ∧ b ∨ 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])
6. 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])
7. 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])
8. (lattice-axioms(l) \mwedge{} bounded-lattice-axioms(l))
\mwedge{} (\mforall{}[a,b,c:Point(l)]. (a \mwedge{} b \mvee{} c = a \mwedge{} b \mvee{} a \mwedge{} c))
\mvdash{} (\mforall{}[a,b:x,y:Point(l)//eq[x;y]]. (l."meet"[a;b] = l."meet"[b;a]))
\mwedge{} (\mforall{}[a,b:x,y:Point(l)//eq[x;y]]. (l."join"[a;b] = l."join"[b;a]))
\mwedge{} (\mforall{}[a,b,c:x,y:Point(l)//eq[x;y]]. (l."meet"[a;l."meet"[b;c]] = l."meet"[l."meet"[a;b];c]))
\mwedge{} (\mforall{}[a,b,c:x,y:Point(l)//eq[x;y]]. (l."join"[a;l."join"[b;c]] = l."join"[l."join"[a;b];c]))
\mwedge{} (\mforall{}[a,b:x,y:Point(l)//eq[x;y]]. (l."join"[a;l."meet"[a;b]] = a))
\mwedge{} (\mforall{}[a,b:x,y:Point(l)//eq[x;y]]. (l."meet"[a;l."join"[a;b]] = a))
\mwedge{} (\mforall{}[a:x,y:Point(l)//eq[x;y]]. (l."meet"[a;l."1"] = a))
\mwedge{} (\mforall{}[a:x,y:Point(l)//eq[x;y]]. (l."join"[a;l."0"] = a))
\mwedge{} (\mforall{}[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]]))
By
Latex:
(RepUR ``so\_apply`` 0
THEN Folds ``lattice-meet lattice-join`` 0
THEN Folds ``lattice-0 lattice-1`` 0
THEN RepUR ``lattice-axioms bounded-lattice-axioms`` -1
THEN ExRepD)
Home
Index