		Search-engine friendly clone of the ACL2 documentation.

Npn4

Npn4->polarity

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

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

Definitions and Theorems

Function: npn4->polarity

(defun npn4->polarity (x)
  (declare (xargs :guard (npn4-p x)))
  (mbe :logic
       (let ((x (npn4-fix x)))
         (part-select x :low 17 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 10)
                               (ash (the (unsigned-byte 27) x)
                                    -17))))))

Theorem: polarity4-p-of-npn4->polarity

(defthm polarity4-p-of-npn4->polarity
  (b* ((polarity (npn4->polarity x)))
    (polarity4-p polarity))
  :rule-classes :rewrite)

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

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

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

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

Theorem: npn4->polarity-of-npn4

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

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

(defthm npn4->polarity-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) 1966080)
              0))
  (equal (npn4->polarity x)
         (npn4->polarity acl2::y))))