---

Step * 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)
⊢ (x=0) ∧ (x=1) = 0 ∈ Point(face-lattice(T;eq))
BY
{ ((InstLemma `free-dlwc-satisfies-constraints` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜λ2x.face-lattice-constraints(x)⌝;
    ⌜inl x⌝]⋅
    THENA Try (Complete ((Auto THEN SubsumeC ⌜(T + T) List⌝⋅ THEN Auto)))
    )
   THEN Try ((Fold `face-lattice` (-1) THEN Reduce (-1)))
   THEN (InstHyp [⌜{inl x,inr x }⌝] (-1)⋅ THENA Auto)) }

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)

2
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))

---

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)
\mvdash{}  (x=0)  \mwedge{}  (x=1)  =  0


By

---

Latex:
((InstLemma  `free-dlwc-satisfies-constraints`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};
    \mkleeneopen{}\mlambda{}\msubtwo{}x.face-lattice-constraints(x)\mkleeneclose{};\mkleeneopen{}inl  x\mkleeneclose{}]\mcdot{}
    THENA  Try  (Complete  ((Auto  THEN  SubsumeC  \mkleeneopen{}(T  +  T)  List\mkleeneclose{}\mcdot{}  THEN  Auto)))
    )
  THEN  Try  ((Fold  `face-lattice`  (-1)  THEN  Reduce  (-1)))
  THEN  (InstHyp  [\mkleeneopen{}\{inl  x,inr  x  \}\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index