---

Step * 2 1 2 1 1 1 1 1 of Lemma lattice-fset-join_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;0;v) = u ∨ reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
7. u1 = u ∈ Point(l)
⊢ u ∨ u1 ∨ reduce(λx,y. x ∨ y;0;v) = u ∨ reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
BY
{ ((RWO  "-2< -1" 0 THEN Auto) THEN (GenConclTerm ⌜reduce(λx,y. x ∨ y;0;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  \mvee{}  reduce(\mlambda{}x,y.  x  \mvee{}  y;0;v)  =  u  \mvee{}  reduce(\mlambda{}x,y.  x  \mvee{}  y;0;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))
7.  u1  =  u
\mvdash{}  u  \mvee{}  u1  \mvee{}  reduce(\mlambda{}x,y.  x  \mvee{}  y;0;v)  =  u  \mvee{}  reduce(\mlambda{}x,y.  x  \mvee{}  y;0;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  \mvee{}  y;0;v)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin\000C)

---

Home Index