Step
*
1
2
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])
⊢ (∀[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
{ (Assert (lattice-axioms(l) ∧ bounded-lattice-axioms(l))
∧ (∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))) BY
(D 1 THEN Unhide THEN Auto THEN RepUR ``lattice-axioms bounded-lattice-axioms`` 0 THEN Auto)) }
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. (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])))
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])
\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:
(Assert (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)) BY
(D 1 THEN Unhide THEN Auto THEN RepUR ``lattice-axioms bounded-lattice-axioms`` 0 THEN Auto))
Home
Index