---

Step * 2 of Lemma lattice-fset-join_wf


1. l : BoundedLattice
2. ∀x,y:Point(l).  Dec(x = y ∈ Point(l))
3. s : fset(Point(l))
4. EqDecider(Point(l))
⊢ \/(s) ∈ Point(l)
BY
{ (RenameVar `eq' (-1)
   THEN Thin 2
   THEN PromoteHyp(-1) 2
   THEN D -1
   THEN MoveToConcl (-1)
   THEN ((GenConcl ⌜s = L1 ∈ (Point(l) List)⌝⋅ THENA Auto) THEN ThinVar `s')
   THEN ((GenConcl ⌜s1 = L2 ∈ (Point(l) List)⌝⋅ THENA Auto) THEN ThinVar `s1')
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (Assert ⌜∀n:ℕ. ∀L1:Point(l) List.
                   (||L1|| < n ⇒ (∀L2:Point(l) List. (set-equal(Point(l);L1;L2) ⇒ (\/(L1) = \/(L2) ∈ Point(l)))))⌝⋅
   THENM ((D 0 THENA Auto) THEN InstHyp [⌜||L1|| + 1⌝;⌜L1⌝] (-2)⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto') }

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

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  \mforall{}x,y:Point(l).    Dec(x  =  y)
3.  s  :  fset(Point(l))
4.  EqDecider(Point(l))
\mvdash{}  \mbackslash{}/(s)  \mmember{}  Point(l)


By

---

Latex:
(RenameVar  `eq'  (-1)
  THEN  Thin  2
  THEN  PromoteHyp(-1)  2
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}s  =  L1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `s')
  THEN  ((GenConcl  \mkleeneopen{}s1  =  L2\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `s1')
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}L1:Point(l)  List.
                                  (||L1||  <  n
                                  {}\mRightarrow{}  (\mforall{}L2:Point(l)  List.  (set-equal(Point(l);L1;L2)  {}\mRightarrow{}  (\mbackslash{}/(L1)  =  \mbackslash{}/(L2)))))\mkleeneclose{}\mcdot{}
  THENM  ((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}||L1||  +  1\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto')

---

Home Index