---

Step * 2 2 1 1 of Lemma mk-DeMorgan-algebra_wf


1. L : BoundedLatticeStructure
2. lattice-axioms(L)
3. bounded-lattice-axioms(L)
4. ∀[a,b,c:Point(L)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L))
5. n : Point(L) ⟶ Point(L)
6. ∀x:Point(L). ((n (n x)) = x ∈ Point(L))
7. (∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L)))
8. L["neg" := n] ∈ BoundedLatticeStructure
9. L["neg" := n] ∈ DeMorganAlgebraStructure
⊢ L = L["neg" := n] ∈ BoundedLatticeStructure
BY
{ ((RecordExt THEN Try (Trivial))
   THEN Try ((Reduce 0
              THEN Folds ``lattice-point lattice-0 lattice-1`` 0
              THEN ((RepeatFor 2 ((FunExt THENA Auto)) THEN Folds ``lattice-meet lattice-join`` 0 THEN Auto)
              ORELSE Auto
              )))
   ) }

1
1. L : BoundedLatticeStructure
2. lattice-axioms(L)
3. bounded-lattice-axioms(L)
4. ∀[a,b,c:Point(L)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L))
5. n : Point(L) ⟶ Point(L)
6. ∀x:Point(L). ((n (n x)) = x ∈ Point(L))
7. (∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L)))
8. L["neg" := n] ∈ BoundedLatticeStructure
9. L["neg" := n] ∈ DeMorganAlgebraStructure
10. L ∈ record(x.Top)
11. L["neg" := n] ∈ record(x.Top)
⊢ L = L["neg" := n] ∈ record(x.Top)

---

Latex:

---

Latex:

1.  L  :  BoundedLatticeStructure
2.  lattice-axioms(L)
3.  bounded-lattice-axioms(L)
4.  \mforall{}[a,b,c:Point(L)].    (a  \mwedge{}  b  \mvee{}  c  =  a  \mwedge{}  b  \mvee{}  a  \mwedge{}  c)
5.  n  :  Point(L)  {}\mrightarrow{}  Point(L)
6.  \mforall{}x:Point(L).  ((n  (n  x))  =  x)
7.  (\mforall{}x,y:Point(L).    ((n  x  \mwedge{}  y)  =  n  x  \mvee{}  n  y))  \mvee{}  (\mforall{}x,y:Point(L).    ((n  x  \mvee{}  y)  =  n  x  \mwedge{}  n  y))
8.  L["neg"  :=  n]  \mmember{}  BoundedLatticeStructure
9.  L["neg"  :=  n]  \mmember{}  DeMorganAlgebraStructure
\mvdash{}  L  =  L["neg"  :=  n]


By

---

Latex:
((RecordExt  THEN  Try  (Trivial))
  THEN  Try  ((Reduce  0
                        THEN  Folds  ``lattice-point  lattice-0  lattice-1``  0
                        THEN  ((RepeatFor  2  ((FunExt  THENA  Auto))
                                      THEN  Folds  ``lattice-meet  lattice-join``  0
                                      THEN  Auto)
                        ORELSE  Auto
                        )))
  )

---

Home Index