---

Step * 2 1 2 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)
⊢ \/([u / v]) = \/(L2) ∈ Point(l)
BY
{ ((InstLemma `set-equal-cons2` [Point(l);eq;u;⌜v⌝;⌜L2⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN RepeatFor 2 ((D -1 THENA Auto))
   THEN (FHyp 5 [-1] THENA 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. 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)

---

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)
\mvdash{}  \mbackslash{}/([u  /  v])  =  \mbackslash{}/(L2)


By

---

Latex:
((InstLemma  `set-equal-cons2`  [Point(l);eq;u;\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  RepeatFor  2  ((D  -1  THENA  Auto))
  THEN  (FHyp  5  [-1]  THENA  Auto))

---

Home Index