---

Step * 2 1 2 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. v : Point(l) List
6. (u ∈ v) ⇒ (reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l))
7. (u ∈ [u1 / v])
8. ∀u:Point(l). ∀v:Point(l) List.
     (u ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l))
⊢ u1 ∧ reduce(λx,y. x ∧ y;1;v)
= u ∧ reduce(λx,y. x ∧ y;1;if ¬b(eq u1 u) then [u1 / filter(λx.(¬b(eq x u));v)] else filter(λx.(¬b(eq x u));v) fi )
∈ Point(l)
BY
{ ((RWO "cons_member" (-2) THENA Auto) THEN D -2 THEN AutoSplit THEN ThinTrivial THEN HypSubst' (-1) 0 THEN Auto) }

1
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. u : Point(l)
4. u1 : Point(l)
5. v : Point(l) List
6. (u ∈ v)
7. ∀u:Point(l). ∀v:Point(l) List.
     (u ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l))
8. u1 = u ∈ Point(l)
9. reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
⊢ u1 ∧ u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point\000C(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 ∈ v)
8. ∀u:Point(l). ∀v:Point(l) List.
     (u ∧ reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l))
9. reduce(λx,y. x ∧ y;1;v) = u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ Point(l)
⊢ u1 ∧ u ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) = u ∧ u1 ∧ reduce(λx,y. x ∧ y;1;filter(λx.(¬b(eq x u));v)) ∈ \000CPoint(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  \mmember{}  v)  {}\mRightarrow{}  (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.  (u  \mmember{}  [u1  /  v])
8.  \mforall{}u:Point(l).  \mforall{}v:Point(l)  List.
          (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{}  u1  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;v)
=  u  \mwedge{}  reduce(\mlambda{}x,y.  x  \mwedge{}  y;1;if  \mneg{}\msubb{}(eq  u1  u)
    then  [u1  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v)]
    else  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v)
    fi  )


By

---

Latex:
((RWO  "cons\_member"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  AutoSplit
  THEN  ThinTrivial
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index