---

Step * 3 of Lemma dm-neg-sq


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)
BY
{ RepeatFor 3 ((EqCD THEN Try (Trivial))) }

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

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

---

Latex:

---

Latex:

1.  I  :  Top
2.  J  :  Top
3.  v  :  Top
\mvdash{}  ..."(v) 
\msim{}  ..."(v)


By

---

Latex:
RepeatFor  3  ((EqCD  THEN  Try  (Trivial)))

---

Home Index