		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->truth-idx: Access the |TRUTH|::|TRUTH-IDX| field of a npn4 bit structure.
Npn4->polarity: Access the |TRUTH|::|POLARITY| 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.