---

Step * 2 1 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. ||[]|| < n
7. L2 : Point(l) List
8. set-equal(Point(l);[];L2)
⊢ \/([]) = \/(L2) ∈ Point(l)
BY
{ ((RWO "set-equal-nil" (-1) THENA Auto)
   THEN DVar `L2'
   THEN All Reduce
   THEN Auto
   THEN RepUR ``lattice-fset-join`` 0
   THEN Auto) }

---

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


By

---

Latex:
((RWO  "set-equal-nil"  (-1)  THENA  Auto)
  THEN  DVar  `L2'
  THEN  All  Reduce
  THEN  Auto
  THEN  RepUR  ``lattice-fset-join``  0
  THEN  Auto)

---

Home Index