---

Step * of Lemma fl-deq_wf

∀[T:Type]. ∀[eq:EqDecider(T)].  (fl-deq(T;eq) ∈ EqDecider(Point(face-lattice(T;eq))))
BY
{ ((InstLemma `fl-point` [] THEN RepeatFor 2 (ParallelLast'))
   THEN SubsumeC ⌜EqDecider({ac:fset(fset(T + T))| 
                             (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                             ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} )⌝⋅
   ) }

1
1. T : Type
2. eq : EqDecider(T)
3. Point(face-lattice(T;eq)) ≡ {ac:fset(fset(T + T))| 
                                (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                                ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} 
⊢ fl-deq(T;eq) ∈ EqDecider({ac:fset(fset(T + T))| 
                            (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                            ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} )

2
1. T : Type
2. eq : EqDecider(T)
3. Point(face-lattice(T;eq)) ≡ {ac:fset(fset(T + T))| 
                                (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                                ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} 
4. fl-deq(T;eq)
= fl-deq(T;eq)
∈ EqDecider({ac:fset(fset(T + T))| 
             (↑fset-antichain(union-deq(T;T;eq;eq);ac))
             ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} )
⊢ EqDecider({ac:fset(fset(T + T))| 
             (↑fset-antichain(union-deq(T;T;eq;eq);ac))
             ∧ (∀a:fset(T + T). (a ∈ ac ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))} ) ⊆r EqDecider(Point(face-lattice(T;eq\000C)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].    (fl-deq(T;eq)  \mmember{}  EqDecider(Point(face-lattice(T;eq))))


By

---

Latex:
((InstLemma  `fl-point`  []  THEN  RepeatFor  2  (ParallelLast'))
  THEN  SubsumeC  \mkleeneopen{}EqDecider(\{ac:fset(fset(T  +  T))| 
                                                      (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);ac))
                                                      \mwedge{}  (\mforall{}a:fset(T  +  T).  (a  \mmember{}  ac  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)))))\}  )\mkleeneclose{}\mcdot{}
  )

---

Home Index