---

Step * 1 2 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)
⊢ TERMOF{free-DeMorgan-algebra-property:o, 1:l, i:l} T eq dm eq2 f ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| 
                                                                      ∀i:T. ((g <i>) = (f i) ∈ Point(dm))} 
BY
{ GenConclAtAddr [2;1;1;1;1] }

1
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))} 

---

Latex:

---

Latex:

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


By

---

Latex:
GenConclAtAddr  [2;1;1;1;1]

---

Home Index