---

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

.....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))
BY
{ (All Thin THEN (D 0 THENA Auto) THEN InductionOnList THEN Reduce 0 THEN Auto THEN AutoSplit) }

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

---

Latex:

---

Latex:
.....assertion..... 
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])
\mvdash{}  \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)))


By

---

Latex:
(All  Thin  THEN  (D  0  THENA  Auto)  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  AutoSplit)

---

Home Index