---

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


1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. u : Point(l)
4. u1 : Point(l)
5. ¬(u1 = u ∈ Point(l))
6. v : Point(l) List
7. (u ∈ v)
8. ∀u:Point(l). ∀v:Point(l) List.
     (u ∨ reduce(λx,y. x ∨ y;0;v) = u ∨ reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v)) ∈ Point(l))
9. reduce(λx,y. x ∨ y;0;v) = u ∨ reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
⊢ u1 ∨ u ∨ reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v)) = u ∨ u1 ∨ reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v)) ∈ \000CPoint(l)
BY
{ ((GenConclTerm ⌜reduce(λx,y. x ∨ y;0;filter(λx.(¬b(eq x u));v))⌝⋅ THENA Auto) THEN All Thin) }

1
1. l : BoundedLattice
2. u : Point(l)
3. u1 : Point(l)
4. v1 : Point(l)
⊢ u1 ∨ u ∨ v1 = u ∨ u1 ∨ v1 ∈ Point(l)

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  eq  :  EqDecider(Point(l))
3.  u  :  Point(l)
4.  u1  :  Point(l)
5.  \mneg{}(u1  =  u)
6.  v  :  Point(l)  List
7.  (u  \mmember{}  v)
8.  \mforall{}u:Point(l).  \mforall{}v:Point(l)  List.
          (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)))
9.  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))
\mvdash{}  u1  \mvee{}  u  \mvee{}  reduce(\mlambda{}x,y.  x  \mvee{}  y;0;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))
=  u  \mvee{}  u1  \mvee{}  reduce(\mlambda{}x,y.  x  \mvee{}  y;0;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}reduce(\mlambda{}x,y.  x  \mvee{}  y;0;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index