---

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


1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. u : Point(l)
⊢ ∀L:Point(l) List. ((u ∈ L) ⇒ (/\(L) = u ∧ /\(filter(λx.(¬b(eq x u));L)) ∈ Point(l)))
BY
{ (Unfold `lattice-fset-meet` 0
   THEN (InductionOnList THEN Auto)
   THEN Reduce 0
   THEN Assert ⌜∀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))⌝⋅) }

1
.....assertion..... 
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])
⊢ ∀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)) ∈ P\000Coint(l))

2
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)

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  eq  :  EqDecider(Point(l))
3.  u  :  Point(l)
\mvdash{}  \mforall{}L:Point(l)  List.  ((u  \mmember{}  L)  {}\mRightarrow{}  (/\mbackslash{}(L)  =  u  \mwedge{}  /\mbackslash{}(filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));L))))


By

---

Latex:
(Unfold  `lattice-fset-meet`  0
  THEN  (InductionOnList  THEN  Auto)
  THEN  Reduce  0
  THEN  Assert  \mkleeneopen{}\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)))\mkleeneclose{}\000C\mcdot{})

---

Home Index