---

Step * 2 1 2 1 1 1 1 2 of Lemma lattice-fset-meet_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 ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
⊢ u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
BY
{ (Subst' u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v))
   = u1 ∧ u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v))
   ∈ Point(l) 0
   THENA Auto
   ) }

1
.....equality..... 
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 ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
⊢ u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) = u1 ∧ u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ \000CPoint(l)

2
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 ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
⊢ u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;v) = u1 ∧ u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ 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  \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))
\mvdash{}  u  \mwedge{}  u1  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;v)  =  u  \mwedge{}  u1  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))


By

---

Latex:
(Subst'  u  \mwedge{}  u1  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))
  =  u1  \mwedge{}  u  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))  0
  THENA  Auto
  )

---

Home Index