		Search-engine friendly clone of the ACL2 documentation.

Npn4

Npn4->negate

Access the |TRUTH|::|NEGATE| field of a npn4 bit structure.

Signature
(npn4->negate x) → negate
Arguments: x — Guard (npn4-p x).
Returns: negate — Type (bitp negate).

Definitions and Theorems

Function: npn4->negate

(defun npn4->negate (x)
  (declare (xargs :guard (npn4-p x)))
  (mbe :logic
       (let ((x (npn4-fix x)))
         (part-select x :low 16 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 11)
                               (ash (the (unsigned-byte 27) x)
                                    -16))))))

Theorem: bitp-of-npn4->negate

(defthm bitp-of-npn4->negate
  (b* ((negate (npn4->negate x)))
    (bitp negate))
  :rule-classes :rewrite)

Theorem: npn4->negate-of-npn4-fix-x

(defthm npn4->negate-of-npn4-fix-x
  (equal (npn4->negate (npn4-fix x))
         (npn4->negate x)))

Theorem: npn4->negate-npn4-equiv-congruence-on-x

(defthm npn4->negate-npn4-equiv-congruence-on-x
  (implies (npn4-equiv x x-equiv)
           (equal (npn4->negate x)
                  (npn4->negate x-equiv)))
  :rule-classes :congruence)

Theorem: npn4->negate-of-npn4

(defthm npn4->negate-of-npn4
  (equal (npn4->negate (npn4 truth-idx negate polarity perm))
         (bfix negate)))

Theorem: npn4->negate-of-write-with-mask

(defthm npn4->negate-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps x npn4-equiv-under-mask)
       (npn4-equiv-under-mask x acl2::y fty::mask)
       (equal (logand (lognot fty::mask) 65536)
              0))
  (equal (npn4->negate x)
         (npn4->negate acl2::y))))