		Search-engine friendly clone of the ACL2 documentation.

Ihs/lognot-lemmas

Lemmas about lognot from the logops-lemmas book.

Definitions and Theorems

Theorem: lognot-lognot

(defthm lognot-lognot
  (implies (case-split (integerp i))
           (equal (lognot (lognot i)) i)))

Theorem: cancel-equal-lognot

(defthm cancel-equal-lognot
  (equal (equal (lognot i) (lognot j))
         (equal (ifix i) (ifix j)))
  :rule-classes
  ((:rewrite)
   (:rewrite
        :corollary (implies (and (syntaxp (constant-syntaxp j))
                                 (integerp j))
                            (equal (equal (lognot i) j)
                                   (equal (ifix i) (lognot j)))))))