		Search-engine friendly clone of the ACL2 documentation.

Fp-bitstructs

Mxcsrbits

The MXCSR Control and Status Register.

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

Fields

ie — bit
de — bit
ze — bit
oe — bit
ue — bit
pe — bit
daz — bit
im — bit
dm — bit
zm — bit
om — bit
um — bit
pm — bit
rc — 2bits
ftz — bit
reserved — 16bits

Source: Intel Manual, Dec-23, Vol. 1, Section 10.2.3.

Definitions and Theorems

Function: mxcsrbits-p

(defun mxcsrbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'mxcsrbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 32 x)
         :exec (and (natp x) (< x 4294967296)))))

Theorem: mxcsrbits-p-when-unsigned-byte-p

(defthm mxcsrbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 32 x)
           (mxcsrbits-p x)))

Theorem: unsigned-byte-p-when-mxcsrbits-p

(defthm unsigned-byte-p-when-mxcsrbits-p
  (implies (mxcsrbits-p x)
           (unsigned-byte-p 32 x)))

Theorem: mxcsrbits-p-compound-recognizer

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

Function: mxcsrbits-fix

(defun mxcsrbits-fix (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (let ((__function__ 'mxcsrbits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 32 x) :exec x)))

Theorem: mxcsrbits-p-of-mxcsrbits-fix

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

Theorem: mxcsrbits-fix-when-mxcsrbits-p

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

Function: mxcsrbits-equiv$inline

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

Theorem: mxcsrbits-equiv-is-an-equivalence

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

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

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

Theorem: mxcsrbits-fix-under-mxcsrbits-equiv

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

Function: mxcsrbits

(defun mxcsrbits (ie de ze oe ue pe
                     daz im dm zm om um pm rc ftz reserved)
 (declare (xargs :guard (and (bitp ie)
                             (bitp de)
                             (bitp ze)
                             (bitp oe)
                             (bitp ue)
                             (bitp pe)
                             (bitp daz)
                             (bitp im)
                             (bitp dm)
                             (bitp zm)
                             (bitp om)
                             (bitp um)
                             (bitp pm)
                             (2bits-p rc)
                             (bitp ftz)
                             (16bits-p reserved))))
 (let ((__function__ 'mxcsrbits))
  (declare (ignorable __function__))
  (b* ((ie (mbe :logic (bfix ie) :exec ie))
       (de (mbe :logic (bfix de) :exec de))
       (ze (mbe :logic (bfix ze) :exec ze))
       (oe (mbe :logic (bfix oe) :exec oe))
       (ue (mbe :logic (bfix ue) :exec ue))
       (pe (mbe :logic (bfix pe) :exec pe))
       (daz (mbe :logic (bfix daz) :exec daz))
       (im (mbe :logic (bfix im) :exec im))
       (dm (mbe :logic (bfix dm) :exec dm))
       (zm (mbe :logic (bfix zm) :exec zm))
       (om (mbe :logic (bfix om) :exec om))
       (um (mbe :logic (bfix um) :exec um))
       (pm (mbe :logic (bfix pm) :exec pm))
       (rc (mbe :logic (2bits-fix rc) :exec rc))
       (ftz (mbe :logic (bfix ftz) :exec ftz))
       (reserved (mbe :logic (16bits-fix reserved)
                      :exec reserved)))
   (logapp
    1 ie
    (logapp
     1 de
     (logapp
      1 ze
      (logapp
       1 oe
       (logapp
        1 ue
        (logapp
         1 pe
         (logapp
          1 daz
          (logapp
           1 im
           (logapp
            1 dm
            (logapp
             1 zm
             (logapp
              1 om
              (logapp
               1 um
               (logapp
                    1 pm
                    (logapp 2 rc
                            (logapp 1 ftz reserved))))))))))))))))))

Theorem: mxcsrbits-p-of-mxcsrbits

(defthm mxcsrbits-p-of-mxcsrbits
 (b* ((mxcsrbits (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)))
   (mxcsrbits-p mxcsrbits))
 :rule-classes :rewrite)

Theorem: mxcsrbits-of-bfix-ie

(defthm mxcsrbits-of-bfix-ie
  (equal (mxcsrbits (bfix ie)
                    de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-ie

(defthm mxcsrbits-bit-equiv-congruence-on-ie
 (implies (bit-equiv ie ie-equiv)
          (equal (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)
                 (mxcsrbits ie-equiv de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)))
 :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-de

(defthm mxcsrbits-of-bfix-de
  (equal (mxcsrbits ie (bfix de)
                    ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-de

(defthm mxcsrbits-bit-equiv-congruence-on-de
 (implies (bit-equiv de de-equiv)
          (equal (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)
                 (mxcsrbits ie de-equiv ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)))
 :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-ze

(defthm mxcsrbits-of-bfix-ze
  (equal (mxcsrbits ie de (bfix ze)
                    oe ue pe
                    daz im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-ze

(defthm mxcsrbits-bit-equiv-congruence-on-ze
 (implies (bit-equiv ze ze-equiv)
          (equal (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)
                 (mxcsrbits ie de ze-equiv oe ue pe
                            daz im dm zm om um pm rc ftz reserved)))
 :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-oe

(defthm mxcsrbits-of-bfix-oe
  (equal (mxcsrbits ie de ze (bfix oe)
                    ue pe
                    daz im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-oe

(defthm mxcsrbits-bit-equiv-congruence-on-oe
 (implies (bit-equiv oe oe-equiv)
          (equal (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)
                 (mxcsrbits ie de ze oe-equiv ue pe
                            daz im dm zm om um pm rc ftz reserved)))
 :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-ue

(defthm mxcsrbits-of-bfix-ue
  (equal (mxcsrbits ie de ze oe (bfix ue)
                    pe
                    daz im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-ue

(defthm mxcsrbits-bit-equiv-congruence-on-ue
 (implies (bit-equiv ue ue-equiv)
          (equal (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)
                 (mxcsrbits ie de ze oe ue-equiv pe
                            daz im dm zm om um pm rc ftz reserved)))
 :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-pe

(defthm mxcsrbits-of-bfix-pe
  (equal (mxcsrbits ie de ze oe ue (bfix pe)
                    daz im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-pe

(defthm mxcsrbits-bit-equiv-congruence-on-pe
 (implies (bit-equiv pe pe-equiv)
          (equal (mxcsrbits ie de ze oe ue pe
                            daz im dm zm om um pm rc ftz reserved)
                 (mxcsrbits ie de ze oe ue pe-equiv
                            daz im dm zm om um pm rc ftz reserved)))
 :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-daz

(defthm mxcsrbits-of-bfix-daz
  (equal (mxcsrbits ie de ze oe ue pe (bfix daz)
                    im dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-daz

(defthm mxcsrbits-bit-equiv-congruence-on-daz
  (implies (bit-equiv daz daz-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz-equiv
                             im dm zm om um pm rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-im

(defthm mxcsrbits-of-bfix-im
  (equal (mxcsrbits ie de ze oe ue pe daz (bfix im)
                    dm zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-im

(defthm mxcsrbits-bit-equiv-congruence-on-im
  (implies (bit-equiv im im-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im-equiv
                             dm zm om um pm rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-dm

(defthm mxcsrbits-of-bfix-dm
  (equal (mxcsrbits ie de ze oe ue pe daz im (bfix dm)
                    zm om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-dm

(defthm mxcsrbits-bit-equiv-congruence-on-dm
  (implies (bit-equiv dm dm-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm-equiv zm om um pm rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-zm

(defthm mxcsrbits-of-bfix-zm
  (equal (mxcsrbits ie de ze oe ue pe daz im dm (bfix zm)
                    om um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-zm

(defthm mxcsrbits-bit-equiv-congruence-on-zm
  (implies (bit-equiv zm zm-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm-equiv om um pm rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-om

(defthm mxcsrbits-of-bfix-om
  (equal (mxcsrbits ie de ze oe ue pe daz im dm zm (bfix om)
                    um pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-om

(defthm mxcsrbits-bit-equiv-congruence-on-om
  (implies (bit-equiv om om-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm om-equiv um pm rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-um

(defthm mxcsrbits-of-bfix-um
  (equal (mxcsrbits ie
                    de ze oe ue pe daz im dm zm om (bfix um)
                    pm rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-um

(defthm mxcsrbits-bit-equiv-congruence-on-um
  (implies (bit-equiv um um-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm om um-equiv pm rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-pm

(defthm mxcsrbits-of-bfix-pm
  (equal (mxcsrbits ie de
                    ze oe ue pe daz im dm zm om um (bfix pm)
                    rc ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-pm

(defthm mxcsrbits-bit-equiv-congruence-on-pm
  (implies (bit-equiv pm pm-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm om um pm-equiv rc ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-2bits-fix-rc

(defthm mxcsrbits-of-2bits-fix-rc
  (equal (mxcsrbits ie de ze oe ue
                    pe daz im dm zm om um pm (2bits-fix rc)
                    ftz reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-2bits-equiv-congruence-on-rc

(defthm mxcsrbits-2bits-equiv-congruence-on-rc
  (implies (2bits-equiv rc rc-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm om um pm rc-equiv ftz reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-bfix-ftz

(defthm mxcsrbits-of-bfix-ftz
  (equal (mxcsrbits ie de ze oe ue
                    pe daz im dm zm om um pm rc (bfix ftz)
                    reserved)
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-bit-equiv-congruence-on-ftz

(defthm mxcsrbits-bit-equiv-congruence-on-ftz
  (implies (bit-equiv ftz ftz-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm om um pm rc ftz-equiv reserved)))
  :rule-classes :congruence)

Theorem: mxcsrbits-of-16bits-fix-reserved

(defthm mxcsrbits-of-16bits-fix-reserved
  (equal (mxcsrbits ie de ze oe ue pe daz im dm zm
                    om um pm rc ftz (16bits-fix reserved))
         (mxcsrbits ie de ze oe ue pe
                    daz im dm zm om um pm rc ftz reserved)))

Theorem: mxcsrbits-16bits-equiv-congruence-on-reserved

(defthm mxcsrbits-16bits-equiv-congruence-on-reserved
  (implies (16bits-equiv reserved reserved-equiv)
           (equal (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved)
                  (mxcsrbits ie de ze oe ue pe daz im
                             dm zm om um pm rc ftz reserved-equiv)))
  :rule-classes :congruence)

Function: mxcsrbits-equiv-under-mask

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

Function: mxcsrbits->ie$inline

(defun mxcsrbits->ie$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 0 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 32) x)))))

Theorem: bitp-of-mxcsrbits->ie

(defthm bitp-of-mxcsrbits->ie
  (b* ((ie (mxcsrbits->ie$inline x)))
    (bitp ie))
  :rule-classes :rewrite)

Theorem: mxcsrbits->ie$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->ie$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->ie$inline (mxcsrbits-fix x))
         (mxcsrbits->ie$inline x)))

Theorem: mxcsrbits->ie$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->ie$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->ie$inline x)
                  (mxcsrbits->ie$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->ie-of-mxcsrbits

(defthm mxcsrbits->ie-of-mxcsrbits
 (equal
   (mxcsrbits->ie (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix ie)))

Theorem: mxcsrbits->ie-of-write-with-mask

(defthm mxcsrbits->ie-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 1) 0))
           (equal (mxcsrbits->ie x)
                  (mxcsrbits->ie y))))

Function: mxcsrbits->de$inline

(defun mxcsrbits->de$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 1 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 31)
                            (ash (the (unsigned-byte 32) x) -1))))))

Theorem: bitp-of-mxcsrbits->de

(defthm bitp-of-mxcsrbits->de
  (b* ((de (mxcsrbits->de$inline x)))
    (bitp de))
  :rule-classes :rewrite)

Theorem: mxcsrbits->de$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->de$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->de$inline (mxcsrbits-fix x))
         (mxcsrbits->de$inline x)))

Theorem: mxcsrbits->de$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->de$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->de$inline x)
                  (mxcsrbits->de$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->de-of-mxcsrbits

(defthm mxcsrbits->de-of-mxcsrbits
 (equal
   (mxcsrbits->de (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix de)))

Theorem: mxcsrbits->de-of-write-with-mask

(defthm mxcsrbits->de-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 2) 0))
           (equal (mxcsrbits->de x)
                  (mxcsrbits->de y))))

Function: mxcsrbits->ze$inline

(defun mxcsrbits->ze$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 2 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 30)
                            (ash (the (unsigned-byte 32) x) -2))))))

Theorem: bitp-of-mxcsrbits->ze

(defthm bitp-of-mxcsrbits->ze
  (b* ((ze (mxcsrbits->ze$inline x)))
    (bitp ze))
  :rule-classes :rewrite)

Theorem: mxcsrbits->ze$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->ze$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->ze$inline (mxcsrbits-fix x))
         (mxcsrbits->ze$inline x)))

Theorem: mxcsrbits->ze$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->ze$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->ze$inline x)
                  (mxcsrbits->ze$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->ze-of-mxcsrbits

(defthm mxcsrbits->ze-of-mxcsrbits
 (equal
   (mxcsrbits->ze (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix ze)))

Theorem: mxcsrbits->ze-of-write-with-mask

(defthm mxcsrbits->ze-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4) 0))
           (equal (mxcsrbits->ze x)
                  (mxcsrbits->ze y))))

Function: mxcsrbits->oe$inline

(defun mxcsrbits->oe$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 3 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 29)
                            (ash (the (unsigned-byte 32) x) -3))))))

Theorem: bitp-of-mxcsrbits->oe

(defthm bitp-of-mxcsrbits->oe
  (b* ((oe (mxcsrbits->oe$inline x)))
    (bitp oe))
  :rule-classes :rewrite)

Theorem: mxcsrbits->oe$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->oe$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->oe$inline (mxcsrbits-fix x))
         (mxcsrbits->oe$inline x)))

Theorem: mxcsrbits->oe$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->oe$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->oe$inline x)
                  (mxcsrbits->oe$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->oe-of-mxcsrbits

(defthm mxcsrbits->oe-of-mxcsrbits
 (equal
   (mxcsrbits->oe (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix oe)))

Theorem: mxcsrbits->oe-of-write-with-mask

(defthm mxcsrbits->oe-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 8) 0))
           (equal (mxcsrbits->oe x)
                  (mxcsrbits->oe y))))

Function: mxcsrbits->ue$inline

(defun mxcsrbits->ue$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 4 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 28)
                            (ash (the (unsigned-byte 32) x) -4))))))

Theorem: bitp-of-mxcsrbits->ue

(defthm bitp-of-mxcsrbits->ue
  (b* ((ue (mxcsrbits->ue$inline x)))
    (bitp ue))
  :rule-classes :rewrite)

Theorem: mxcsrbits->ue$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->ue$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->ue$inline (mxcsrbits-fix x))
         (mxcsrbits->ue$inline x)))

Theorem: mxcsrbits->ue$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->ue$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->ue$inline x)
                  (mxcsrbits->ue$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->ue-of-mxcsrbits

(defthm mxcsrbits->ue-of-mxcsrbits
 (equal
   (mxcsrbits->ue (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix ue)))

Theorem: mxcsrbits->ue-of-write-with-mask

(defthm mxcsrbits->ue-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 16)
                       0))
           (equal (mxcsrbits->ue x)
                  (mxcsrbits->ue y))))

Function: mxcsrbits->pe$inline

(defun mxcsrbits->pe$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 5 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 27)
                            (ash (the (unsigned-byte 32) x) -5))))))

Theorem: bitp-of-mxcsrbits->pe

(defthm bitp-of-mxcsrbits->pe
  (b* ((pe (mxcsrbits->pe$inline x)))
    (bitp pe))
  :rule-classes :rewrite)

Theorem: mxcsrbits->pe$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->pe$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->pe$inline (mxcsrbits-fix x))
         (mxcsrbits->pe$inline x)))

Theorem: mxcsrbits->pe$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->pe$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->pe$inline x)
                  (mxcsrbits->pe$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->pe-of-mxcsrbits

(defthm mxcsrbits->pe-of-mxcsrbits
 (equal
   (mxcsrbits->pe (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix pe)))

Theorem: mxcsrbits->pe-of-write-with-mask

(defthm mxcsrbits->pe-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 32)
                       0))
           (equal (mxcsrbits->pe x)
                  (mxcsrbits->pe y))))

Function: mxcsrbits->daz$inline

(defun mxcsrbits->daz$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 6 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 26)
                            (ash (the (unsigned-byte 32) x) -6))))))

Theorem: bitp-of-mxcsrbits->daz

(defthm bitp-of-mxcsrbits->daz
  (b* ((daz (mxcsrbits->daz$inline x)))
    (bitp daz))
  :rule-classes :rewrite)

Theorem: mxcsrbits->daz$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->daz$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->daz$inline (mxcsrbits-fix x))
         (mxcsrbits->daz$inline x)))

Theorem: mxcsrbits->daz$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->daz$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->daz$inline x)
                  (mxcsrbits->daz$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->daz-of-mxcsrbits

(defthm mxcsrbits->daz-of-mxcsrbits
 (equal
  (mxcsrbits->daz (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
  (bfix daz)))

Theorem: mxcsrbits->daz-of-write-with-mask

(defthm mxcsrbits->daz-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 64)
                       0))
           (equal (mxcsrbits->daz x)
                  (mxcsrbits->daz y))))

Function: mxcsrbits->im$inline

(defun mxcsrbits->im$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 7 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 25)
                            (ash (the (unsigned-byte 32) x) -7))))))

Theorem: bitp-of-mxcsrbits->im

(defthm bitp-of-mxcsrbits->im
  (b* ((im (mxcsrbits->im$inline x)))
    (bitp im))
  :rule-classes :rewrite)

Theorem: mxcsrbits->im$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->im$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->im$inline (mxcsrbits-fix x))
         (mxcsrbits->im$inline x)))

Theorem: mxcsrbits->im$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->im$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->im$inline x)
                  (mxcsrbits->im$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->im-of-mxcsrbits

(defthm mxcsrbits->im-of-mxcsrbits
 (equal
   (mxcsrbits->im (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix im)))

Theorem: mxcsrbits->im-of-write-with-mask

(defthm mxcsrbits->im-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 128)
                       0))
           (equal (mxcsrbits->im x)
                  (mxcsrbits->im y))))

Function: mxcsrbits->dm$inline

(defun mxcsrbits->dm$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 8 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 24)
                            (ash (the (unsigned-byte 32) x) -8))))))

Theorem: bitp-of-mxcsrbits->dm

(defthm bitp-of-mxcsrbits->dm
  (b* ((dm (mxcsrbits->dm$inline x)))
    (bitp dm))
  :rule-classes :rewrite)

Theorem: mxcsrbits->dm$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->dm$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->dm$inline (mxcsrbits-fix x))
         (mxcsrbits->dm$inline x)))

Theorem: mxcsrbits->dm$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->dm$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->dm$inline x)
                  (mxcsrbits->dm$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->dm-of-mxcsrbits

(defthm mxcsrbits->dm-of-mxcsrbits
 (equal
   (mxcsrbits->dm (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix dm)))

Theorem: mxcsrbits->dm-of-write-with-mask

(defthm mxcsrbits->dm-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 256)
                       0))
           (equal (mxcsrbits->dm x)
                  (mxcsrbits->dm y))))

Function: mxcsrbits->zm$inline

(defun mxcsrbits->zm$inline (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (mbe
    :logic
    (let ((x (mxcsrbits-fix x)))
      (part-select x :low 9 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 23)
                            (ash (the (unsigned-byte 32) x) -9))))))

Theorem: bitp-of-mxcsrbits->zm

(defthm bitp-of-mxcsrbits->zm
  (b* ((zm (mxcsrbits->zm$inline x)))
    (bitp zm))
  :rule-classes :rewrite)

Theorem: mxcsrbits->zm$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->zm$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->zm$inline (mxcsrbits-fix x))
         (mxcsrbits->zm$inline x)))

Theorem: mxcsrbits->zm$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->zm$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->zm$inline x)
                  (mxcsrbits->zm$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->zm-of-mxcsrbits

(defthm mxcsrbits->zm-of-mxcsrbits
 (equal
   (mxcsrbits->zm (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix zm)))

Theorem: mxcsrbits->zm-of-write-with-mask

(defthm mxcsrbits->zm-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 512)
                       0))
           (equal (mxcsrbits->zm x)
                  (mxcsrbits->zm y))))

Function: mxcsrbits->om$inline

(defun mxcsrbits->om$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 10 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 22)
                               (ash (the (unsigned-byte 32) x)
                                    -10))))))

Theorem: bitp-of-mxcsrbits->om

(defthm bitp-of-mxcsrbits->om
  (b* ((om (mxcsrbits->om$inline x)))
    (bitp om))
  :rule-classes :rewrite)

Theorem: mxcsrbits->om$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->om$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->om$inline (mxcsrbits-fix x))
         (mxcsrbits->om$inline x)))

Theorem: mxcsrbits->om$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->om$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->om$inline x)
                  (mxcsrbits->om$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->om-of-mxcsrbits

(defthm mxcsrbits->om-of-mxcsrbits
 (equal
   (mxcsrbits->om (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix om)))

Theorem: mxcsrbits->om-of-write-with-mask

(defthm mxcsrbits->om-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 1024)
                       0))
           (equal (mxcsrbits->om x)
                  (mxcsrbits->om y))))

Function: mxcsrbits->um$inline

(defun mxcsrbits->um$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 11 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 21)
                               (ash (the (unsigned-byte 32) x)
                                    -11))))))

Theorem: bitp-of-mxcsrbits->um

(defthm bitp-of-mxcsrbits->um
  (b* ((um (mxcsrbits->um$inline x)))
    (bitp um))
  :rule-classes :rewrite)

Theorem: mxcsrbits->um$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->um$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->um$inline (mxcsrbits-fix x))
         (mxcsrbits->um$inline x)))

Theorem: mxcsrbits->um$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->um$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->um$inline x)
                  (mxcsrbits->um$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->um-of-mxcsrbits

(defthm mxcsrbits->um-of-mxcsrbits
 (equal
   (mxcsrbits->um (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix um)))

Theorem: mxcsrbits->um-of-write-with-mask

(defthm mxcsrbits->um-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 2048)
                       0))
           (equal (mxcsrbits->um x)
                  (mxcsrbits->um y))))

Function: mxcsrbits->pm$inline

(defun mxcsrbits->pm$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 12 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 20)
                               (ash (the (unsigned-byte 32) x)
                                    -12))))))

Theorem: bitp-of-mxcsrbits->pm

(defthm bitp-of-mxcsrbits->pm
  (b* ((pm (mxcsrbits->pm$inline x)))
    (bitp pm))
  :rule-classes :rewrite)

Theorem: mxcsrbits->pm$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->pm$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->pm$inline (mxcsrbits-fix x))
         (mxcsrbits->pm$inline x)))

Theorem: mxcsrbits->pm$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->pm$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->pm$inline x)
                  (mxcsrbits->pm$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->pm-of-mxcsrbits

(defthm mxcsrbits->pm-of-mxcsrbits
 (equal
   (mxcsrbits->pm (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (bfix pm)))

Theorem: mxcsrbits->pm-of-write-with-mask

(defthm mxcsrbits->pm-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4096)
                       0))
           (equal (mxcsrbits->pm x)
                  (mxcsrbits->pm y))))

Function: mxcsrbits->rc$inline

(defun mxcsrbits->rc$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 13 :width 2))
       :exec (the (unsigned-byte 2)
                  (logand (the (unsigned-byte 2) 3)
                          (the (unsigned-byte 19)
                               (ash (the (unsigned-byte 32) x)
                                    -13))))))

Theorem: 2bits-p-of-mxcsrbits->rc

(defthm 2bits-p-of-mxcsrbits->rc
  (b* ((rc (mxcsrbits->rc$inline x)))
    (2bits-p rc))
  :rule-classes :rewrite)

Theorem: mxcsrbits->rc$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->rc$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->rc$inline (mxcsrbits-fix x))
         (mxcsrbits->rc$inline x)))

Theorem: mxcsrbits->rc$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->rc$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->rc$inline x)
                  (mxcsrbits->rc$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->rc-of-mxcsrbits

(defthm mxcsrbits->rc-of-mxcsrbits
 (equal
   (mxcsrbits->rc (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
   (2bits-fix rc)))

Theorem: mxcsrbits->rc-of-write-with-mask

(defthm mxcsrbits->rc-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 24576)
                       0))
           (equal (mxcsrbits->rc x)
                  (mxcsrbits->rc y))))

Function: mxcsrbits->ftz$inline

(defun mxcsrbits->ftz$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 15 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 17)
                               (ash (the (unsigned-byte 32) x)
                                    -15))))))

Theorem: bitp-of-mxcsrbits->ftz

(defthm bitp-of-mxcsrbits->ftz
  (b* ((ftz (mxcsrbits->ftz$inline x)))
    (bitp ftz))
  :rule-classes :rewrite)

Theorem: mxcsrbits->ftz$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->ftz$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->ftz$inline (mxcsrbits-fix x))
         (mxcsrbits->ftz$inline x)))

Theorem: mxcsrbits->ftz$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->ftz$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->ftz$inline x)
                  (mxcsrbits->ftz$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->ftz-of-mxcsrbits

(defthm mxcsrbits->ftz-of-mxcsrbits
 (equal
  (mxcsrbits->ftz (mxcsrbits ie de ze oe ue pe
                             daz im dm zm om um pm rc ftz reserved))
  (bfix ftz)))

Theorem: mxcsrbits->ftz-of-write-with-mask

(defthm mxcsrbits->ftz-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 32768)
                       0))
           (equal (mxcsrbits->ftz x)
                  (mxcsrbits->ftz y))))

Function: mxcsrbits->reserved$inline

(defun mxcsrbits->reserved$inline (x)
  (declare (xargs :guard (mxcsrbits-p x)))
  (mbe :logic
       (let ((x (mxcsrbits-fix x)))
         (part-select x :low 16 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 16)
                               (ash (the (unsigned-byte 32) x)
                                    -16))))))

Theorem: 16bits-p-of-mxcsrbits->reserved

(defthm 16bits-p-of-mxcsrbits->reserved
  (b* ((reserved (mxcsrbits->reserved$inline x)))
    (16bits-p reserved))
  :rule-classes :rewrite)

Theorem: mxcsrbits->reserved$inline-of-mxcsrbits-fix-x

(defthm mxcsrbits->reserved$inline-of-mxcsrbits-fix-x
  (equal (mxcsrbits->reserved$inline (mxcsrbits-fix x))
         (mxcsrbits->reserved$inline x)))

Theorem: mxcsrbits->reserved$inline-mxcsrbits-equiv-congruence-on-x

(defthm mxcsrbits->reserved$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (mxcsrbits->reserved$inline x)
                  (mxcsrbits->reserved$inline x-equiv)))
  :rule-classes :congruence)

Theorem: mxcsrbits->reserved-of-mxcsrbits

(defthm mxcsrbits->reserved-of-mxcsrbits
  (equal (mxcsrbits->reserved
              (mxcsrbits ie de ze oe ue pe
                         daz im dm zm om um pm rc ftz reserved))
         (16bits-fix reserved)))

Theorem: mxcsrbits->reserved-of-write-with-mask

(defthm mxcsrbits->reserved-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x mxcsrbits-equiv-under-mask)
                (mxcsrbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4294901760)
                       0))
           (equal (mxcsrbits->reserved x)
                  (mxcsrbits->reserved y))))

Theorem: mxcsrbits-fix-in-terms-of-mxcsrbits

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

Function: !mxcsrbits->ie$inline

(defun !mxcsrbits->ie$inline (ie x)
  (declare (xargs :guard (and (bitp ie) (mxcsrbits-p x))))
  (mbe :logic
       (b* ((ie (mbe :logic (bfix ie) :exec ie))
            (x (mxcsrbits-fix x)))
         (part-install ie x :width 1 :low 0))
       :exec (the (unsigned-byte 32)
                  (logior (the (unsigned-byte 32)
                               (logand (the (unsigned-byte 32) x)
                                       (the (signed-byte 2) -2)))
                          (the (unsigned-byte 1) ie)))))

Theorem: mxcsrbits-p-of-!mxcsrbits->ie

(defthm mxcsrbits-p-of-!mxcsrbits->ie
  (b* ((new-x (!mxcsrbits->ie$inline ie x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->ie$inline-of-bfix-ie

(defthm !mxcsrbits->ie$inline-of-bfix-ie
  (equal (!mxcsrbits->ie$inline (bfix ie) x)
         (!mxcsrbits->ie$inline ie x)))

Theorem: !mxcsrbits->ie$inline-bit-equiv-congruence-on-ie

(defthm !mxcsrbits->ie$inline-bit-equiv-congruence-on-ie
  (implies (bit-equiv ie ie-equiv)
           (equal (!mxcsrbits->ie$inline ie x)
                  (!mxcsrbits->ie$inline ie-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ie$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->ie$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->ie$inline ie (mxcsrbits-fix x))
         (!mxcsrbits->ie$inline ie x)))

Theorem: !mxcsrbits->ie$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->ie$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->ie$inline ie x)
                  (!mxcsrbits->ie$inline ie x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ie-is-mxcsrbits

(defthm !mxcsrbits->ie-is-mxcsrbits
  (equal (!mxcsrbits->ie ie x)
         (change-mxcsrbits x :ie ie)))

Theorem: mxcsrbits->ie-of-!mxcsrbits->ie

(defthm mxcsrbits->ie-of-!mxcsrbits->ie
  (b* ((?new-x (!mxcsrbits->ie$inline ie x)))
    (equal (mxcsrbits->ie new-x)
           (bfix ie))))

Theorem: !mxcsrbits->ie-equiv-under-mask

(defthm !mxcsrbits->ie-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->ie$inline ie x)))
    (mxcsrbits-equiv-under-mask new-x x -2)))

Function: !mxcsrbits->de$inline

(defun !mxcsrbits->de$inline (de x)
 (declare (xargs :guard (and (bitp de) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((de (mbe :logic (bfix de) :exec de))
          (x (mxcsrbits-fix x)))
       (part-install de x :width 1 :low 1))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 3) -3)))
                        (the (unsigned-byte 2)
                             (ash (the (unsigned-byte 1) de) 1))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->de

(defthm mxcsrbits-p-of-!mxcsrbits->de
  (b* ((new-x (!mxcsrbits->de$inline de x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->de$inline-of-bfix-de

(defthm !mxcsrbits->de$inline-of-bfix-de
  (equal (!mxcsrbits->de$inline (bfix de) x)
         (!mxcsrbits->de$inline de x)))

Theorem: !mxcsrbits->de$inline-bit-equiv-congruence-on-de

(defthm !mxcsrbits->de$inline-bit-equiv-congruence-on-de
  (implies (bit-equiv de de-equiv)
           (equal (!mxcsrbits->de$inline de x)
                  (!mxcsrbits->de$inline de-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->de$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->de$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->de$inline de (mxcsrbits-fix x))
         (!mxcsrbits->de$inline de x)))

Theorem: !mxcsrbits->de$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->de$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->de$inline de x)
                  (!mxcsrbits->de$inline de x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->de-is-mxcsrbits

(defthm !mxcsrbits->de-is-mxcsrbits
  (equal (!mxcsrbits->de de x)
         (change-mxcsrbits x :de de)))

Theorem: mxcsrbits->de-of-!mxcsrbits->de

(defthm mxcsrbits->de-of-!mxcsrbits->de
  (b* ((?new-x (!mxcsrbits->de$inline de x)))
    (equal (mxcsrbits->de new-x)
           (bfix de))))

Theorem: !mxcsrbits->de-equiv-under-mask

(defthm !mxcsrbits->de-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->de$inline de x)))
    (mxcsrbits-equiv-under-mask new-x x -3)))

Function: !mxcsrbits->ze$inline

(defun !mxcsrbits->ze$inline (ze x)
 (declare (xargs :guard (and (bitp ze) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((ze (mbe :logic (bfix ze) :exec ze))
          (x (mxcsrbits-fix x)))
       (part-install ze x :width 1 :low 2))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 4) -5)))
                        (the (unsigned-byte 3)
                             (ash (the (unsigned-byte 1) ze) 2))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->ze

(defthm mxcsrbits-p-of-!mxcsrbits->ze
  (b* ((new-x (!mxcsrbits->ze$inline ze x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->ze$inline-of-bfix-ze

(defthm !mxcsrbits->ze$inline-of-bfix-ze
  (equal (!mxcsrbits->ze$inline (bfix ze) x)
         (!mxcsrbits->ze$inline ze x)))

Theorem: !mxcsrbits->ze$inline-bit-equiv-congruence-on-ze

(defthm !mxcsrbits->ze$inline-bit-equiv-congruence-on-ze
  (implies (bit-equiv ze ze-equiv)
           (equal (!mxcsrbits->ze$inline ze x)
                  (!mxcsrbits->ze$inline ze-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ze$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->ze$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->ze$inline ze (mxcsrbits-fix x))
         (!mxcsrbits->ze$inline ze x)))

Theorem: !mxcsrbits->ze$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->ze$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->ze$inline ze x)
                  (!mxcsrbits->ze$inline ze x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ze-is-mxcsrbits

(defthm !mxcsrbits->ze-is-mxcsrbits
  (equal (!mxcsrbits->ze ze x)
         (change-mxcsrbits x :ze ze)))

Theorem: mxcsrbits->ze-of-!mxcsrbits->ze

(defthm mxcsrbits->ze-of-!mxcsrbits->ze
  (b* ((?new-x (!mxcsrbits->ze$inline ze x)))
    (equal (mxcsrbits->ze new-x)
           (bfix ze))))

Theorem: !mxcsrbits->ze-equiv-under-mask

(defthm !mxcsrbits->ze-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->ze$inline ze x)))
    (mxcsrbits-equiv-under-mask new-x x -5)))

Function: !mxcsrbits->oe$inline

(defun !mxcsrbits->oe$inline (oe x)
 (declare (xargs :guard (and (bitp oe) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((oe (mbe :logic (bfix oe) :exec oe))
          (x (mxcsrbits-fix x)))
       (part-install oe x :width 1 :low 3))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 5) -9)))
                        (the (unsigned-byte 4)
                             (ash (the (unsigned-byte 1) oe) 3))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->oe

(defthm mxcsrbits-p-of-!mxcsrbits->oe
  (b* ((new-x (!mxcsrbits->oe$inline oe x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->oe$inline-of-bfix-oe

(defthm !mxcsrbits->oe$inline-of-bfix-oe
  (equal (!mxcsrbits->oe$inline (bfix oe) x)
         (!mxcsrbits->oe$inline oe x)))

Theorem: !mxcsrbits->oe$inline-bit-equiv-congruence-on-oe

(defthm !mxcsrbits->oe$inline-bit-equiv-congruence-on-oe
  (implies (bit-equiv oe oe-equiv)
           (equal (!mxcsrbits->oe$inline oe x)
                  (!mxcsrbits->oe$inline oe-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->oe$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->oe$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->oe$inline oe (mxcsrbits-fix x))
         (!mxcsrbits->oe$inline oe x)))

Theorem: !mxcsrbits->oe$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->oe$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->oe$inline oe x)
                  (!mxcsrbits->oe$inline oe x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->oe-is-mxcsrbits

(defthm !mxcsrbits->oe-is-mxcsrbits
  (equal (!mxcsrbits->oe oe x)
         (change-mxcsrbits x :oe oe)))

Theorem: mxcsrbits->oe-of-!mxcsrbits->oe

(defthm mxcsrbits->oe-of-!mxcsrbits->oe
  (b* ((?new-x (!mxcsrbits->oe$inline oe x)))
    (equal (mxcsrbits->oe new-x)
           (bfix oe))))

Theorem: !mxcsrbits->oe-equiv-under-mask

(defthm !mxcsrbits->oe-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->oe$inline oe x)))
    (mxcsrbits-equiv-under-mask new-x x -9)))

Function: !mxcsrbits->ue$inline

(defun !mxcsrbits->ue$inline (ue x)
 (declare (xargs :guard (and (bitp ue) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((ue (mbe :logic (bfix ue) :exec ue))
          (x (mxcsrbits-fix x)))
       (part-install ue x :width 1 :low 4))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 6) -17)))
                        (the (unsigned-byte 5)
                             (ash (the (unsigned-byte 1) ue) 4))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->ue

(defthm mxcsrbits-p-of-!mxcsrbits->ue
  (b* ((new-x (!mxcsrbits->ue$inline ue x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->ue$inline-of-bfix-ue

(defthm !mxcsrbits->ue$inline-of-bfix-ue
  (equal (!mxcsrbits->ue$inline (bfix ue) x)
         (!mxcsrbits->ue$inline ue x)))

Theorem: !mxcsrbits->ue$inline-bit-equiv-congruence-on-ue

(defthm !mxcsrbits->ue$inline-bit-equiv-congruence-on-ue
  (implies (bit-equiv ue ue-equiv)
           (equal (!mxcsrbits->ue$inline ue x)
                  (!mxcsrbits->ue$inline ue-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ue$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->ue$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->ue$inline ue (mxcsrbits-fix x))
         (!mxcsrbits->ue$inline ue x)))

Theorem: !mxcsrbits->ue$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->ue$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->ue$inline ue x)
                  (!mxcsrbits->ue$inline ue x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ue-is-mxcsrbits

(defthm !mxcsrbits->ue-is-mxcsrbits
  (equal (!mxcsrbits->ue ue x)
         (change-mxcsrbits x :ue ue)))

Theorem: mxcsrbits->ue-of-!mxcsrbits->ue

(defthm mxcsrbits->ue-of-!mxcsrbits->ue
  (b* ((?new-x (!mxcsrbits->ue$inline ue x)))
    (equal (mxcsrbits->ue new-x)
           (bfix ue))))

Theorem: !mxcsrbits->ue-equiv-under-mask

(defthm !mxcsrbits->ue-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->ue$inline ue x)))
    (mxcsrbits-equiv-under-mask new-x x -17)))

Function: !mxcsrbits->pe$inline

(defun !mxcsrbits->pe$inline (pe x)
 (declare (xargs :guard (and (bitp pe) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((pe (mbe :logic (bfix pe) :exec pe))
          (x (mxcsrbits-fix x)))
       (part-install pe x :width 1 :low 5))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 7) -33)))
                        (the (unsigned-byte 6)
                             (ash (the (unsigned-byte 1) pe) 5))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->pe

(defthm mxcsrbits-p-of-!mxcsrbits->pe
  (b* ((new-x (!mxcsrbits->pe$inline pe x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->pe$inline-of-bfix-pe

(defthm !mxcsrbits->pe$inline-of-bfix-pe
  (equal (!mxcsrbits->pe$inline (bfix pe) x)
         (!mxcsrbits->pe$inline pe x)))

Theorem: !mxcsrbits->pe$inline-bit-equiv-congruence-on-pe

(defthm !mxcsrbits->pe$inline-bit-equiv-congruence-on-pe
  (implies (bit-equiv pe pe-equiv)
           (equal (!mxcsrbits->pe$inline pe x)
                  (!mxcsrbits->pe$inline pe-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->pe$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->pe$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->pe$inline pe (mxcsrbits-fix x))
         (!mxcsrbits->pe$inline pe x)))

Theorem: !mxcsrbits->pe$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->pe$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->pe$inline pe x)
                  (!mxcsrbits->pe$inline pe x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->pe-is-mxcsrbits

(defthm !mxcsrbits->pe-is-mxcsrbits
  (equal (!mxcsrbits->pe pe x)
         (change-mxcsrbits x :pe pe)))

Theorem: mxcsrbits->pe-of-!mxcsrbits->pe

(defthm mxcsrbits->pe-of-!mxcsrbits->pe
  (b* ((?new-x (!mxcsrbits->pe$inline pe x)))
    (equal (mxcsrbits->pe new-x)
           (bfix pe))))

Theorem: !mxcsrbits->pe-equiv-under-mask

(defthm !mxcsrbits->pe-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->pe$inline pe x)))
    (mxcsrbits-equiv-under-mask new-x x -33)))

Function: !mxcsrbits->daz$inline

(defun !mxcsrbits->daz$inline (daz x)
 (declare (xargs :guard (and (bitp daz) (mxcsrbits-p x))))
 (mbe
    :logic
    (b* ((daz (mbe :logic (bfix daz) :exec daz))
         (x (mxcsrbits-fix x)))
      (part-install daz x :width 1 :low 6))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 8) -65)))
                       (the (unsigned-byte 7)
                            (ash (the (unsigned-byte 1) daz) 6))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->daz

(defthm mxcsrbits-p-of-!mxcsrbits->daz
  (b* ((new-x (!mxcsrbits->daz$inline daz x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->daz$inline-of-bfix-daz

(defthm !mxcsrbits->daz$inline-of-bfix-daz
  (equal (!mxcsrbits->daz$inline (bfix daz) x)
         (!mxcsrbits->daz$inline daz x)))

Theorem: !mxcsrbits->daz$inline-bit-equiv-congruence-on-daz

(defthm !mxcsrbits->daz$inline-bit-equiv-congruence-on-daz
  (implies (bit-equiv daz daz-equiv)
           (equal (!mxcsrbits->daz$inline daz x)
                  (!mxcsrbits->daz$inline daz-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->daz$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->daz$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->daz$inline daz (mxcsrbits-fix x))
         (!mxcsrbits->daz$inline daz x)))

Theorem: !mxcsrbits->daz$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->daz$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->daz$inline daz x)
                  (!mxcsrbits->daz$inline daz x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->daz-is-mxcsrbits

(defthm !mxcsrbits->daz-is-mxcsrbits
  (equal (!mxcsrbits->daz daz x)
         (change-mxcsrbits x :daz daz)))

Theorem: mxcsrbits->daz-of-!mxcsrbits->daz

(defthm mxcsrbits->daz-of-!mxcsrbits->daz
  (b* ((?new-x (!mxcsrbits->daz$inline daz x)))
    (equal (mxcsrbits->daz new-x)
           (bfix daz))))

Theorem: !mxcsrbits->daz-equiv-under-mask

(defthm !mxcsrbits->daz-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->daz$inline daz x)))
    (mxcsrbits-equiv-under-mask new-x x -65)))

Function: !mxcsrbits->im$inline

(defun !mxcsrbits->im$inline (im x)
 (declare (xargs :guard (and (bitp im) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((im (mbe :logic (bfix im) :exec im))
          (x (mxcsrbits-fix x)))
       (part-install im x :width 1 :low 7))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 9) -129)))
                        (the (unsigned-byte 8)
                             (ash (the (unsigned-byte 1) im) 7))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->im

(defthm mxcsrbits-p-of-!mxcsrbits->im
  (b* ((new-x (!mxcsrbits->im$inline im x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->im$inline-of-bfix-im

(defthm !mxcsrbits->im$inline-of-bfix-im
  (equal (!mxcsrbits->im$inline (bfix im) x)
         (!mxcsrbits->im$inline im x)))

Theorem: !mxcsrbits->im$inline-bit-equiv-congruence-on-im

(defthm !mxcsrbits->im$inline-bit-equiv-congruence-on-im
  (implies (bit-equiv im im-equiv)
           (equal (!mxcsrbits->im$inline im x)
                  (!mxcsrbits->im$inline im-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->im$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->im$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->im$inline im (mxcsrbits-fix x))
         (!mxcsrbits->im$inline im x)))

Theorem: !mxcsrbits->im$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->im$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->im$inline im x)
                  (!mxcsrbits->im$inline im x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->im-is-mxcsrbits

(defthm !mxcsrbits->im-is-mxcsrbits
  (equal (!mxcsrbits->im im x)
         (change-mxcsrbits x :im im)))

Theorem: mxcsrbits->im-of-!mxcsrbits->im

(defthm mxcsrbits->im-of-!mxcsrbits->im
  (b* ((?new-x (!mxcsrbits->im$inline im x)))
    (equal (mxcsrbits->im new-x)
           (bfix im))))

Theorem: !mxcsrbits->im-equiv-under-mask

(defthm !mxcsrbits->im-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->im$inline im x)))
    (mxcsrbits-equiv-under-mask new-x x -129)))

Function: !mxcsrbits->dm$inline

(defun !mxcsrbits->dm$inline (dm x)
 (declare (xargs :guard (and (bitp dm) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((dm (mbe :logic (bfix dm) :exec dm))
          (x (mxcsrbits-fix x)))
       (part-install dm x :width 1 :low 8))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 10) -257)))
                        (the (unsigned-byte 9)
                             (ash (the (unsigned-byte 1) dm) 8))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->dm

(defthm mxcsrbits-p-of-!mxcsrbits->dm
  (b* ((new-x (!mxcsrbits->dm$inline dm x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->dm$inline-of-bfix-dm

(defthm !mxcsrbits->dm$inline-of-bfix-dm
  (equal (!mxcsrbits->dm$inline (bfix dm) x)
         (!mxcsrbits->dm$inline dm x)))

Theorem: !mxcsrbits->dm$inline-bit-equiv-congruence-on-dm

(defthm !mxcsrbits->dm$inline-bit-equiv-congruence-on-dm
  (implies (bit-equiv dm dm-equiv)
           (equal (!mxcsrbits->dm$inline dm x)
                  (!mxcsrbits->dm$inline dm-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->dm$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->dm$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->dm$inline dm (mxcsrbits-fix x))
         (!mxcsrbits->dm$inline dm x)))

Theorem: !mxcsrbits->dm$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->dm$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->dm$inline dm x)
                  (!mxcsrbits->dm$inline dm x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->dm-is-mxcsrbits

(defthm !mxcsrbits->dm-is-mxcsrbits
  (equal (!mxcsrbits->dm dm x)
         (change-mxcsrbits x :dm dm)))

Theorem: mxcsrbits->dm-of-!mxcsrbits->dm

(defthm mxcsrbits->dm-of-!mxcsrbits->dm
  (b* ((?new-x (!mxcsrbits->dm$inline dm x)))
    (equal (mxcsrbits->dm new-x)
           (bfix dm))))

Theorem: !mxcsrbits->dm-equiv-under-mask

(defthm !mxcsrbits->dm-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->dm$inline dm x)))
    (mxcsrbits-equiv-under-mask new-x x -257)))

Function: !mxcsrbits->zm$inline

(defun !mxcsrbits->zm$inline (zm x)
 (declare (xargs :guard (and (bitp zm) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((zm (mbe :logic (bfix zm) :exec zm))
          (x (mxcsrbits-fix x)))
       (part-install zm x :width 1 :low 9))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 11) -513)))
                        (the (unsigned-byte 10)
                             (ash (the (unsigned-byte 1) zm) 9))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->zm

(defthm mxcsrbits-p-of-!mxcsrbits->zm
  (b* ((new-x (!mxcsrbits->zm$inline zm x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->zm$inline-of-bfix-zm

(defthm !mxcsrbits->zm$inline-of-bfix-zm
  (equal (!mxcsrbits->zm$inline (bfix zm) x)
         (!mxcsrbits->zm$inline zm x)))

Theorem: !mxcsrbits->zm$inline-bit-equiv-congruence-on-zm

(defthm !mxcsrbits->zm$inline-bit-equiv-congruence-on-zm
  (implies (bit-equiv zm zm-equiv)
           (equal (!mxcsrbits->zm$inline zm x)
                  (!mxcsrbits->zm$inline zm-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->zm$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->zm$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->zm$inline zm (mxcsrbits-fix x))
         (!mxcsrbits->zm$inline zm x)))

Theorem: !mxcsrbits->zm$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->zm$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->zm$inline zm x)
                  (!mxcsrbits->zm$inline zm x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->zm-is-mxcsrbits

(defthm !mxcsrbits->zm-is-mxcsrbits
  (equal (!mxcsrbits->zm zm x)
         (change-mxcsrbits x :zm zm)))

Theorem: mxcsrbits->zm-of-!mxcsrbits->zm

(defthm mxcsrbits->zm-of-!mxcsrbits->zm
  (b* ((?new-x (!mxcsrbits->zm$inline zm x)))
    (equal (mxcsrbits->zm new-x)
           (bfix zm))))

Theorem: !mxcsrbits->zm-equiv-under-mask

(defthm !mxcsrbits->zm-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->zm$inline zm x)))
    (mxcsrbits-equiv-under-mask new-x x -513)))

Function: !mxcsrbits->om$inline

(defun !mxcsrbits->om$inline (om x)
 (declare (xargs :guard (and (bitp om) (mxcsrbits-p x))))
 (mbe
    :logic
    (b* ((om (mbe :logic (bfix om) :exec om))
         (x (mxcsrbits-fix x)))
      (part-install om x :width 1 :low 10))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 12) -1025)))
                       (the (unsigned-byte 11)
                            (ash (the (unsigned-byte 1) om) 10))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->om

(defthm mxcsrbits-p-of-!mxcsrbits->om
  (b* ((new-x (!mxcsrbits->om$inline om x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->om$inline-of-bfix-om

(defthm !mxcsrbits->om$inline-of-bfix-om
  (equal (!mxcsrbits->om$inline (bfix om) x)
         (!mxcsrbits->om$inline om x)))

Theorem: !mxcsrbits->om$inline-bit-equiv-congruence-on-om

(defthm !mxcsrbits->om$inline-bit-equiv-congruence-on-om
  (implies (bit-equiv om om-equiv)
           (equal (!mxcsrbits->om$inline om x)
                  (!mxcsrbits->om$inline om-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->om$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->om$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->om$inline om (mxcsrbits-fix x))
         (!mxcsrbits->om$inline om x)))

Theorem: !mxcsrbits->om$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->om$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->om$inline om x)
                  (!mxcsrbits->om$inline om x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->om-is-mxcsrbits

(defthm !mxcsrbits->om-is-mxcsrbits
  (equal (!mxcsrbits->om om x)
         (change-mxcsrbits x :om om)))

Theorem: mxcsrbits->om-of-!mxcsrbits->om

(defthm mxcsrbits->om-of-!mxcsrbits->om
  (b* ((?new-x (!mxcsrbits->om$inline om x)))
    (equal (mxcsrbits->om new-x)
           (bfix om))))

Theorem: !mxcsrbits->om-equiv-under-mask

(defthm !mxcsrbits->om-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->om$inline om x)))
    (mxcsrbits-equiv-under-mask new-x x -1025)))

Function: !mxcsrbits->um$inline

(defun !mxcsrbits->um$inline (um x)
 (declare (xargs :guard (and (bitp um) (mxcsrbits-p x))))
 (mbe
    :logic
    (b* ((um (mbe :logic (bfix um) :exec um))
         (x (mxcsrbits-fix x)))
      (part-install um x :width 1 :low 11))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 13) -2049)))
                       (the (unsigned-byte 12)
                            (ash (the (unsigned-byte 1) um) 11))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->um

(defthm mxcsrbits-p-of-!mxcsrbits->um
  (b* ((new-x (!mxcsrbits->um$inline um x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->um$inline-of-bfix-um

(defthm !mxcsrbits->um$inline-of-bfix-um
  (equal (!mxcsrbits->um$inline (bfix um) x)
         (!mxcsrbits->um$inline um x)))

Theorem: !mxcsrbits->um$inline-bit-equiv-congruence-on-um

(defthm !mxcsrbits->um$inline-bit-equiv-congruence-on-um
  (implies (bit-equiv um um-equiv)
           (equal (!mxcsrbits->um$inline um x)
                  (!mxcsrbits->um$inline um-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->um$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->um$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->um$inline um (mxcsrbits-fix x))
         (!mxcsrbits->um$inline um x)))

Theorem: !mxcsrbits->um$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->um$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->um$inline um x)
                  (!mxcsrbits->um$inline um x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->um-is-mxcsrbits

(defthm !mxcsrbits->um-is-mxcsrbits
  (equal (!mxcsrbits->um um x)
         (change-mxcsrbits x :um um)))

Theorem: mxcsrbits->um-of-!mxcsrbits->um

(defthm mxcsrbits->um-of-!mxcsrbits->um
  (b* ((?new-x (!mxcsrbits->um$inline um x)))
    (equal (mxcsrbits->um new-x)
           (bfix um))))

Theorem: !mxcsrbits->um-equiv-under-mask

(defthm !mxcsrbits->um-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->um$inline um x)))
    (mxcsrbits-equiv-under-mask new-x x -2049)))

Function: !mxcsrbits->pm$inline

(defun !mxcsrbits->pm$inline (pm x)
 (declare (xargs :guard (and (bitp pm) (mxcsrbits-p x))))
 (mbe
    :logic
    (b* ((pm (mbe :logic (bfix pm) :exec pm))
         (x (mxcsrbits-fix x)))
      (part-install pm x :width 1 :low 12))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 14) -4097)))
                       (the (unsigned-byte 13)
                            (ash (the (unsigned-byte 1) pm) 12))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->pm

(defthm mxcsrbits-p-of-!mxcsrbits->pm
  (b* ((new-x (!mxcsrbits->pm$inline pm x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->pm$inline-of-bfix-pm

(defthm !mxcsrbits->pm$inline-of-bfix-pm
  (equal (!mxcsrbits->pm$inline (bfix pm) x)
         (!mxcsrbits->pm$inline pm x)))

Theorem: !mxcsrbits->pm$inline-bit-equiv-congruence-on-pm

(defthm !mxcsrbits->pm$inline-bit-equiv-congruence-on-pm
  (implies (bit-equiv pm pm-equiv)
           (equal (!mxcsrbits->pm$inline pm x)
                  (!mxcsrbits->pm$inline pm-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->pm$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->pm$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->pm$inline pm (mxcsrbits-fix x))
         (!mxcsrbits->pm$inline pm x)))

Theorem: !mxcsrbits->pm$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->pm$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->pm$inline pm x)
                  (!mxcsrbits->pm$inline pm x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->pm-is-mxcsrbits

(defthm !mxcsrbits->pm-is-mxcsrbits
  (equal (!mxcsrbits->pm pm x)
         (change-mxcsrbits x :pm pm)))

Theorem: mxcsrbits->pm-of-!mxcsrbits->pm

(defthm mxcsrbits->pm-of-!mxcsrbits->pm
  (b* ((?new-x (!mxcsrbits->pm$inline pm x)))
    (equal (mxcsrbits->pm new-x)
           (bfix pm))))

Theorem: !mxcsrbits->pm-equiv-under-mask

(defthm !mxcsrbits->pm-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->pm$inline pm x)))
    (mxcsrbits-equiv-under-mask new-x x -4097)))

Function: !mxcsrbits->rc$inline

(defun !mxcsrbits->rc$inline (rc x)
 (declare (xargs :guard (and (2bits-p rc) (mxcsrbits-p x))))
 (mbe
    :logic
    (b* ((rc (mbe :logic (2bits-fix rc) :exec rc))
         (x (mxcsrbits-fix x)))
      (part-install rc x :width 2 :low 13))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 16) -24577)))
                       (the (unsigned-byte 15)
                            (ash (the (unsigned-byte 2) rc) 13))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->rc

(defthm mxcsrbits-p-of-!mxcsrbits->rc
  (b* ((new-x (!mxcsrbits->rc$inline rc x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->rc$inline-of-2bits-fix-rc

(defthm !mxcsrbits->rc$inline-of-2bits-fix-rc
  (equal (!mxcsrbits->rc$inline (2bits-fix rc) x)
         (!mxcsrbits->rc$inline rc x)))

Theorem: !mxcsrbits->rc$inline-2bits-equiv-congruence-on-rc

(defthm !mxcsrbits->rc$inline-2bits-equiv-congruence-on-rc
  (implies (2bits-equiv rc rc-equiv)
           (equal (!mxcsrbits->rc$inline rc x)
                  (!mxcsrbits->rc$inline rc-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->rc$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->rc$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->rc$inline rc (mxcsrbits-fix x))
         (!mxcsrbits->rc$inline rc x)))

Theorem: !mxcsrbits->rc$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->rc$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->rc$inline rc x)
                  (!mxcsrbits->rc$inline rc x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->rc-is-mxcsrbits

(defthm !mxcsrbits->rc-is-mxcsrbits
  (equal (!mxcsrbits->rc rc x)
         (change-mxcsrbits x :rc rc)))

Theorem: mxcsrbits->rc-of-!mxcsrbits->rc

(defthm mxcsrbits->rc-of-!mxcsrbits->rc
  (b* ((?new-x (!mxcsrbits->rc$inline rc x)))
    (equal (mxcsrbits->rc new-x)
           (2bits-fix rc))))

Theorem: !mxcsrbits->rc-equiv-under-mask

(defthm !mxcsrbits->rc-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->rc$inline rc x)))
    (mxcsrbits-equiv-under-mask new-x x -24577)))

Function: !mxcsrbits->ftz$inline

(defun !mxcsrbits->ftz$inline (ftz x)
 (declare (xargs :guard (and (bitp ftz) (mxcsrbits-p x))))
 (mbe
     :logic
     (b* ((ftz (mbe :logic (bfix ftz) :exec ftz))
          (x (mxcsrbits-fix x)))
       (part-install ftz x :width 1 :low 15))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 17) -32769)))
                        (the (unsigned-byte 16)
                             (ash (the (unsigned-byte 1) ftz)
                                  15))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->ftz

(defthm mxcsrbits-p-of-!mxcsrbits->ftz
  (b* ((new-x (!mxcsrbits->ftz$inline ftz x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->ftz$inline-of-bfix-ftz

(defthm !mxcsrbits->ftz$inline-of-bfix-ftz
  (equal (!mxcsrbits->ftz$inline (bfix ftz) x)
         (!mxcsrbits->ftz$inline ftz x)))

Theorem: !mxcsrbits->ftz$inline-bit-equiv-congruence-on-ftz

(defthm !mxcsrbits->ftz$inline-bit-equiv-congruence-on-ftz
  (implies (bit-equiv ftz ftz-equiv)
           (equal (!mxcsrbits->ftz$inline ftz x)
                  (!mxcsrbits->ftz$inline ftz-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ftz$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->ftz$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->ftz$inline ftz (mxcsrbits-fix x))
         (!mxcsrbits->ftz$inline ftz x)))

Theorem: !mxcsrbits->ftz$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->ftz$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->ftz$inline ftz x)
                  (!mxcsrbits->ftz$inline ftz x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->ftz-is-mxcsrbits

(defthm !mxcsrbits->ftz-is-mxcsrbits
  (equal (!mxcsrbits->ftz ftz x)
         (change-mxcsrbits x :ftz ftz)))

Theorem: mxcsrbits->ftz-of-!mxcsrbits->ftz

(defthm mxcsrbits->ftz-of-!mxcsrbits->ftz
  (b* ((?new-x (!mxcsrbits->ftz$inline ftz x)))
    (equal (mxcsrbits->ftz new-x)
           (bfix ftz))))

Theorem: !mxcsrbits->ftz-equiv-under-mask

(defthm !mxcsrbits->ftz-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->ftz$inline ftz x)))
    (mxcsrbits-equiv-under-mask new-x x -32769)))

Function: !mxcsrbits->reserved$inline

(defun !mxcsrbits->reserved$inline (reserved x)
 (declare (xargs :guard (and (16bits-p reserved)
                             (mxcsrbits-p x))))
 (mbe :logic
      (b* ((reserved (mbe :logic (16bits-fix reserved)
                          :exec reserved))
           (x (mxcsrbits-fix x)))
        (part-install reserved x
                      :width 16
                      :low 16))
      :exec
      (the (unsigned-byte 32)
           (logior (the (unsigned-byte 32)
                        (logand (the (unsigned-byte 32) x)
                                (the (signed-byte 33) -4294901761)))
                   (the (unsigned-byte 32)
                        (ash (the (unsigned-byte 16) reserved)
                             16))))))

Theorem: mxcsrbits-p-of-!mxcsrbits->reserved

(defthm mxcsrbits-p-of-!mxcsrbits->reserved
  (b* ((new-x (!mxcsrbits->reserved$inline reserved x)))
    (mxcsrbits-p new-x))
  :rule-classes :rewrite)

Theorem: !mxcsrbits->reserved$inline-of-16bits-fix-reserved

(defthm !mxcsrbits->reserved$inline-of-16bits-fix-reserved
  (equal (!mxcsrbits->reserved$inline (16bits-fix reserved)
                                      x)
         (!mxcsrbits->reserved$inline reserved x)))

Theorem: !mxcsrbits->reserved$inline-16bits-equiv-congruence-on-reserved

(defthm
    !mxcsrbits->reserved$inline-16bits-equiv-congruence-on-reserved
  (implies (16bits-equiv reserved reserved-equiv)
           (equal (!mxcsrbits->reserved$inline reserved x)
                  (!mxcsrbits->reserved$inline reserved-equiv x)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->reserved$inline-of-mxcsrbits-fix-x

(defthm !mxcsrbits->reserved$inline-of-mxcsrbits-fix-x
  (equal (!mxcsrbits->reserved$inline reserved (mxcsrbits-fix x))
         (!mxcsrbits->reserved$inline reserved x)))

Theorem: !mxcsrbits->reserved$inline-mxcsrbits-equiv-congruence-on-x

(defthm !mxcsrbits->reserved$inline-mxcsrbits-equiv-congruence-on-x
  (implies (mxcsrbits-equiv x x-equiv)
           (equal (!mxcsrbits->reserved$inline reserved x)
                  (!mxcsrbits->reserved$inline reserved x-equiv)))
  :rule-classes :congruence)

Theorem: !mxcsrbits->reserved-is-mxcsrbits

(defthm !mxcsrbits->reserved-is-mxcsrbits
  (equal (!mxcsrbits->reserved reserved x)
         (change-mxcsrbits x
                           :reserved reserved)))

Theorem: mxcsrbits->reserved-of-!mxcsrbits->reserved

(defthm mxcsrbits->reserved-of-!mxcsrbits->reserved
  (b* ((?new-x (!mxcsrbits->reserved$inline reserved x)))
    (equal (mxcsrbits->reserved new-x)
           (16bits-fix reserved))))

Theorem: !mxcsrbits->reserved-equiv-under-mask

(defthm !mxcsrbits->reserved-equiv-under-mask
  (b* ((?new-x (!mxcsrbits->reserved$inline reserved x)))
    (mxcsrbits-equiv-under-mask new-x x 65535)))

Function: mxcsrbits-debug

(defun mxcsrbits-debug (x)
 (declare (xargs :guard (mxcsrbits-p x)))
 (let ((__function__ 'mxcsrbits-debug))
  (declare (ignorable __function__))
  (b* (((mxcsrbits x)))
   (cons
    (cons 'ie x.ie)
    (cons
     (cons 'de x.de)
     (cons
      (cons 'ze x.ze)
      (cons
       (cons 'oe x.oe)
       (cons
        (cons 'ue x.ue)
        (cons
         (cons 'pe x.pe)
         (cons
          (cons 'daz x.daz)
          (cons
           (cons 'im x.im)
           (cons
            (cons 'dm x.dm)
            (cons
             (cons 'zm x.zm)
             (cons
              (cons 'om x.om)
              (cons
                 (cons 'um x.um)
                 (cons (cons 'pm x.pm)
                       (cons (cons 'rc x.rc)
                             (cons (cons 'ftz x.ftz)
                                   (cons (cons 'reserved x.reserved)
                                         nil)))))))))))))))))))

Subtopics

Mxcsrbits-p: Recognizer for mxcsrbits bit structures.
!mxcsrbits->reserved: Update the |X86ISA|::|RESERVED| field of a mxcsrbits bit structure.
!mxcsrbits->ftz: Update the |X86ISA|::|FTZ| field of a mxcsrbits bit structure.
!mxcsrbits->zm: Update the |X86ISA|::|ZM| field of a mxcsrbits bit structure.
!mxcsrbits->ze: Update the |X86ISA|::|ZE| field of a mxcsrbits bit structure.
!mxcsrbits->um: Update the |X86ISA|::|UM| field of a mxcsrbits bit structure.
!mxcsrbits->ue: Update the |X86ISA|::|UE| field of a mxcsrbits bit structure.
!mxcsrbits->rc: Update the |X86ISA|::|RC| field of a mxcsrbits bit structure.
!mxcsrbits->pm: Update the |X86ISA|::|PM| field of a mxcsrbits bit structure.
!mxcsrbits->pe: Update the |ACL2|::|PE| field of a mxcsrbits bit structure.
!mxcsrbits->om: Update the |X86ISA|::|OM| field of a mxcsrbits bit structure.
!mxcsrbits->oe: Update the |X86ISA|::|OE| field of a mxcsrbits bit structure.
!mxcsrbits->im: Update the |X86ISA|::|IM| field of a mxcsrbits bit structure.
!mxcsrbits->dm: Update the |X86ISA|::|DM| field of a mxcsrbits bit structure.
!mxcsrbits->de: Update the |X86ISA|::|DE| field of a mxcsrbits bit structure.
!mxcsrbits->daz: Update the |X86ISA|::|DAZ| field of a mxcsrbits bit structure.
!mxcsrbits->ie: Update the |X86ISA|::|IE| field of a mxcsrbits bit structure.
Mxcsrbits->reserved: Access the |X86ISA|::|RESERVED| field of a mxcsrbits bit structure.
Mxcsrbits->rc: Access the |X86ISA|::|RC| field of a mxcsrbits bit structure.
Mxcsrbits->ftz: Access the |X86ISA|::|FTZ| field of a mxcsrbits bit structure.
Mxcsrbits-fix: Fixing function for mxcsrbits bit structures.
Mxcsrbits->zm: Access the |X86ISA|::|ZM| field of a mxcsrbits bit structure.
Mxcsrbits->ze: Access the |X86ISA|::|ZE| field of a mxcsrbits bit structure.
Mxcsrbits->um: Access the |X86ISA|::|UM| field of a mxcsrbits bit structure.
Mxcsrbits->ue: Access the |X86ISA|::|UE| field of a mxcsrbits bit structure.
Mxcsrbits->pm: Access the |X86ISA|::|PM| field of a mxcsrbits bit structure.
Mxcsrbits->pe: Access the |ACL2|::|PE| field of a mxcsrbits bit structure.
Mxcsrbits->om: Access the |X86ISA|::|OM| field of a mxcsrbits bit structure.
Mxcsrbits->oe: Access the |X86ISA|::|OE| field of a mxcsrbits bit structure.
Mxcsrbits->im: Access the |X86ISA|::|IM| field of a mxcsrbits bit structure.
Mxcsrbits->ie: Access the |X86ISA|::|IE| field of a mxcsrbits bit structure.
Mxcsrbits->dm: Access the |X86ISA|::|DM| field of a mxcsrbits bit structure.
Mxcsrbits->de: Access the |X86ISA|::|DE| field of a mxcsrbits bit structure.
Mxcsrbits->daz: Access the |X86ISA|::|DAZ| field of a mxcsrbits bit structure.