		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Npn4

An 27-bit unsigned bitstruct type.

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 27-bit integer.

Fields

truth-idx — truth-idx: normal-form truth table
negate — bit
polarity — polarity4
perm — perm4

Definitions and Theorems

Function: npn4-p

(defun npn4-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'npn4-p))
    (declare (ignorable __function__))
    (and (mbe :logic (unsigned-byte-p 27 x)
              :exec (and (natp x) (< x 134217728)))
         (perm4p (part-select x :low 21 :width 6)))))

Theorem: unsigned-byte-p-when-npn4-p

(defthm unsigned-byte-p-when-npn4-p
  (implies (npn4-p x)
           (unsigned-byte-p 27 x)))

Theorem: npn4-p-compound-recognizer

(defthm npn4-p-compound-recognizer
  (implies (npn4-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: npn4-fix

(defun npn4-fix (x)
 (declare (xargs :guard (npn4-p x)))
 (let ((__function__ 'npn4-fix))
  (declare (ignorable __function__))
  (mbe
   :logic
   (loghead
    27
    (logapp
       16 (part-select x :width 16 :low 0)
       (logapp
            1 (part-select x :width 1 :low 16)
            (logapp 4 (part-select x :width 4 :low 17)
                    (perm4-fix (part-select x :width 6 :low 21))))))
   :exec x)))

Theorem: npn4-p-of-npn4-fix

(defthm npn4-p-of-npn4-fix
  (b* ((fty::fixed (npn4-fix x)))
    (npn4-p fty::fixed))
  :rule-classes :rewrite)

Theorem: npn4-fix-when-npn4-p

(defthm npn4-fix-when-npn4-p
  (implies (npn4-p x)
           (equal (npn4-fix x) x)))

Function: npn4-equiv$inline

(defun npn4-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (npn4-p acl2::x)
                              (npn4-p acl2::y))))
  (equal (npn4-fix acl2::x)
         (npn4-fix acl2::y)))

Theorem: npn4-equiv-is-an-equivalence

(defthm npn4-equiv-is-an-equivalence
  (and (booleanp (npn4-equiv x y))
       (npn4-equiv x x)
       (implies (npn4-equiv x y)
                (npn4-equiv y x))
       (implies (and (npn4-equiv x y) (npn4-equiv y z))
                (npn4-equiv x z)))
  :rule-classes (:equivalence))

Theorem: npn4-equiv-implies-equal-npn4-fix-1

(defthm npn4-equiv-implies-equal-npn4-fix-1
  (implies (npn4-equiv acl2::x x-equiv)
           (equal (npn4-fix acl2::x)
                  (npn4-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: npn4-fix-under-npn4-equiv

(defthm npn4-fix-under-npn4-equiv
  (npn4-equiv (npn4-fix acl2::x) acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: npn4-fix-of-npn4-fix-x

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

Theorem: npn4-fix-npn4-equiv-congruence-on-x

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

Function: npn4

(defun npn4 (truth-idx negate polarity perm)
  (declare (xargs :guard (and (truth-idx-p truth-idx)
                              (bitp negate)
                              (polarity4-p polarity)
                              (perm4p perm))))
  (let ((__function__ 'npn4))
    (declare (ignorable __function__))
    (b* ((truth-idx (mbe :logic (truth-idx-fix truth-idx)
                         :exec truth-idx))
         (negate (mbe :logic (bfix negate) :exec negate))
         (polarity (mbe :logic (polarity4-fix polarity)
                        :exec polarity))
         (perm (mbe :logic (perm4-fix perm)
                    :exec perm)))
      (logapp 16 truth-idx
              (logapp 1 negate (logapp 4 polarity perm))))))

Theorem: npn4-p-of-npn4

(defthm npn4-p-of-npn4
  (b* ((npn4 (npn4 truth-idx negate polarity perm)))
    (npn4-p npn4))
  :rule-classes :rewrite)

Theorem: npn4-of-truth-idx-fix-truth-idx

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

Theorem: npn4-truth-idx-equiv-congruence-on-truth-idx

(defthm npn4-truth-idx-equiv-congruence-on-truth-idx
  (implies (truth-idx-equiv truth-idx truth-idx-equiv)
           (equal (npn4 truth-idx negate polarity perm)
                  (npn4 truth-idx-equiv negate polarity perm)))
  :rule-classes :congruence)

Theorem: npn4-of-bfix-negate

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

Theorem: npn4-bit-equiv-congruence-on-negate

(defthm npn4-bit-equiv-congruence-on-negate
  (implies (bit-equiv negate negate-equiv)
           (equal (npn4 truth-idx negate polarity perm)
                  (npn4 truth-idx negate-equiv polarity perm)))
  :rule-classes :congruence)

Theorem: npn4-of-polarity4-fix-polarity

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

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

(defthm npn4-polarity4-equiv-congruence-on-polarity
  (implies (polarity4-equiv polarity polarity-equiv)
           (equal (npn4 truth-idx negate polarity perm)
                  (npn4 truth-idx negate polarity-equiv perm)))
  :rule-classes :congruence)

Theorem: npn4-of-perm4-fix-perm

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

Theorem: npn4-perm4-equiv-congruence-on-perm

(defthm npn4-perm4-equiv-congruence-on-perm
  (implies (perm4-equiv perm perm-equiv)
           (equal (npn4 truth-idx negate polarity perm)
                  (npn4 truth-idx negate polarity perm-equiv)))
  :rule-classes :congruence)

Function: npn4-equiv-under-mask

(defun npn4-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (npn4-p x)
                              (npn4-p x1)
                              (integerp mask))))
  (let ((__function__ 'npn4-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (npn4-fix x)
                               (npn4-fix x1)
                               mask)))

Theorem: npn4-equiv-under-mask-of-npn4-fix-x

(defthm npn4-equiv-under-mask-of-npn4-fix-x
  (equal (npn4-equiv-under-mask (npn4-fix x)
                                x1 mask)
         (npn4-equiv-under-mask x x1 mask)))

Theorem: npn4-equiv-under-mask-npn4-equiv-congruence-on-x

(defthm npn4-equiv-under-mask-npn4-equiv-congruence-on-x
  (implies (npn4-equiv x x-equiv)
           (equal (npn4-equiv-under-mask x x1 mask)
                  (npn4-equiv-under-mask x-equiv x1 mask)))
  :rule-classes :congruence)

Theorem: npn4-equiv-under-mask-of-npn4-fix-x1

(defthm npn4-equiv-under-mask-of-npn4-fix-x1
  (equal (npn4-equiv-under-mask x (npn4-fix x1)
                                mask)
         (npn4-equiv-under-mask x x1 mask)))

Theorem: npn4-equiv-under-mask-npn4-equiv-congruence-on-x1

(defthm npn4-equiv-under-mask-npn4-equiv-congruence-on-x1
  (implies (npn4-equiv x1 x1-equiv)
           (equal (npn4-equiv-under-mask x x1 mask)
                  (npn4-equiv-under-mask x x1-equiv mask)))
  :rule-classes :congruence)

Theorem: npn4-equiv-under-mask-of-ifix-mask

(defthm npn4-equiv-under-mask-of-ifix-mask
  (equal (npn4-equiv-under-mask x x1 (ifix mask))
         (npn4-equiv-under-mask x x1 mask)))

Theorem: npn4-equiv-under-mask-int-equiv-congruence-on-mask

(defthm npn4-equiv-under-mask-int-equiv-congruence-on-mask
  (implies (int-equiv mask mask-equiv)
           (equal (npn4-equiv-under-mask x x1 mask)
                  (npn4-equiv-under-mask x x1 mask-equiv)))
  :rule-classes :congruence)

Function: npn4->truth-idx

(defun npn4->truth-idx (x)
  (declare (xargs :guard (npn4-p x)))
  (mbe :logic
       (let ((x (npn4-fix x)))
         (part-select x :low 0 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 27) x)))))

Theorem: truth-idx-p-of-npn4->truth-idx

(defthm truth-idx-p-of-npn4->truth-idx
  (b* ((truth-idx (npn4->truth-idx x)))
    (truth-idx-p truth-idx))
  :rule-classes :rewrite)

Theorem: npn4->truth-idx-of-npn4-fix-x

(defthm npn4->truth-idx-of-npn4-fix-x
  (equal (npn4->truth-idx (npn4-fix x))
         (npn4->truth-idx x)))

Theorem: npn4->truth-idx-npn4-equiv-congruence-on-x

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

Theorem: npn4->truth-idx-of-npn4

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

Theorem: npn4->truth-idx-of-write-with-mask

(defthm npn4->truth-idx-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) 65535)
              0))
  (equal (npn4->truth-idx x)
         (npn4->truth-idx acl2::y))))

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))))

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))))

Function: npn4->perm

(defun npn4->perm (x)
  (declare (xargs :guard (npn4-p x)))
  (mbe :logic
       (let ((x (npn4-fix x)))
         (part-select x :low 21 :width 6))
       :exec (the (unsigned-byte 6)
                  (logand (the (unsigned-byte 6) 63)
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 27) x)
                                    -21))))))

Theorem: perm4p-of-npn4->perm

(defthm perm4p-of-npn4->perm
  (b* ((perm (npn4->perm x)))
    (perm4p perm))
  :rule-classes :rewrite)

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

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

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

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

Theorem: npn4->perm-of-npn4

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

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

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

Theorem: npn4-fix-in-terms-of-npn4

(defthm npn4-fix-in-terms-of-npn4
  (equal (npn4-fix x) (change-npn4 x)))

Function: !npn4->truth-idx

(defun !npn4->truth-idx (truth-idx x)
 (declare (xargs :guard (and (truth-idx-p truth-idx)
                             (npn4-p x))))
 (mbe
     :logic
     (b* ((truth-idx (mbe :logic (truth-idx-fix truth-idx)
                          :exec truth-idx))
          (x (npn4-fix x)))
       (part-install truth-idx x
                     :width 16
                     :low 0))
     :exec (the (unsigned-byte 27)
                (logior (the (unsigned-byte 27)
                             (logand (the (unsigned-byte 27) x)
                                     (the (signed-byte 17) -65536)))
                        (the (unsigned-byte 16) truth-idx)))))

Theorem: npn4-p-of-!npn4->truth-idx

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

Theorem: !npn4->truth-idx-of-truth-idx-fix-truth-idx

(defthm !npn4->truth-idx-of-truth-idx-fix-truth-idx
  (equal (!npn4->truth-idx (truth-idx-fix truth-idx)
                           x)
         (!npn4->truth-idx truth-idx x)))

Theorem: !npn4->truth-idx-truth-idx-equiv-congruence-on-truth-idx

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

Theorem: !npn4->truth-idx-of-npn4-fix-x

(defthm !npn4->truth-idx-of-npn4-fix-x
  (equal (!npn4->truth-idx truth-idx (npn4-fix x))
         (!npn4->truth-idx truth-idx x)))

Theorem: !npn4->truth-idx-npn4-equiv-congruence-on-x

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

Theorem: !npn4->truth-idx-is-npn4

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

Theorem: npn4->truth-idx-of-!npn4->truth-idx

(defthm npn4->truth-idx-of-!npn4->truth-idx
  (b* ((?new-x (!npn4->truth-idx truth-idx x)))
    (equal (npn4->truth-idx new-x)
           (truth-idx-fix truth-idx))))

Theorem: !npn4->truth-idx-equiv-under-mask

(defthm !npn4->truth-idx-equiv-under-mask
  (b* ((?new-x (!npn4->truth-idx truth-idx x)))
    (npn4-equiv-under-mask new-x x -65536)))

Function: !npn4->negate

(defun !npn4->negate (negate x)
 (declare (xargs :guard (and (bitp negate) (npn4-p x))))
 (mbe
     :logic
     (b* ((negate (mbe :logic (bfix negate) :exec negate))
          (x (npn4-fix x)))
       (part-install negate x
                     :width 1
                     :low 16))
     :exec (the (unsigned-byte 27)
                (logior (the (unsigned-byte 27)
                             (logand (the (unsigned-byte 27) x)
                                     (the (signed-byte 18) -65537)))
                        (the (unsigned-byte 17)
                             (ash (the (unsigned-byte 1) negate)
                                  16))))))

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

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

Theorem: !npn4->negate-of-bfix-negate

(defthm !npn4->negate-of-bfix-negate
  (equal (!npn4->negate (bfix negate) x)
         (!npn4->negate negate x)))

Theorem: !npn4->negate-bit-equiv-congruence-on-negate

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

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

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

Theorem: !npn4->negate-is-npn4

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

Theorem: npn4->negate-of-!npn4->negate

(defthm npn4->negate-of-!npn4->negate
  (b* ((?new-x (!npn4->negate negate x)))
    (equal (npn4->negate new-x)
           (bfix negate))))

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

(defthm !npn4->negate-equiv-under-mask
  (b* ((?new-x (!npn4->negate negate x)))
    (npn4-equiv-under-mask new-x x -65537)))

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)))

Function: !npn4->perm

(defun !npn4->perm (perm x)
  (declare (xargs :guard (and (perm4p perm) (npn4-p x))))
  (mbe :logic
       (b* ((perm (mbe :logic (perm4-fix perm)
                       :exec perm))
            (x (npn4-fix x)))
         (part-install perm x :width 6 :low 21))
       :exec
       (the (unsigned-byte 27)
            (logior (the (unsigned-byte 27)
                         (logand (the (unsigned-byte 27) x)
                                 (the (signed-byte 28) -132120577)))
                    (the (unsigned-byte 27)
                         (ash (the (unsigned-byte 6) perm)
                              21))))))

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

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

Theorem: !npn4->perm-of-perm4-fix-perm

(defthm !npn4->perm-of-perm4-fix-perm
  (equal (!npn4->perm (perm4-fix perm) x)
         (!npn4->perm perm x)))

Theorem: !npn4->perm-perm4-equiv-congruence-on-perm

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

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

(defthm !npn4->perm-of-npn4-fix-x
  (equal (!npn4->perm perm (npn4-fix x))
         (!npn4->perm perm x)))

Theorem: !npn4->perm-npn4-equiv-congruence-on-x

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

Theorem: !npn4->perm-is-npn4

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

Theorem: npn4->perm-of-!npn4->perm

(defthm npn4->perm-of-!npn4->perm
  (b* ((?new-x (!npn4->perm perm x)))
    (equal (npn4->perm new-x)
           (perm4-fix perm))))

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

(defthm !npn4->perm-equiv-under-mask
  (b* ((?new-x (!npn4->perm perm x)))
    (npn4-equiv-under-mask new-x x 2097151)))

Function: npn4-debug

(defun npn4-debug (x)
  (declare (xargs :guard (npn4-p x)))
  (let ((__function__ 'npn4-debug))
    (declare (ignorable __function__))
    (b* (((npn4 x)))
      (cons (cons 'truth-idx x.truth-idx)
            (cons (cons 'negate x.negate)
                  (cons (cons 'polarity x.polarity)
                        (cons (cons 'perm x.perm) nil)))))))

Theorem: npn4-debug-of-npn4-fix-x

(defthm npn4-debug-of-npn4-fix-x
  (equal (npn4-debug (npn4-fix x))
         (npn4-debug x)))

Theorem: npn4-debug-npn4-equiv-congruence-on-x

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

Subtopics

!npn4->truth-idx: Update the |TRUTH|::|TRUTH-IDX| field of a npn4 bit structure.
!npn4->polarity: Update the |TRUTH|::|POLARITY| field of a npn4 bit structure.
!npn4->negate: Update the |TRUTH|::|NEGATE| field of a npn4 bit structure.
!npn4->perm: Update the |TRUTH|::|PERM| field of a npn4 bit structure.
Npn4-fix: Fixing function for npn4 bit structures.
Npn4->polarity: Access the |TRUTH|::|POLARITY| field of a npn4 bit structure.
Npn4->truth-idx: Access the |TRUTH|::|TRUTH-IDX| field of a npn4 bit structure.
Npn4->negate: Access the |TRUTH|::|NEGATE| field of a npn4 bit structure.
Npn4-p: Recognizer for npn4 bit structures.
Npn4->perm: Access the |TRUTH|::|PERM| field of a npn4 bit structure.