---

Step * of Lemma dm-neg-properties

∀[T:Type]. ∀[eq:EqDecider(T)].
  ((∀[x,y:Point(free-DeMorgan-lattice(T;eq))].  (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))))
  ∧ (∀[x,y:Point(free-DeMorgan-lattice(T;eq))].  (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))))
  ∧ (¬(0) = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
  ∧ (¬(1) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))))
BY
{ (InstLemma `dm-neg-is-hom` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (MemTypeHD (-1) THENA Auto)
   THEN All Reduce
   THEN Fold `member` (-2)
   THEN (MemTypeHD (-2) THENA Auto)
   THEN All Reduce
   THEN (Assert Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))) BY
               (RW (SubC (SymbCompC [`free-DeMorgan-lattice`] 30)) 0 THEN Auto))
   THEN RevHypSubst (-1) (-2)
   THEN Auto
   THEN InstHyp [⌜x⌝;⌜y⌝] 4⋅
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. (λx.¬(x)) = (λx.¬(x)) ∈ (Point(free-DeMorgan-lattice(T;eq)) ⟶ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
4. ∀[a,b:Point(free-DeMorgan-lattice(T;eq))].
     ((¬(a) ∧ ¬(b) = ¬(a ∧ b) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
     ∧ (¬(a) ∨ ¬(b) = ¬(a ∨ b) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))))
5. ¬(0) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))
6. ¬(1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq))
7. Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
8. x : Point(free-DeMorgan-lattice(T;eq))
9. y : Point(free-DeMorgan-lattice(T;eq))
10. ¬(x) ∧ ¬(y) = ¬(x ∧ y) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
11. ¬(x) ∨ ¬(y) = ¬(x ∨ y) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
⊢ ¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))

2
1. T : Type
2. eq : EqDecider(T)
3. (λx.¬(x)) = (λx.¬(x)) ∈ (Point(free-DeMorgan-lattice(T;eq)) ⟶ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
4. ∀[a,b:Point(free-DeMorgan-lattice(T;eq))].
     ((¬(a) ∧ ¬(b) = ¬(a ∧ b) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
     ∧ (¬(a) ∨ ¬(b) = ¬(a ∨ b) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))))
5. ¬(0) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))
6. ¬(1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq))
7. Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
8. ∀[x,y:Point(free-DeMorgan-lattice(T;eq))].  (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq)))
9. x : Point(free-DeMorgan-lattice(T;eq))
10. y : Point(free-DeMorgan-lattice(T;eq))
11. ¬(x) ∧ ¬(y) = ¬(x ∧ y) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
12. ¬(x) ∨ ¬(y) = ¬(x ∨ y) ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
⊢ ¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].
    ((\mforall{}[x,y:Point(free-DeMorgan-lattice(T;eq))].    (\mneg{}(x  \mwedge{}  y)  =  \mneg{}(x)  \mvee{}  \mneg{}(y)))
    \mwedge{}  (\mforall{}[x,y:Point(free-DeMorgan-lattice(T;eq))].    (\mneg{}(x  \mvee{}  y)  =  \mneg{}(x)  \mwedge{}  \mneg{}(y)))
    \mwedge{}  (\mneg{}(0)  =  1)
    \mwedge{}  (\mneg{}(1)  =  0))


By

---

Latex:
(InstLemma  `dm-neg-is-hom`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  Fold  `member`  (-2)
  THEN  (MemTypeHD  (-2)  THENA  Auto)
  THEN  All  Reduce
  THEN  (Assert  Point(free-DeMorgan-lattice(T;eq)) 
                          \msim{}  Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))  BY
                          (RW  (SubC  (SymbCompC  [`free-DeMorgan-lattice`]  30))  0  THEN  Auto))
  THEN  RevHypSubst  (-1)  (-2)
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)

---

Home Index