---

Step * 1 of Lemma assert-fl-eq


1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. Point(face_lattice(I)) ⊆r Point(free-DeMorgan-lattice(names(I);NamesDeq))
⊢ uiff(↑(x==y);x = y ∈ Point(face_lattice(I)))
BY
{ (Unfold `fl-eq` 0 THEN (GenConclTerm ⌜free-dml-deq(names(I);NamesDeq)⌝⋅ THENA Auto)) }

1
1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. Point(face_lattice(I)) ⊆r Point(free-DeMorgan-lattice(names(I);NamesDeq))
5. v : EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))
6. free-dml-deq(names(I);NamesDeq) = v ∈ EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))
⊢ uiff(↑(v x y);x = y ∈ Point(face_lattice(I)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(face\_lattice(I))
3.  y  :  Point(face\_lattice(I))
4.  Point(face\_lattice(I))  \msubseteq{}r  Point(free-DeMorgan-lattice(names(I);NamesDeq))
\mvdash{}  uiff(\muparrow{}(x==y);x  =  y)


By

---

Latex:
(Unfold  `fl-eq`  0  THEN  (GenConclTerm  \mkleeneopen{}free-dml-deq(names(I);NamesDeq)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index