---

Step * 1 of Lemma dm-neg-sq


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)
BY
{ RepeatFor 2 (EqCD) }

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

---

Latex:

---

Latex:

1.  I  :  Top
2.  J  :  Top
3.  v  :  Top
\mvdash{}  \mlambda{}x,y.  (opposite-lattice(free-DeMorgan-lattice(names(I);NamesDeq))."join"  x  y) 
\msim{}  \mlambda{}x,y.  (opposite-lattice(free-DeMorgan-lattice(names(J);NamesDeq))."join"  x  y)


By

---

Latex:
RepeatFor  2  (EqCD)

---

Home Index