---

Step * of Lemma dM-lift-sq

∀[I',J',I,J,f:Top].  (dM-lift(I;J;f) ~ dM-lift(I';J';f))
BY
{ (((UnivCD THENA Auto) THEN RW (SubC (TagC (mk_tag_term 4))) 0)
   THEN RepUR ``union-deq free-dml-deq dma-neg dM lattice-extend`` 0
   THEN (RepUR ``lattice-fset-join lattice-join free-DeMorgan-algebra`` 0
         THEN RepUR ``lattice-fset-meet lattice-meet`` 0
         )
   THEN RepUR ``mk-DeMorgan-algebra free-DeMorgan-lattice`` 0
   THEN RepUR ``free-dist-lattice union-deq mk-bounded-distributive-lattice`` 0
   THEN RepUR ``mk-bounded-lattice lattice-0 lattice-1`` 0
   THEN RepeatFor 8 ((EqCD THEN Try (Trivial)))) }

1
1. I' : Top
2. J' : Top
3. I : Top
4. J : Top
5. f : Top
6. ac : Base
7. xs : Base
8. p : Base
9. a : Base
⊢ dm-neg(names(I);NamesDeq;f a) ~ dm-neg(names(I');NamesDeq;f a)

---

Latex:

---

Latex:
\mforall{}[I',J',I,J,f:Top].    (dM-lift(I;J;f)  \msim{}  dM-lift(I';J';f))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  RW  (SubC  (TagC  (mk\_tag\_term  4)))  0)
  THEN  RepUR  ``union-deq  free-dml-deq  dma-neg  dM  lattice-extend``  0
  THEN  (RepUR  ``lattice-fset-join  lattice-join  free-DeMorgan-algebra``  0
              THEN  RepUR  ``lattice-fset-meet  lattice-meet``  0
              )
  THEN  RepUR  ``mk-DeMorgan-algebra  free-DeMorgan-lattice``  0
  THEN  RepUR  ``free-dist-lattice  union-deq  mk-bounded-distributive-lattice``  0
  THEN  RepUR  ``mk-bounded-lattice  lattice-0  lattice-1``  0
  THEN  RepeatFor  8  ((EqCD  THEN  Try  (Trivial))))

---

Home Index