---

Step * 1 1 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
⊢ free-DeMorgan-lattice(T;eq) = free-DeMorgan-algebra(T;eq) ∈ BoundedLatticeStructure
BY
{ (Unfold `free-DeMorgan-algebra` 0
   THEN RecordExt
   THEN RepUR ``mk-DeMorgan-algebra`` 0
   THEN Try (Folds ``lattice-point lattice-1 lattice-0`` 0)
   THEN Try ((Fold `member` 0 THEN Auto))
   THEN Try (Trivial)
   THEN Try ((RepeatFor 2 ((FunExt THENA Auto)) THEN Folds ``lattice-meet lattice-join`` 0 THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. dm : BoundedDistributiveLattice
4. free-DeMorgan-lattice(T;eq) ∈ BoundedLatticeStructure
5. free-DeMorgan-lattice(T;eq) ∈ BoundedLatticeStructure
⊢ free-DeMorgan-lattice(T;eq)["neg" := λx.¬(x)] ∈ BoundedLatticeStructure

2
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)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  dm  :  BoundedDistributiveLattice
4.  free-DeMorgan-lattice(T;eq)  \mmember{}  BoundedLatticeStructure
\mvdash{}  free-DeMorgan-lattice(T;eq)  =  free-DeMorgan-algebra(T;eq)


By

---

Latex:
(Unfold  `free-DeMorgan-algebra`  0
  THEN  RecordExt
  THEN  RepUR  ``mk-DeMorgan-algebra``  0
  THEN  Try  (Folds  ``lattice-point  lattice-1  lattice-0``  0)
  THEN  Try  ((Fold  `member`  0  THEN  Auto))
  THEN  Try  (Trivial)
  THEN  Try  ((RepeatFor  2  ((FunExt  THENA  Auto))
                        THEN  Folds  ``lattice-meet  lattice-join``  0
                        THEN  Auto)))

---

Home Index