		Search-engine friendly clone of the ACL2 documentation.

Ihs/logxor-lemmas

Lemmas about logxor from the logops-lemmas book.

Definitions and Theorems

Theorem: commutativity-of-logxor

(defthm commutativity-of-logxor
  (equal (logxor i j) (logxor j i)))

Theorem: simplify-logxor

(defthm simplify-logxor
  (and (equal (logxor 0 i) (ifix i))
       (equal (logxor -1 i) (lognot i))))

Theorem: logxor-=-0

(defthm logxor-=-0
  (implies (and (force (integerp i))
                (force (integerp j)))
           (equal (equal (logxor i j) 0)
                  (equal i j))))

Theorem: unsigned-byte-p-logxor

(defthm unsigned-byte-p-logxor
  (implies (and (unsigned-byte-p size i)
                (unsigned-byte-p size j)
                (force (integerp i))
                (force (integerp j)))
           (unsigned-byte-p size (logxor i j))))