---

Step * 1 1 2 of Lemma free-dma-hom-is-lattice-hom


1. T : Type
2. eq : EqDecider(T)
3. dm : BoundedDistributiveLattice
4. free-DeMorgan-lattice(T;eq) ∈ BoundedLatticeStructure
5. free-DeMorgan-lattice(T;eq) ∈ record(x.Top)
6. mk-DeMorgan-algebra(free-DeMorgan-lattice(T;eq);λx.¬(x)) ∈ record(x.Top)
⊢ free-DeMorgan-lattice(T;eq) = free-DeMorgan-lattice(T;eq)["neg" := λx.¬(x)] ∈ record(x.Top)
BY
{ ((GenConclTerm ⌜free-DeMorgan-lattice(T;eq)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λx.¬(x)) = F ∈ Top⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. v : record(x.Top)
2. F : Top
⊢ v = v["neg" := F] ∈ record(x.Top)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  dm  :  BoundedDistributiveLattice
4.  free-DeMorgan-lattice(T;eq)  \mmember{}  BoundedLatticeStructure
5.  free-DeMorgan-lattice(T;eq)  \mmember{}  record(x.Top)
6.  mk-DeMorgan-algebra(free-DeMorgan-lattice(T;eq);\mlambda{}x.\mneg{}(x))  \mmember{}  record(x.Top)
\mvdash{}  free-DeMorgan-lattice(T;eq)  =  free-DeMorgan-lattice(T;eq)["neg"  :=  \mlambda{}x.\mneg{}(x)]


By

---

Latex:
((GenConclTerm  \mkleeneopen{}free-DeMorgan-lattice(T;eq)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}x.\mneg{}(x))  =  F\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index