---

Step * 1 of Lemma dm-neg-properties


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))
BY
{ (Symmetry THEN NthHypEq (-2) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  (\mlambda{}x.\mneg{}(x))  =  (\mlambda{}x.\mneg{}(x))
4.  \mforall{}[a,b:Point(free-DeMorgan-lattice(T;eq))].    ((\mneg{}(a)  \mwedge{}  \mneg{}(b)  =  \mneg{}(a  \mwedge{}  b))  \mwedge{}  (\mneg{}(a)  \mvee{}  \mneg{}(b)  =  \mneg{}(a  \mvee{}  b)))
5.  \mneg{}(0)  =  0
6.  \mneg{}(1)  =  1
7.  Point(free-DeMorgan-lattice(T;eq))  \msim{}  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.  \mneg{}(x)  \mwedge{}  \mneg{}(y)  =  \mneg{}(x  \mwedge{}  y)
11.  \mneg{}(x)  \mvee{}  \mneg{}(y)  =  \mneg{}(x  \mvee{}  y)
\mvdash{}  \mneg{}(x  \mwedge{}  y)  =  \mneg{}(x)  \mvee{}  \mneg{}(y)


By

---

Latex:
(Symmetry  THEN  NthHypEq  (-2)  THEN  EqCD  THEN  Auto)

---

Home Index