---

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


1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. n : ℤ
4. 0 < n
5. ∀L1:Point(l) List
     (||L1|| < n - 1 ⇒ (∀L2:Point(l) List. (set-equal(Point(l);L1;L2) ⇒ (\/(L1) = \/(L2) ∈ Point(l)))))
6. u : Point(l)
7. v : Point(l) List
8. ||[u / v]|| < n
9. L2 : Point(l) List
10. set-equal(Point(l);[u / v];L2)
11. (u ∈ L2)
12. set-equal(Point(l);filter(λx.(¬b(eq x u));v);filter(λx.(¬b(eq x u));L2))
13. \/(filter(λx.(¬b(eq x u));v)) = \/(filter(λx.(¬b(eq x u));L2)) ∈ Point(l)
⊢ \/([u / v]) = \/(L2) ∈ Point(l)
BY
{ Assert ⌜∀L:Point(l) List. ((u ∈ L) ⇒ (\/(L) = u ∨ \/(filter(λx.(¬b(eq x u));L)) ∈ Point(l)))⌝⋅ }

1
.....assertion..... 
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. n : ℤ
4. 0 < n
5. ∀L1:Point(l) List
     (||L1|| < n - 1 ⇒ (∀L2:Point(l) List. (set-equal(Point(l);L1;L2) ⇒ (\/(L1) = \/(L2) ∈ Point(l)))))
6. u : Point(l)
7. v : Point(l) List
8. ||[u / v]|| < n
9. L2 : Point(l) List
10. set-equal(Point(l);[u / v];L2)
11. (u ∈ L2)
12. set-equal(Point(l);filter(λx.(¬b(eq x u));v);filter(λx.(¬b(eq x u));L2))
13. \/(filter(λx.(¬b(eq x u));v)) = \/(filter(λx.(¬b(eq x u));L2)) ∈ Point(l)
⊢ ∀L:Point(l) List. ((u ∈ L) ⇒ (\/(L) = u ∨ \/(filter(λx.(¬b(eq x u));L)) ∈ Point(l)))

2
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. n : ℤ
4. 0 < n
5. ∀L1:Point(l) List
     (||L1|| < n - 1 ⇒ (∀L2:Point(l) List. (set-equal(Point(l);L1;L2) ⇒ (\/(L1) = \/(L2) ∈ Point(l)))))
6. u : Point(l)
7. v : Point(l) List
8. ||[u / v]|| < n
9. L2 : Point(l) List
10. set-equal(Point(l);[u / v];L2)
11. (u ∈ L2)
12. set-equal(Point(l);filter(λx.(¬b(eq x u));v);filter(λx.(¬b(eq x u));L2))
13. \/(filter(λx.(¬b(eq x u));v)) = \/(filter(λx.(¬b(eq x u));L2)) ∈ Point(l)
14. ∀L:Point(l) List. ((u ∈ L) ⇒ (\/(L) = u ∨ \/(filter(λx.(¬b(eq x u));L)) ∈ Point(l)))
⊢ \/([u / v]) = \/(L2) ∈ Point(l)

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  eq  :  EqDecider(Point(l))
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}L1:Point(l)  List
          (||L1||  <  n  -  1  {}\mRightarrow{}  (\mforall{}L2:Point(l)  List.  (set-equal(Point(l);L1;L2)  {}\mRightarrow{}  (\mbackslash{}/(L1)  =  \mbackslash{}/(L2)))))
6.  u  :  Point(l)
7.  v  :  Point(l)  List
8.  ||[u  /  v]||  <  n
9.  L2  :  Point(l)  List
10.  set-equal(Point(l);[u  /  v];L2)
11.  (u  \mmember{}  L2)
12.  set-equal(Point(l);filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v);filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));L2))
13.  \mbackslash{}/(filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));v))  =  \mbackslash{}/(filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));L2))
\mvdash{}  \mbackslash{}/([u  /  v])  =  \mbackslash{}/(L2)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}L:Point(l)  List.  ((u  \mmember{}  L)  {}\mRightarrow{}  (\mbackslash{}/(L)  =  u  \mvee{}  \mbackslash{}/(filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));L))))\mkleeneclose{}\mcdot{}

---

Home Index