		Search-engine friendly clone of the ACL2 documentation.

Ihs/logior-lemmas

Lemmas about logior from the logops-lemmas book.

Definitions and Theorems

Theorem: commutativity-of-logior

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

Theorem: simplify-logior

(defthm simplify-logior
  (and (equal (logior 0 i) (ifix i))
       (equal (logior -1 i) -1)))

Theorem: logior-=-0

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

Theorem: unsigned-byte-p-logior

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