---

Step * of Lemma free-DeMorgan-algebra-property

∀T:Type. ∀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)))])
BY
{ (Auto
   THEN (InstLemma `free-dist-lattice-property` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜dm⌝;⌜eq2⌝;⌜λp.case p
                                                                                                of inl(a) =>
                                                                                                f a
                                                                                                | inr(a) =>
                                                                                                ¬(f a)⌝]⋅
         THENA Auto
         )
   THEN Fold `free-DeMorgan-lattice` (-1)
   THEN ExRepD
   THEN (Assert ∀i:T. ((g <i>) = (f i) ∈ Point(dm)) BY
               (Auto
                THEN ((ApFunToHypEquands `Z' ⌜Z (inl i)⌝ ⌜Point(dm)⌝ (-2)⋅ THENM Reduce (-1)) THENA Auto)
                THEN Fold `dminc` (-1)
                THEN Eq))
   THEN With ⌜g⌝ (D 0)⋅
   THEN Auto) }

1
.....wf..... 
1. T : Type@i'
2. eq : EqDecider(T)@i
3. dm : DeMorganAlgebra@i'
4. eq2 : EqDecider(Point(dm))@i
5. f : T ⟶ Point(dm)@i
6. g : Hom(free-DeMorgan-lattice(T;eq);dm)
7. (λp.case p of inl(a) => f a | inr(a) => ¬(f a)) = (g o (λx.free-dl-inc(x))) ∈ ((T + T) ⟶ Point(dm))
8. ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
⊢ g ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm)

---

Latex:

---

Latex:
\mforall{}T:Type.  \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)))])


By

---

Latex:
(Auto
  THEN  (InstLemma  `free-dist-lattice-property`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};\mkleeneopen{}dm\mkleeneclose{};\mkleeneopen{}eq2\mkleeneclose{};
              \mkleeneopen{}\mlambda{}p.case  p  of  inl(a)  =>  f  a  |  inr(a)  =>  \mneg{}(f  a)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `free-DeMorgan-lattice`  (-1)
  THEN  ExRepD
  THEN  (Assert  \mforall{}i:T.  ((g  <i>)  =  (f  i))  BY
                          (Auto
                            THEN  ((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  (inl  i)\mkleeneclose{}  \mkleeneopen{}Point(dm)\mkleeneclose{}  (-2)\mcdot{}  THENM  Reduce  (-1))
                                        THENA  Auto
                                        )
                            THEN  Fold  `dminc`  (-1)
                            THEN  Eq))
  THEN  With  \mkleeneopen{}g\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index