---

Step * of Lemma dm-neg-sq

∀[I,J,v:Top].  (dm-neg(names(I);NamesDeq;v) ~ dm-neg(names(J);NamesDeq;v))
BY
{ ((UnivCD THENA Auto)
   THEN (RepUR ``dm-neg lattice-extend lattice-fset-join lattice-fset-meet union-deq`` 0
         THEN RepUR ``lattice-meet lattice-join lattice-0 lattice-1`` 0
         )
   THEN EqCD) }

1
1. I : Top
2. J : Top
3. v : Top
⊢ λx,y. (opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."join" x y) 
~ λx,y. (opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."join" x y)

2
1. I : Top
2. J : Top
3. v : Top
⊢ opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."0" 
~ opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."0"

3
1. I : Top
2. J : Top
3. v : Top
⊢ λxs.reduce(λx,y. (opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."meet" x 
                    y);opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."1";λz.case z
                                                                                      of inl(a) =>
                                                                                      {{inr a }}
                                                                                      | inr(a) =>
                                                                                      {{inl a}}"(xs))"(v) 
~ λxs.reduce(λx,y. (opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."meet" x 
                    y);opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."1";λz.case z
                                                                                      of inl(a) =>
                                                                                      {{inr a }}
                                                                                      | inr(a) =>
                                                                                      {{inl a}}"(xs))"(v)

---

Latex:

---

Latex:
\mforall{}[I,J,v:Top].    (dm-neg(names(I);NamesDeq;v)  \msim{}  dm-neg(names(J);NamesDeq;v))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepUR  ``dm-neg  lattice-extend  lattice-fset-join  lattice-fset-meet  union-deq``  0
              THEN  RepUR  ``lattice-meet  lattice-join  lattice-0  lattice-1``  0
              )
  THEN  EqCD)

---

Home Index