		Search-engine friendly clone of the ACL2 documentation.

Ihs/lognotu-lemmas

Lemmas about lognotu from the logops-lemmas book.

Definitions and Theorems

Theorem: lognotu-lognotu

(defthm lognotu-lognotu
  (implies (and (<= size1 size)
                (>= size1 0)
                (integerp size1)
                (lognotu-guard size i))
           (equal (lognotu size1 (lognotu size i))
                  (loghead size1 i))))

Theorem: cancel-equal-lognotu

(defthm cancel-equal-lognotu
  (implies (and (unsigned-byte-p size i)
                (unsigned-byte-p size j))
           (equal (equal (lognotu size i)
                         (lognotu size j))
                  (equal i j))))