		Search-engine friendly clone of the ACL2 documentation.

Bitops/extra-defs

Negate-slice8

(negate-slice8 x) computes the 8-bit two's complement negation of x and returns it as an 8-bit natural.

Signature
(negate-slice8 x) → ~x
Returns: ~x — Type (natp ~x).

For example, (negate-slice8 3) = 253.

We leave this enabled; we would usually not expect to try to reason about it.

Definitions and Theorems

Function: negate-slice8$inline

(defun acl2::negate-slice8$inline (x)
 (declare (type (unsigned-byte 8) x))
 (let ((__function__ 'negate-slice8))
  (declare (ignorable __function__))
  (mbe
     :logic (logand (+ 1 (lognot (nfix x)))
                    (1- (expt 2 8)))
     :exec (the (unsigned-byte 8)
                (logand (the (signed-byte 9)
                             (+ 1 (the (signed-byte 9) (lognot x))))
                        255)))))

Theorem: natp-of-negate-slice8

(defthm acl2::natp-of-negate-slice8
  (b* ((~x (acl2::negate-slice8$inline x)))
    (natp ~x))
  :rule-classes :type-prescription)

Theorem: nat-equiv-implies-equal-negate-slice8-1

(defthm nat-equiv-implies-equal-negate-slice8-1
  (implies (nat-equiv x x-equiv)
           (equal (negate-slice8 x)
                  (negate-slice8 x-equiv)))
  :rule-classes (:congruence))

Theorem: unsigned-byte-p-8-of-negate-slice8

(defthm unsigned-byte-p-8-of-negate-slice8
  (unsigned-byte-p 8 (negate-slice8 x)))