---

Step * 1 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)
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)
BY
{ ((Assert ⌜\/(s1) ∧ \/(s2) = \/(f-union(eq;eq;s1;a.λb.a ∧ b"(s2))) ∈ Point(l)⌝⋅ THENM Eq)
   THEN ThinVar `s3'
   THEN ThinVar `s4'
   THEN ((GenConcl ⌜s1 = as ∈ (Point(l) List)⌝⋅ THENA Auto) THEN ThinVar `s1')
   THEN (GenConcl ⌜s2 = bs ∈ (Point(l) List)⌝⋅ THENA Auto)
   THEN ThinVar `s2') }

1
1. l : BoundedDistributiveLattice
2. eq : EqDecider(Point(l))
3. as : Point(l) List@i
4. bs : Point(l) List@i
⊢ \/(as) ∧ \/(bs) = \/(f-union(eq;eq;as;a.λb.a ∧ b"(bs))) ∈ 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)
15.  \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)))
\mvdash{}  \mbackslash{}/(s1)  \mwedge{}  \mbackslash{}/(s2)  =  \mbackslash{}/(f-union(eq;eq;s3;a.\mlambda{}b.a  \mwedge{}  b"(s4)))


By

---

Latex:
((Assert  \mkleeneopen{}\mbackslash{}/(s1)  \mwedge{}  \mbackslash{}/(s2)  =  \mbackslash{}/(f-union(eq;eq;s1;a.\mlambda{}b.a  \mwedge{}  b"(s2)))\mkleeneclose{}\mcdot{}  THENM  Eq)
  THEN  ThinVar  `s3'
  THEN  ThinVar  `s4'
  THEN  ((GenConcl  \mkleeneopen{}s1  =  as\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `s1')
  THEN  (GenConcl  \mkleeneopen{}s2  =  bs\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `s2')

---

Home Index