---

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


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)
BY
{ (Assert \/(f-union(eq;eq;s1;a.λb.a ∧ b"(s2))) = \/(f-union(eq;eq;s3;a.λb.a ∧ b"(s4))) ∈ Point(l) BY
         RepeatFor 3 ((EqCD THEN Auto))) }

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)
15. \/(f-union(eq;eq;s1;a.λb.a ∧ b"(s2))) = \/(f-union(eq;eq;s3;a.λb.a ∧ b"(s4))) ∈ Point(l)
⊢ \/(s1) ∧ \/(s2) = \/(f-union(eq;eq;s3;a.λb.a ∧ b"(s4))) ∈ Point(l)

---

Latex:

---

Latex:

1.  l  :  BoundedDistributiveLattice
2.  eq  :  EqDecider(Point(l))
3.  s1  :  Base
4.  s3  :  Base
5.  s1  =  s3
6.  s1  \mmember{}  Point(l)  List
7.  s3  \mmember{}  Point(l)  List
8.  set-equal(Point(l);s1;s3)
9.  s2  :  Base
10.  s4  :  Base
11.  s2  =  s4
12.  s2  \mmember{}  Point(l)  List
13.  s4  \mmember{}  Point(l)  List
14.  set-equal(Point(l);s2;s4)
\mvdash{}  \mbackslash{}/(s1)  \mwedge{}  \mbackslash{}/(s2)  =  \mbackslash{}/(f-union(eq;eq;s3;a.\mlambda{}b.a  \mwedge{}  b"(s4)))


By

---

Latex:
(Assert  \mbackslash{}/(f-union(eq;eq;s1;a.\mlambda{}b.a  \mwedge{}  b"(s2)))  =  \mbackslash{}/(f-union(eq;eq;s3;a.\mlambda{}b.a  \mwedge{}  b"(s4)))  BY
              RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index