---

Step * 2 1 of Lemma fl-meet-0-1

.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ∀x:T + T. ∀c:fset(T + T).  (c ∈ face-lattice-constraints(x) ⇒ x ∈ c)
5. ∀c:fset(T + T)
     (c ∈ face-lattice-constraints(inl x)
     ⇒ (/\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(c))
        = 0
        ∈ Point(face-lattice(T;eq))))
⊢ {inl x,inr x } ∈ face-lattice-constraints(inl x)
BY
{ ((Assert inl x ∈ T + T BY
          Auto)
   THEN (Assert inr x  ∈ T + T BY
               Auto)
   THEN RepUR ``face-lattice-constraints`` 0
   THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  \mforall{}x:T  +  T.  \mforall{}c:fset(T  +  T).    (c  \mmember{}  face-lattice-constraints(x)  {}\mRightarrow{}  x  \mmember{}  c)
5.  \mforall{}c:fset(T  +  T)
          (c  \mmember{}  face-lattice-constraints(inl  x)
          {}\mRightarrow{}  (/\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(c))  =  0))
\mvdash{}  \{inl  x,inr  x  \}  \mmember{}  face-lattice-constraints(inl  x)


By

---

Latex:
((Assert  inl  x  \mmember{}  T  +  T  BY
                Auto)
  THEN  (Assert  inr  x    \mmember{}  T  +  T  BY
                          Auto)
  THEN  RepUR  ``face-lattice-constraints``  0
  THEN  EAuto  1)

---

Home Index