---

Step * of Lemma lattice-meet-fset-join-distrib

∀[l:BoundedDistributiveLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].
  (\/(s1) ∧ \/(s2) = \/(f-union(eq;eq;s1;a.λb.a ∧ b"(s2))) ∈ Point(l))
BY
{ (Auto THEN QuotientElimForEquality (-2) THEN QuotientElimForEquality (-1)) }

1
1. l : BoundedDistributiveLattice
2. eq : EqDecider(Point(l))
3. s1 : Base
4. s3 : Base
5. s1 = s3 ∈ pertype(λx,y. ((x ∈ Point(l) List) ∧ (y ∈ Point(l) List) ∧ set-equal(Point(l);x;y)))
6. s1 ∈ Point(l) List
7. s3 ∈ Point(l) List
8. set-equal(Point(l);s1;s3)
9. s2 : Base
10. s4 : Base
11. s2 = s4 ∈ pertype(λx,y. ((x ∈ Point(l) List) ∧ (y ∈ Point(l) List) ∧ set-equal(Point(l);x;y)))
12. s2 ∈ Point(l) List
13. s4 ∈ Point(l) List
14. set-equal(Point(l);s2;s4)
⊢ \/(s1) ∧ \/(s2) = \/(f-union(eq;eq;s3;a.λb.a ∧ b"(s4))) ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[l:BoundedDistributiveLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s1,s2:fset(Point(l))].
    (\mbackslash{}/(s1)  \mwedge{}  \mbackslash{}/(s2)  =  \mbackslash{}/(f-union(eq;eq;s1;a.\mlambda{}b.a  \mwedge{}  b"(s2))))


By

---

Latex:
(Auto  THEN  QuotientElimForEquality  (-2)  THEN  QuotientElimForEquality  (-1))

---

Home Index