		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Binary-bittest

Signature
(binary-bittest op x y) → *
Arguments: op — Guard (integerp op).; x — Guard (integerp x).; y — Guard (integerp y).

Definitions and Theorems

Function: binary-bittest

(defun binary-bittest (op x y)
  (declare (type (unsigned-byte 4) op))
  (declare (xargs :guard (and (integerp op)
                              (integerp x)
                              (integerp y))))
  (let ((__function__ 'binary-bittest))
    (declare (ignorable __function__))
    (not (eql 0 (binary-bitop op x y)))))

Theorem: binary-bittest-of-ifix-op

(defthm binary-bittest-of-ifix-op
  (equal (binary-bittest (ifix op) x y)
         (binary-bittest op x y)))

Theorem: binary-bittest-int-equiv-congruence-on-op

(defthm binary-bittest-int-equiv-congruence-on-op
  (implies (int-equiv op op-equiv)
           (equal (binary-bittest op x y)
                  (binary-bittest op-equiv x y)))
  :rule-classes :congruence)

Theorem: binary-bittest-of-ifix-x

(defthm binary-bittest-of-ifix-x
  (equal (binary-bittest op (ifix x) y)
         (binary-bittest op x y)))

Theorem: binary-bittest-int-equiv-congruence-on-x

(defthm binary-bittest-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (binary-bittest op x y)
                  (binary-bittest op x-equiv y)))
  :rule-classes :congruence)

Theorem: binary-bittest-of-ifix-y

(defthm binary-bittest-of-ifix-y
  (equal (binary-bittest op x (ifix y))
         (binary-bittest op x y)))

Theorem: binary-bittest-int-equiv-congruence-on-y

(defthm binary-bittest-int-equiv-congruence-on-y
  (implies (int-equiv y y-equiv)
           (equal (binary-bittest op x y)
                  (binary-bittest op x y-equiv)))
  :rule-classes :congruence)