Step
*
2
1
1
1
of Lemma
lattice-fset-join-union
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. s1 : fset(Point(l))
4. x : 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 D 1 THEN RepeatFor 2 (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