---

Step * 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. L1 : Point(l) List
7. ||L1|| < n
8. L2 : Point(l) List
9. set-equal(Point(l);L1;L2)
⊢ \/(L1) = \/(L2) ∈ Point(l)
BY
{ DVar `L1' }

1
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. ||[]|| < n
7. L2 : Point(l) List
8. set-equal(Point(l);[];L2)
⊢ \/([]) = \/(L2) ∈ 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)
⊢ \/([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.  L1  :  Point(l)  List
7.  ||L1||  <  n
8.  L2  :  Point(l)  List
9.  set-equal(Point(l);L1;L2)
\mvdash{}  \mbackslash{}/(L1)  =  \mbackslash{}/(L2)


By

---

Latex:
DVar  `L1'

---

Home Index