---

Step * 1 1 of Lemma dM-hom-invariant

.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
5. x : Point(dM(I))
⊢ dM(I) = free-DeMorgan-lattice(names(I);NamesDeq) ∈ BoundedLattice
BY
{ ((InstLemma `mk-DeMorgan-algebra-equal-bounded-lattice` [⌜free-DeMorgan-lattice(names(I);NamesDeq)⌝;⌜λx.¬(x)⌝]⋅
    THENA Auto
    )
   THEN Fold `free-DeMorgan-algebra` (-1)
   THEN Fold `dM` (-1)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜free-DeMorgan-lattice(names(I);NamesDeq)⌝⋅ THEN Auto)
   THEN Symmetry
   THEN DVar `v'
   THEN EqTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  I  :  fset(\mBbbN{})
2.  J  :  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 
3.  h  :  Hom(dM(J);dM(I))
4.  \mforall{}i:names(I).  (((h  <i>)  =  <i>)  \mwedge{}  ((h  ə-i>)  =  ə-i>))
5.  x  :  Point(dM(I))
\mvdash{}  dM(I)  =  free-DeMorgan-lattice(names(I);NamesDeq)


By

---

Latex:
((InstLemma  `mk-DeMorgan-algebra-equal-bounded-lattice`  [\mkleeneopen{}free-DeMorgan-lattice(names(I);NamesDeq)\mkleeneclose{};
    \mkleeneopen{}\mlambda{}x.\mneg{}(x)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Fold  `free-DeMorgan-algebra`  (-1)
  THEN  Fold  `dM`  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}free-DeMorgan-lattice(names(I);NamesDeq)\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Symmetry
  THEN  DVar  `v'
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index