---

Step * 1 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))
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)))
BY
{ Assert ⌜uiff(x = y ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq));x = y ∈ Point(face_lattice(I)))⌝⋅ }

1
.....assertion..... 
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(x = y ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq));x = y ∈ Point(face_lattice(I)))

2
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)))
7. uiff(x = y ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq));x = y ∈ Point(face_lattice(I)))
⊢ 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))
5.  v  :  EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))
6.  free-dml-deq(names(I);NamesDeq)  =  v
\mvdash{}  uiff(\muparrow{}(v  x  y);x  =  y)


By

---

Latex:
Assert  \mkleeneopen{}uiff(x  =  y;x  =  y)\mkleeneclose{}\mcdot{}

---

Home Index