Step
*
1
of Lemma
lattice-fset-join_wf
.....assertion.....
1. l : BoundedLattice
2. ∀x,y:Point(l). Dec(x = y ∈ Point(l))
3. s : fset(Point(l))
⊢ EqDecider(Point(l))
BY
{ EAuto 1 }
Latex:
Latex:
.....assertion.....
1. l : BoundedLattice
2. \mforall{}x,y:Point(l). Dec(x = y)
3. s : fset(Point(l))
\mvdash{} EqDecider(Point(l))
By
Latex:
EAuto 1
Home
Index