		Search-engine friendly clone of the ACL2 documentation.

Npn4

!npn4->polarity

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

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

Definitions and Theorems

Function: !npn4->polarity

(defun !npn4->polarity (polarity x)
 (declare (xargs :guard (and (polarity4-p polarity)
                             (npn4-p x))))
 (mbe
   :logic
   (b* ((polarity (mbe :logic (polarity4-fix polarity)
                       :exec polarity))
        (x (npn4-fix x)))
     (part-install polarity x
                   :width 4
                   :low 17))
   :exec (the (unsigned-byte 27)
              (logior (the (unsigned-byte 27)
                           (logand (the (unsigned-byte 27) x)
                                   (the (signed-byte 22) -1966081)))
                      (the (unsigned-byte 21)
                           (ash (the (unsigned-byte 4) polarity)
                                17))))))

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

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

Theorem: !npn4->polarity-of-polarity4-fix-polarity

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

Theorem: !npn4->polarity-polarity4-equiv-congruence-on-polarity

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

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

(defthm !npn4->polarity-of-npn4-fix-x
  (equal (!npn4->polarity polarity (npn4-fix x))
         (!npn4->polarity 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 polarity x)
                  (!npn4->polarity polarity x-equiv)))
  :rule-classes :congruence)

Theorem: !npn4->polarity-is-npn4

(defthm !npn4->polarity-is-npn4
  (equal (!npn4->polarity polarity x)
         (change-npn4 x :polarity polarity)))

Theorem: npn4->polarity-of-!npn4->polarity

(defthm npn4->polarity-of-!npn4->polarity
  (b* ((?new-x (!npn4->polarity polarity x)))
    (equal (npn4->polarity new-x)
           (polarity4-fix polarity))))

Theorem: !npn4->polarity-equiv-under-mask

(defthm !npn4->polarity-equiv-under-mask
  (b* ((?new-x (!npn4->polarity polarity x)))
    (npn4-equiv-under-mask new-x x -1966081)))