---

Step * 1 2 1 of Lemma free-dma-lift_wf


1. T : Type
2. eq : EqDecider(T)
3. dm : DeMorganAlgebra
4. eq2 : EqDecider(Point(dm))
5. f : T ⟶ Point(dm)
6. v : ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
         (∃g:dma-hom(free-DeMorgan-algebra(T;eq);dm) [(∀i:T. ((g <i>) = (f i) ∈ Point(dm)))])
7. (TERMOF{free-DeMorgan-algebra-property:o, 1:l, i:l} T)
= v
∈ (∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
     (∃g:dma-hom(free-DeMorgan-algebra(T;eq);dm) [(∀i:T. ((g <i>) = (f i) ∈ Point(dm)))]))
⊢ v eq dm eq2 f ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| ∀i:T. ((g <i>) = (f i) ∈ Point(dm))} 
BY
{ (Fold `sq_exists` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  dm  :  DeMorganAlgebra
4.  eq2  :  EqDecider(Point(dm))
5.  f  :  T  {}\mrightarrow{}  Point(dm)
6.  v  :  \mforall{}eq:EqDecider(T).  \mforall{}dm:DeMorganAlgebra.  \mforall{}eq2:EqDecider(Point(dm)).  \mforall{}f:T  {}\mrightarrow{}  Point(dm).
                  (\mexists{}g:dma-hom(free-DeMorgan-algebra(T;eq);dm)  [(\mforall{}i:T.  ((g  <i>)  =  (f  i)))])
7.  (TERMOF\{free-DeMorgan-algebra-property:o,  1:l,  i:l\}  T)  =  v
\mvdash{}  v  eq  dm  eq2  f  \mmember{}  \{g:dma-hom(free-DeMorgan-algebra(T;eq);dm)|  \mforall{}i:T.  ((g  <i>)  =  (f  i))\} 


By

---

Latex:
(Fold  `sq\_exists`  0  THEN  Auto)

---

Home Index