---

Step * 2 1 2 1 1 1 1 1 of Lemma lattice-fset-meet_wf


1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. u : Point(l)
4. u1 : Point(l)
5. v : Point(l) List
6. u ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
7. u1 = u ∈ Point(l)
⊢ u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
BY
{ ((RWO  "-2< -1" 0 THEN Auto) THEN (GenConclTerm ⌜reduce(λx,y. x ∧ y;1;v)⌝⋅ THENA Auto) THEN All Thin) }

1
1. l : BoundedLattice
2. u : Point(l)
3. v1 : Point(l)
⊢ u ∧ u ∧ v1 = u ∧ v1 ∈ Point(l)

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  eq  :  EqDecider(Point(l))
3.  u  :  Point(l)
4.  u1  :  Point(l)
5.  v  :  Point(l)  List
6.  u  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;v)  =  u  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))
7.  u1  =  u
\mvdash{}  u  \mwedge{}  u1  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;v)  =  u  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))


By

---

Latex:
((RWO    "-2<  -1"  0  THEN  Auto)  THEN  (GenConclTerm  \mkleeneopen{}reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;v)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin\000C)

---

Home Index