---

Step * 1 of Lemma face-lattice-property


1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f0 : T ⟶ Point(L)@i
6. f1 : T ⟶ Point(L)@i
7. ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
8. x : T + T@i
9. c : fset(T + T)@i
10. c ∈ face-lattice-constraints(x)
⊢ /\(λx.case x of inl(a) => f0 a | inr(b) => f1 b"(c)) = 0 ∈ Point(L)
BY
{ (DVar `x'
   THEN RepUR ``face-lattice-constraints`` -1
   THEN (RWO "member-fset-singleton" (-1) THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN (RepUR ``fset-image fset-pair f-union`` 0 THEN Fold `empty-fset` 0)
   THEN (RWW "lattice-fset-meet-union lattice-fset-meet-singleton" 0 THENA Auto)
   THEN RepUR ``lattice-fset-meet empty-fset`` 0
   THEN RenameVar `z' (-3)
   THEN (InstHyp [⌜z⌝] (-4)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜f0 z⌝;⌜f1 z⌝]⋅
   THEN All Thin) }

1
1. L : BoundedDistributiveLattice@i'
2. v : Point(L)@i
3. v1 : Point(L)@i
⊢ (v ∧ v1 = 0 ∈ Point(L)) ⇒ (1 ∧ v ∧ v1 = 0 ∈ Point(L))

2
1. L : BoundedDistributiveLattice@i'
2. v : Point(L)@i
3. v1 : Point(L)@i
⊢ (v ∧ v1 = 0 ∈ Point(L)) ⇒ (1 ∧ v ∧ v1 = 0 ∈ Point(L))

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  L  :  BoundedDistributiveLattice@i'
4.  eqL  :  EqDecider(Point(L))@i
5.  f0  :  T  {}\mrightarrow{}  Point(L)@i
6.  f1  :  T  {}\mrightarrow{}  Point(L)@i
7.  \mforall{}x:T.  (f0  x  \mwedge{}  f1  x  =  0)
8.  x  :  T  +  T@i
9.  c  :  fset(T  +  T)@i
10.  c  \mmember{}  face-lattice-constraints(x)
\mvdash{}  /\mbackslash{}(\mlambda{}x.case  x  of  inl(a)  =>  f0  a  |  inr(b)  =>  f1  b"(c))  =  0


By

---

Latex:
(DVar  `x'
  THEN  RepUR  ``face-lattice-constraints``  -1
  THEN  (RWO  "member-fset-singleton"  (-1)  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  (RepUR  ``fset-image  fset-pair  f-union``  0  THEN  Fold  `empty-fset`  0)
  THEN  (RWW  "lattice-fset-meet-union  lattice-fset-meet-singleton"  0  THENA  Auto)
  THEN  RepUR  ``lattice-fset-meet  empty-fset``  0
  THEN  RenameVar  `z'  (-3)
  THEN  (InstHyp  [\mkleeneopen{}z\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}f0  z\mkleeneclose{};\mkleeneopen{}f1  z\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index