Step * 2 1 1 1 of Lemma lattice-fset-join-union


1. BoundedLattice
2. eq EqDecider(Point(l))
3. s1 fset(Point(l))
4. Point(l)
5. ∀s2:fset(Point(l)). (\/(s1 ⋃ s2) \/(s1) ∨ \/(s2) ∈ Point(l))
6. ¬x ∈ s1
7. s2 fset(Point(l))
⊢ x ∨ \/(s1) ∨ \/(s2) x ∨ \/(s1) ∨ \/(s2) ∈ Point(l)
BY
((Assert l ∈ BoundedLattice BY Auto) THEN THEN RepeatFor (D 2) THEN Auto) }


Latex:


Latex:

1.  l  :  BoundedLattice
2.  eq  :  EqDecider(Point(l))
3.  s1  :  fset(Point(l))
4.  x  :  Point(l)
5.  \mforall{}s2:fset(Point(l)).  (\mbackslash{}/(s1  \mcup{}  s2)  =  \mbackslash{}/(s1)  \mvee{}  \mbackslash{}/(s2))
6.  \mneg{}x  \mmember{}  s1
7.  s2  :  fset(Point(l))
\mvdash{}  x  \mvee{}  \mbackslash{}/(s1)  \mvee{}  \mbackslash{}/(s2)  =  x  \mvee{}  \mbackslash{}/(s1)  \mvee{}  \mbackslash{}/(s2)


By


Latex:
((Assert  l  \mmember{}  BoundedLattice  BY  Auto)  THEN  D  1  THEN  RepeatFor  2  (D  2)  THEN  Auto)




Home Index