---

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


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))))
6. /\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"({inl x,inr x }))
= 0
∈ Point(face-lattice(T;eq))
⊢ (x=0) ∧ (x=1) = 0 ∈ Point(face-lattice(T;eq))
BY
{ (RepUR ``fset-image f-union fset-pair`` -1
   THEN (RWO "face-lattice0-is-inc< face-lattice1-is-inc<" (-1) THENA Auto)
   THEN Fold `empty-fset` (-1)) }

1
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))))
6. /\({} ⋃ {(x=0)} ⋃ {(x=1)}) = 0 ∈ Point(face-lattice(T;eq))
⊢ (x=0) ∧ (x=1) = 0 ∈ Point(face-lattice(T;eq))

---

Latex:

---

Latex:

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))
6.  /\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(\{inl  x,inr  x  \}))  =  0
\mvdash{}  (x=0)  \mwedge{}  (x=1)  =  0


By

---

Latex:
(RepUR  ``fset-image  f-union  fset-pair``  -1
  THEN  (RWO  "face-lattice0-is-inc<  face-lattice1-is-inc<"  (-1)  THENA  Auto)
  THEN  Fold  `empty-fset`  (-1))

---

Home Index