---

Step * 4 of Lemma face_lattice-fset-join-eq-1


1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇒ (∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
5. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
6. ¬x ∈ s
7. \/(fset-add(face_lattice-deq();x;s)) = 1 ∈ Point(face_lattice(I))
⊢ ∃x@0:Point(face_lattice(I)). (x@0 ∈ fset-add(face_lattice-deq();x;s) ∧ (x@0 = 1 ∈ Point(face_lattice(I))))
BY
{ ((RepUR ``fset-add`` -1 THEN RepUR ``fset-add`` 0)
   THEN (RWW  "lattice-fset-join-union lattice-fset-join-singleton" (-1) THENA Auto)
   THEN (RWO  "face_lattice-1-join-irreducible" (-1) THENA Auto)
   THEN D -1
   THEN ThinTrivial) }

1
1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇒ (∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
5. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
6. ¬x ∈ s
7. x = 1 ∈ Point(face_lattice(I))
⊢ ∃x@0:Point(face_lattice(I)). (x@0 ∈ {x} ⋃ s ∧ (x@0 = 1 ∈ Point(face_lattice(I))))

2
1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
5. ¬x ∈ s
6. \/(s) = 1 ∈ Point(face_lattice(I))
7. ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
⊢ ∃x@0:Point(face_lattice(I)). (x@0 ∈ {x} ⋃ s ∧ (x@0 = 1 ∈ Point(face_lattice(I))))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  s  :  fset(Point(face\_lattice(I)))
3.  x  :  Point(face\_lattice(I))
4.  (\mbackslash{}/(s)  =  1)  {}\mRightarrow{}  (\mexists{}x:Point(face\_lattice(I)).  (x  \mmember{}  s  \mwedge{}  (x  =  1)))
5.  (\mbackslash{}/(s)  =  1)  \mLeftarrow{}{}  \mexists{}x:Point(face\_lattice(I)).  (x  \mmember{}  s  \mwedge{}  (x  =  1))
6.  \mneg{}x  \mmember{}  s
7.  \mbackslash{}/(fset-add(face\_lattice-deq();x;s))  =  1
\mvdash{}  \mexists{}x@0:Point(face\_lattice(I)).  (x@0  \mmember{}  fset-add(face\_lattice-deq();x;s)  \mwedge{}  (x@0  =  1))


By

---

Latex:
((RepUR  ``fset-add``  -1  THEN  RepUR  ``fset-add``  0)
  THEN  (RWW    "lattice-fset-join-union  lattice-fset-join-singleton"  (-1)  THENA  Auto)
  THEN  (RWO    "face\_lattice-1-join-irreducible"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  ThinTrivial)

---

Home Index