---

Step * 2 2 1 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=0)} ⋃ {(x=1)}) = 0 ∈ Point(face-lattice(T;eq))
⊢ (x=0) ∧ (x=1) = 0 ∈ Point(face-lattice(T;eq))
BY
{ (MoveToConcl (-1)
   THEN (GenConcl ⌜(x=0) = a ∈ Point(face-lattice(T;eq))⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(x=1) = b ∈ Point(face-lattice(T;eq))⌝⋅ THENA Auto)
   THEN All Thin
   THEN RepeatFor 2 (MoveToConcl (-1))) }

1
1. T : Type
2. eq : EqDecider(T)
⊢ ∀a,b:Point(face-lattice(T;eq)).
    ((/\({} ⋃ {a} ⋃ {b}) = 0 ∈ Point(face-lattice(T;eq))) ⇒ (a ∧ b = 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{}(\{\}  \mcup{}  \{(x=0)\}  \mcup{}  \{(x=1)\})  =  0
\mvdash{}  (x=0)  \mwedge{}  (x=1)  =  0


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(x=0)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(x=1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index