• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
        • Structures
          • Rflagsbits
          • Cr4bits
          • Xcr0bits
          • Cr0bits
          • Prefixes
          • Ia32_eferbits
          • Evex-byte1
          • Cr3bits
          • Evex-byte3
          • Vex3-byte2
          • Vex3-byte1
          • Vex2-byte1
          • Evex-prefixes
          • Evex-byte2
          • Vex-prefixes
          • Sib
          • Modr/m-structures
          • Vex-prefixes-layout-structures
          • Sib-structures
          • Legacy-prefixes-layout-structure
          • Evex-prefixes-layout-structures
          • Cr8bits
          • Opcode-maps-structures
          • Segmentation-bitstructs
          • 8bits
          • 2bits
          • 4bits
          • 16bits
          • Paging-bitstructs
          • 3bits
          • 11bits
          • 40bits
          • 5bits
          • 32bits
          • 19bits
          • 10bits
          • 7bits
          • 64bits
          • 54bits
          • 45bits
          • 36bits
          • 31bits
          • 24bits
          • 22bits
          • 17bits
          • 13bits
          • 12bits
          • 6bits
          • Vex->x
          • Vex->b
          • Vex-prefixes-map-p
          • Vex-prefixes-byte0-p
          • Vex->w
          • Vex->vvvv
          • Vex->r
          • Fp-bitstructs
            • Mxcsrbits
            • Fp-statusbits
              • Fp-statusbits-p
              • !fp-statusbits->top
              • !fp-statusbits->ze
              • !fp-statusbits->ue
              • !fp-statusbits->sf
              • !fp-statusbits->pe
              • !fp-statusbits->oe
              • !fp-statusbits->ie
              • !fp-statusbits->es
              • !fp-statusbits->de
              • !fp-statusbits->c3
              • !fp-statusbits->c2
              • !fp-statusbits->c1
              • !fp-statusbits->c0
              • !fp-statusbits->b
              • Fp-statusbits->top
              • Fp-statusbits-fix
              • Fp-statusbits->ze
              • Fp-statusbits->ue
              • Fp-statusbits->sf
              • Fp-statusbits->pe
              • Fp-statusbits->oe
              • Fp-statusbits->es
              • Fp-statusbits->de
              • Fp-statusbits->c3
              • Fp-statusbits->c2
              • Fp-statusbits->c1
              • Fp-statusbits->c0
              • Fp-statusbits->b
              • Fp-statusbits->ie
            • Mxcsrbits-debug
            • Mxcsrbits-equiv-under-mask
            • Fp-statusbits-equiv-under-mask
            • Fp-statusbits-debug
          • Cr4bits-debug
          • Vex->pp
          • Vex->l
          • Rflagsbits-debug
          • Evex->v-prime
          • Evex->z
          • Evex->w
          • Evex->vvvv
          • Evex->vl/rc
          • Evex->pp
          • Evex->aaa
          • Xcr0bits-debug
          • Vex3-byte1-equiv-under-mask
          • Vex3-byte2-equiv-under-mask
          • Vex2-byte1-equiv-under-mask
          • Vex-prefixes-equiv-under-mask
          • Rflagsbits-equiv-under-mask
          • Ia32_eferbits-equiv-under-mask
          • Evex-prefixes-equiv-under-mask
          • Evex-byte3-equiv-under-mask
          • Evex-byte2-equiv-under-mask
          • Evex-byte1-equiv-under-mask
          • Cr0bits-debug
          • Xcr0bits-equiv-under-mask
          • Sib-equiv-under-mask
          • Prefixes-equiv-under-mask
          • Cr8bits-equiv-under-mask
          • Cr4bits-equiv-under-mask
          • Cr3bits-equiv-under-mask
          • Cr0bits-equiv-under-mask
          • Vex3-byte1-debug
          • Prefixes-debug
          • Ia32_eferbits-debug
          • Evex-byte1-debug
          • Vex3-byte2-debug
          • Vex2-byte1-debug
          • Vex-prefixes-debug
          • Evex-prefixes-debug
          • Evex-byte3-debug
          • Evex-byte2-debug
          • Cr3bits-debug
          • Sib-debug
          • Cr8bits-debug
        • Utilities
      • Debugging-code-proofs
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Fp-bitstructs

Fp-statusbits

The x87 FPU Status Register.

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

Fields

ie — bit

de — bit

ze — bit

oe — bit

ue — bit

pe — bit

sf — bit

es — bit

c0 — bit

c1 — bit

c2 — bit

top — 3bits

c3 — bit

b — bit

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

Definitions and Theorems

Function: fp-statusbits-p

(defun fp-statusbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'fp-statusbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 16 x)
         :exec (and (natp x) (< x 65536)))))

Theorem: fp-statusbits-p-when-unsigned-byte-p

(defthm fp-statusbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 16 x)
           (fp-statusbits-p x)))

Theorem: unsigned-byte-p-when-fp-statusbits-p

(defthm unsigned-byte-p-when-fp-statusbits-p
  (implies (fp-statusbits-p x)
           (unsigned-byte-p 16 x)))

Theorem: fp-statusbits-p-compound-recognizer

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

Function: fp-statusbits-fix

(defun fp-statusbits-fix (x)
  (declare (xargs :guard (fp-statusbits-p x)))
  (let ((__function__ 'fp-statusbits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 16 x) :exec x)))

Theorem: fp-statusbits-p-of-fp-statusbits-fix

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

Theorem: fp-statusbits-fix-when-fp-statusbits-p

(defthm fp-statusbits-fix-when-fp-statusbits-p
  (implies (fp-statusbits-p x)
           (equal (fp-statusbits-fix x) x)))

Function: fp-statusbits-equiv$inline

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

Theorem: fp-statusbits-equiv-is-an-equivalence

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

Theorem: fp-statusbits-equiv-implies-equal-fp-statusbits-fix-1

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

Theorem: fp-statusbits-fix-under-fp-statusbits-equiv

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

Function: fp-statusbits

(defun fp-statusbits (ie de ze oe ue pe sf es c0 c1 c2 top c3 b)
 (declare (xargs :guard (and (bitp ie)
                             (bitp de)
                             (bitp ze)
                             (bitp oe)
                             (bitp ue)
                             (bitp pe)
                             (bitp sf)
                             (bitp es)
                             (bitp c0)
                             (bitp c1)
                             (bitp c2)
                             (3bits-p top)
                             (bitp c3)
                             (bitp b))))
 (let ((__function__ 'fp-statusbits))
  (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))
       (sf (mbe :logic (bfix sf) :exec sf))
       (es (mbe :logic (bfix es) :exec es))
       (c0 (mbe :logic (bfix c0) :exec c0))
       (c1 (mbe :logic (bfix c1) :exec c1))
       (c2 (mbe :logic (bfix c2) :exec c2))
       (top (mbe :logic (3bits-fix top) :exec top))
       (c3 (mbe :logic (bfix c3) :exec c3))
       (b (mbe :logic (bfix b) :exec b)))
   (logapp
    1 ie
    (logapp
     1 de
     (logapp
      1 ze
      (logapp
       1 oe
       (logapp
        1 ue
        (logapp
         1 pe
         (logapp
          1 sf
          (logapp
           1 es
           (logapp
            1 c0
            (logapp
                1 c1
                (logapp 1 c2
                        (logapp 3 top (logapp 1 c3 b))))))))))))))))

Theorem: fp-statusbits-p-of-fp-statusbits

(defthm fp-statusbits-p-of-fp-statusbits
  (b* ((fp-statusbits
            (fp-statusbits ie de
                           ze oe ue pe sf es c0 c1 c2 top c3 b)))
    (fp-statusbits-p fp-statusbits))
  :rule-classes :rewrite)

Theorem: fp-statusbits-of-bfix-ie

(defthm fp-statusbits-of-bfix-ie
  (equal (fp-statusbits (bfix ie)
                        de ze oe ue pe sf es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-ie

(defthm fp-statusbits-bit-equiv-congruence-on-ie
  (implies
       (bit-equiv ie ie-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie-equiv de
                             ze oe ue pe sf es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-de

(defthm fp-statusbits-of-bfix-de
  (equal (fp-statusbits ie (bfix de)
                        ze oe ue pe sf es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-de

(defthm fp-statusbits-bit-equiv-congruence-on-de
  (implies
       (bit-equiv de de-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de-equiv
                             ze oe ue pe sf es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-ze

(defthm fp-statusbits-of-bfix-ze
  (equal (fp-statusbits ie de (bfix ze)
                        oe ue pe sf es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-ze

(defthm fp-statusbits-bit-equiv-congruence-on-ze
  (implies
       (bit-equiv ze ze-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze-equiv
                             oe ue pe sf es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-oe

(defthm fp-statusbits-of-bfix-oe
  (equal (fp-statusbits ie de ze (bfix oe)
                        ue pe sf es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-oe

(defthm fp-statusbits-bit-equiv-congruence-on-oe
  (implies
       (bit-equiv oe oe-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe-equiv
                             ue pe sf es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-ue

(defthm fp-statusbits-of-bfix-ue
  (equal (fp-statusbits ie de ze oe (bfix ue)
                        pe sf es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-ue

(defthm fp-statusbits-bit-equiv-congruence-on-ue
  (implies
       (bit-equiv ue ue-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue-equiv pe sf es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-pe

(defthm fp-statusbits-of-bfix-pe
  (equal (fp-statusbits ie de ze oe ue (bfix pe)
                        sf es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-pe

(defthm fp-statusbits-bit-equiv-congruence-on-pe
  (implies
       (bit-equiv pe pe-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe-equiv sf es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-sf

(defthm fp-statusbits-of-bfix-sf
  (equal (fp-statusbits ie de ze oe ue pe (bfix sf)
                        es c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-sf

(defthm fp-statusbits-bit-equiv-congruence-on-sf
  (implies
       (bit-equiv sf sf-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf-equiv es c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-es

(defthm fp-statusbits-of-bfix-es
  (equal (fp-statusbits ie de ze oe ue pe sf (bfix es)
                        c0 c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-es

(defthm fp-statusbits-bit-equiv-congruence-on-es
  (implies
       (bit-equiv es es-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es-equiv c0 c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-c0

(defthm fp-statusbits-of-bfix-c0
  (equal (fp-statusbits ie de ze oe ue pe sf es (bfix c0)
                        c1 c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-c0

(defthm fp-statusbits-bit-equiv-congruence-on-c0
  (implies
       (bit-equiv c0 c0-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es c0-equiv c1 c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-c1

(defthm fp-statusbits-of-bfix-c1
  (equal (fp-statusbits ie de ze oe ue pe sf es c0 (bfix c1)
                        c2 top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-c1

(defthm fp-statusbits-bit-equiv-congruence-on-c1
  (implies
       (bit-equiv c1 c1-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es c0 c1-equiv c2 top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-c2

(defthm fp-statusbits-of-bfix-c2
  (equal (fp-statusbits ie de ze oe ue pe sf es c0 c1 (bfix c2)
                        top c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-c2

(defthm fp-statusbits-bit-equiv-congruence-on-c2
  (implies
       (bit-equiv c2 c2-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es c0 c1 c2-equiv top c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-3bits-fix-top

(defthm fp-statusbits-of-3bits-fix-top
  (equal (fp-statusbits ie de ze
                        oe ue pe sf es c0 c1 c2 (3bits-fix top)
                        c3 b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-3bits-equiv-congruence-on-top

(defthm fp-statusbits-3bits-equiv-congruence-on-top
  (implies
       (3bits-equiv top top-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es c0 c1 c2 top-equiv c3 b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-c3

(defthm fp-statusbits-of-bfix-c3
  (equal (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top (bfix c3)
                        b)
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-c3

(defthm fp-statusbits-bit-equiv-congruence-on-c3
  (implies
       (bit-equiv c3 c3-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es c0 c1 c2 top c3-equiv b)))
  :rule-classes :congruence)

Theorem: fp-statusbits-of-bfix-b

(defthm fp-statusbits-of-bfix-b
  (equal (fp-statusbits ie de ze
                        oe ue pe sf es c0 c1 c2 top c3 (bfix b))
         (fp-statusbits ie de
                        ze oe ue pe sf es c0 c1 c2 top c3 b)))

Theorem: fp-statusbits-bit-equiv-congruence-on-b

(defthm fp-statusbits-bit-equiv-congruence-on-b
  (implies
       (bit-equiv b b-equiv)
       (equal (fp-statusbits ie
                             de ze oe ue pe sf es c0 c1 c2 top c3 b)
              (fp-statusbits ie de ze oe
                             ue pe sf es c0 c1 c2 top c3 b-equiv)))
  :rule-classes :congruence)

Function: fp-statusbits-equiv-under-mask

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

Function: fp-statusbits->ie$inline

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

Theorem: bitp-of-fp-statusbits->ie

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

Theorem: fp-statusbits->ie$inline-of-fp-statusbits-fix-x

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

Theorem: fp-statusbits->ie$inline-fp-statusbits-equiv-congruence-on-x

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

Theorem: fp-statusbits->ie-of-fp-statusbits

(defthm fp-statusbits->ie-of-fp-statusbits
 (equal (fp-statusbits->ie
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix ie)))

Theorem: fp-statusbits->ie-of-write-with-mask

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

Function: fp-statusbits->de$inline

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

Theorem: bitp-of-fp-statusbits->de

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

Theorem: fp-statusbits->de$inline-of-fp-statusbits-fix-x

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

Theorem: fp-statusbits->de$inline-fp-statusbits-equiv-congruence-on-x

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

Theorem: fp-statusbits->de-of-fp-statusbits

(defthm fp-statusbits->de-of-fp-statusbits
 (equal (fp-statusbits->de
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix de)))

Theorem: fp-statusbits->de-of-write-with-mask

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

Function: fp-statusbits->ze$inline

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

Theorem: bitp-of-fp-statusbits->ze

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

Theorem: fp-statusbits->ze$inline-of-fp-statusbits-fix-x

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

Theorem: fp-statusbits->ze$inline-fp-statusbits-equiv-congruence-on-x

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

Theorem: fp-statusbits->ze-of-fp-statusbits

(defthm fp-statusbits->ze-of-fp-statusbits
 (equal (fp-statusbits->ze
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix ze)))

Theorem: fp-statusbits->ze-of-write-with-mask

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

Function: fp-statusbits->oe$inline

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

Theorem: bitp-of-fp-statusbits->oe

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

Theorem: fp-statusbits->oe$inline-of-fp-statusbits-fix-x

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

Theorem: fp-statusbits->oe$inline-fp-statusbits-equiv-congruence-on-x

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

Theorem: fp-statusbits->oe-of-fp-statusbits

(defthm fp-statusbits->oe-of-fp-statusbits
 (equal (fp-statusbits->oe
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix oe)))

Theorem: fp-statusbits->oe-of-write-with-mask

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

Function: fp-statusbits->ue$inline

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

Theorem: bitp-of-fp-statusbits->ue

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

Theorem: fp-statusbits->ue$inline-of-fp-statusbits-fix-x

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

Theorem: fp-statusbits->ue$inline-fp-statusbits-equiv-congruence-on-x

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

Theorem: fp-statusbits->ue-of-fp-statusbits

(defthm fp-statusbits->ue-of-fp-statusbits
 (equal (fp-statusbits->ue
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix ue)))

Theorem: fp-statusbits->ue-of-write-with-mask

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

Function: fp-statusbits->pe$inline

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

Theorem: bitp-of-fp-statusbits->pe

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

Theorem: fp-statusbits->pe$inline-of-fp-statusbits-fix-x

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

Theorem: fp-statusbits->pe$inline-fp-statusbits-equiv-congruence-on-x

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

Theorem: fp-statusbits->pe-of-fp-statusbits

(defthm fp-statusbits->pe-of-fp-statusbits
 (equal (fp-statusbits->pe
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix pe)))

Theorem: fp-statusbits->pe-of-write-with-mask

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

Function: fp-statusbits->sf$inline

(defun fp-statusbits->sf$inline (x)
 (declare (xargs :guard (fp-statusbits-p x)))
 (mbe
    :logic
    (let ((x (fp-statusbits-fix x)))
      (part-select x :low 6 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 10)
                            (ash (the (unsigned-byte 16) x) -6))))))

Theorem: bitp-of-fp-statusbits->sf

(defthm bitp-of-fp-statusbits->sf
  (b* ((sf (fp-statusbits->sf$inline x)))
    (bitp sf))
  :rule-classes :rewrite)

Theorem: fp-statusbits->sf$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->sf$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->sf$inline (fp-statusbits-fix x))
         (fp-statusbits->sf$inline x)))

Theorem: fp-statusbits->sf$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->sf$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->sf$inline x)
                  (fp-statusbits->sf$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->sf-of-fp-statusbits

(defthm fp-statusbits->sf-of-fp-statusbits
 (equal (fp-statusbits->sf
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix sf)))

Theorem: fp-statusbits->sf-of-write-with-mask

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

Function: fp-statusbits->es$inline

(defun fp-statusbits->es$inline (x)
 (declare (xargs :guard (fp-statusbits-p x)))
 (mbe
    :logic
    (let ((x (fp-statusbits-fix x)))
      (part-select x :low 7 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 9)
                            (ash (the (unsigned-byte 16) x) -7))))))

Theorem: bitp-of-fp-statusbits->es

(defthm bitp-of-fp-statusbits->es
  (b* ((es (fp-statusbits->es$inline x)))
    (bitp es))
  :rule-classes :rewrite)

Theorem: fp-statusbits->es$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->es$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->es$inline (fp-statusbits-fix x))
         (fp-statusbits->es$inline x)))

Theorem: fp-statusbits->es$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->es$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->es$inline x)
                  (fp-statusbits->es$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->es-of-fp-statusbits

(defthm fp-statusbits->es-of-fp-statusbits
 (equal (fp-statusbits->es
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix es)))

Theorem: fp-statusbits->es-of-write-with-mask

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

Function: fp-statusbits->c0$inline

(defun fp-statusbits->c0$inline (x)
 (declare (xargs :guard (fp-statusbits-p x)))
 (mbe
    :logic
    (let ((x (fp-statusbits-fix x)))
      (part-select x :low 8 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 8)
                            (ash (the (unsigned-byte 16) x) -8))))))

Theorem: bitp-of-fp-statusbits->c0

(defthm bitp-of-fp-statusbits->c0
  (b* ((c0 (fp-statusbits->c0$inline x)))
    (bitp c0))
  :rule-classes :rewrite)

Theorem: fp-statusbits->c0$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->c0$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->c0$inline (fp-statusbits-fix x))
         (fp-statusbits->c0$inline x)))

Theorem: fp-statusbits->c0$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->c0$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->c0$inline x)
                  (fp-statusbits->c0$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->c0-of-fp-statusbits

(defthm fp-statusbits->c0-of-fp-statusbits
 (equal (fp-statusbits->c0
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix c0)))

Theorem: fp-statusbits->c0-of-write-with-mask

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

Function: fp-statusbits->c1$inline

(defun fp-statusbits->c1$inline (x)
 (declare (xargs :guard (fp-statusbits-p x)))
 (mbe
    :logic
    (let ((x (fp-statusbits-fix x)))
      (part-select x :low 9 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 7)
                            (ash (the (unsigned-byte 16) x) -9))))))

Theorem: bitp-of-fp-statusbits->c1

(defthm bitp-of-fp-statusbits->c1
  (b* ((c1 (fp-statusbits->c1$inline x)))
    (bitp c1))
  :rule-classes :rewrite)

Theorem: fp-statusbits->c1$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->c1$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->c1$inline (fp-statusbits-fix x))
         (fp-statusbits->c1$inline x)))

Theorem: fp-statusbits->c1$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->c1$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->c1$inline x)
                  (fp-statusbits->c1$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->c1-of-fp-statusbits

(defthm fp-statusbits->c1-of-fp-statusbits
 (equal (fp-statusbits->c1
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix c1)))

Theorem: fp-statusbits->c1-of-write-with-mask

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

Function: fp-statusbits->c2$inline

(defun fp-statusbits->c2$inline (x)
  (declare (xargs :guard (fp-statusbits-p x)))
  (mbe :logic
       (let ((x (fp-statusbits-fix x)))
         (part-select x :low 10 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 16) x)
                                    -10))))))

Theorem: bitp-of-fp-statusbits->c2

(defthm bitp-of-fp-statusbits->c2
  (b* ((c2 (fp-statusbits->c2$inline x)))
    (bitp c2))
  :rule-classes :rewrite)

Theorem: fp-statusbits->c2$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->c2$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->c2$inline (fp-statusbits-fix x))
         (fp-statusbits->c2$inline x)))

Theorem: fp-statusbits->c2$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->c2$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->c2$inline x)
                  (fp-statusbits->c2$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->c2-of-fp-statusbits

(defthm fp-statusbits->c2-of-fp-statusbits
 (equal (fp-statusbits->c2
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix c2)))

Theorem: fp-statusbits->c2-of-write-with-mask

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

Function: fp-statusbits->top$inline

(defun fp-statusbits->top$inline (x)
  (declare (xargs :guard (fp-statusbits-p x)))
  (mbe :logic
       (let ((x (fp-statusbits-fix x)))
         (part-select x :low 11 :width 3))
       :exec (the (unsigned-byte 3)
                  (logand (the (unsigned-byte 3) 7)
                          (the (unsigned-byte 5)
                               (ash (the (unsigned-byte 16) x)
                                    -11))))))

Theorem: 3bits-p-of-fp-statusbits->top

(defthm 3bits-p-of-fp-statusbits->top
  (b* ((top (fp-statusbits->top$inline x)))
    (3bits-p top))
  :rule-classes :rewrite)

Theorem: fp-statusbits->top$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->top$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->top$inline (fp-statusbits-fix x))
         (fp-statusbits->top$inline x)))

Theorem: fp-statusbits->top$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      fp-statusbits->top$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->top$inline x)
                  (fp-statusbits->top$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->top-of-fp-statusbits

(defthm fp-statusbits->top-of-fp-statusbits
 (equal (fp-statusbits->top
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (3bits-fix top)))

Theorem: fp-statusbits->top-of-write-with-mask

(defthm fp-statusbits->top-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x fp-statusbits-equiv-under-mask)
                (fp-statusbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 14336)
                       0))
           (equal (fp-statusbits->top x)
                  (fp-statusbits->top y))))

Function: fp-statusbits->c3$inline

(defun fp-statusbits->c3$inline (x)
  (declare (xargs :guard (fp-statusbits-p x)))
  (mbe :logic
       (let ((x (fp-statusbits-fix x)))
         (part-select x :low 14 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 2)
                               (ash (the (unsigned-byte 16) x)
                                    -14))))))

Theorem: bitp-of-fp-statusbits->c3

(defthm bitp-of-fp-statusbits->c3
  (b* ((c3 (fp-statusbits->c3$inline x)))
    (bitp c3))
  :rule-classes :rewrite)

Theorem: fp-statusbits->c3$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->c3$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->c3$inline (fp-statusbits-fix x))
         (fp-statusbits->c3$inline x)))

Theorem: fp-statusbits->c3$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->c3$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->c3$inline x)
                  (fp-statusbits->c3$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->c3-of-fp-statusbits

(defthm fp-statusbits->c3-of-fp-statusbits
 (equal (fp-statusbits->c3
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix c3)))

Theorem: fp-statusbits->c3-of-write-with-mask

(defthm fp-statusbits->c3-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x fp-statusbits-equiv-under-mask)
                (fp-statusbits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 16384)
                       0))
           (equal (fp-statusbits->c3 x)
                  (fp-statusbits->c3 y))))

Function: fp-statusbits->b$inline

(defun fp-statusbits->b$inline (x)
  (declare (xargs :guard (fp-statusbits-p x)))
  (mbe :logic
       (let ((x (fp-statusbits-fix x)))
         (part-select x :low 15 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 1)
                               (ash (the (unsigned-byte 16) x)
                                    -15))))))

Theorem: bitp-of-fp-statusbits->b

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

Theorem: fp-statusbits->b$inline-of-fp-statusbits-fix-x

(defthm fp-statusbits->b$inline-of-fp-statusbits-fix-x
  (equal (fp-statusbits->b$inline (fp-statusbits-fix x))
         (fp-statusbits->b$inline x)))

Theorem: fp-statusbits->b$inline-fp-statusbits-equiv-congruence-on-x

(defthm fp-statusbits->b$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (fp-statusbits->b$inline x)
                  (fp-statusbits->b$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fp-statusbits->b-of-fp-statusbits

(defthm fp-statusbits->b-of-fp-statusbits
 (equal (fp-statusbits->b
             (fp-statusbits ie
                            de ze oe ue pe sf es c0 c1 c2 top c3 b))
        (bfix b)))

Theorem: fp-statusbits->b-of-write-with-mask

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

Theorem: fp-statusbits-fix-in-terms-of-fp-statusbits

(defthm fp-statusbits-fix-in-terms-of-fp-statusbits
  (equal (fp-statusbits-fix x)
         (change-fp-statusbits x)))

Function: !fp-statusbits->ie$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->ie

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

Theorem: !fp-statusbits->ie$inline-of-bfix-ie

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

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

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

Theorem: !fp-statusbits->ie$inline-of-fp-statusbits-fix-x

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

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

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

Theorem: !fp-statusbits->ie-is-fp-statusbits

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

Theorem: fp-statusbits->ie-of-!fp-statusbits->ie

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

Theorem: !fp-statusbits->ie-equiv-under-mask

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

Function: !fp-statusbits->de$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->de

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

Theorem: !fp-statusbits->de$inline-of-bfix-de

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

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

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

Theorem: !fp-statusbits->de$inline-of-fp-statusbits-fix-x

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

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

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

Theorem: !fp-statusbits->de-is-fp-statusbits

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

Theorem: fp-statusbits->de-of-!fp-statusbits->de

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

Theorem: !fp-statusbits->de-equiv-under-mask

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

Function: !fp-statusbits->ze$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->ze

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

Theorem: !fp-statusbits->ze$inline-of-bfix-ze

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

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

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

Theorem: !fp-statusbits->ze$inline-of-fp-statusbits-fix-x

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

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

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

Theorem: !fp-statusbits->ze-is-fp-statusbits

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

Theorem: fp-statusbits->ze-of-!fp-statusbits->ze

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

Theorem: !fp-statusbits->ze-equiv-under-mask

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

Function: !fp-statusbits->oe$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->oe

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

Theorem: !fp-statusbits->oe$inline-of-bfix-oe

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

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

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

Theorem: !fp-statusbits->oe$inline-of-fp-statusbits-fix-x

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

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

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

Theorem: !fp-statusbits->oe-is-fp-statusbits

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

Theorem: fp-statusbits->oe-of-!fp-statusbits->oe

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

Theorem: !fp-statusbits->oe-equiv-under-mask

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

Function: !fp-statusbits->ue$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->ue

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

Theorem: !fp-statusbits->ue$inline-of-bfix-ue

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

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

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

Theorem: !fp-statusbits->ue$inline-of-fp-statusbits-fix-x

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

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

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

Theorem: !fp-statusbits->ue-is-fp-statusbits

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

Theorem: fp-statusbits->ue-of-!fp-statusbits->ue

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

Theorem: !fp-statusbits->ue-equiv-under-mask

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

Function: !fp-statusbits->pe$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->pe

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

Theorem: !fp-statusbits->pe$inline-of-bfix-pe

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

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

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

Theorem: !fp-statusbits->pe$inline-of-fp-statusbits-fix-x

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

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

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

Theorem: !fp-statusbits->pe-is-fp-statusbits

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

Theorem: fp-statusbits->pe-of-!fp-statusbits->pe

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

Theorem: !fp-statusbits->pe-equiv-under-mask

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

Function: !fp-statusbits->sf$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->sf

(defthm fp-statusbits-p-of-!fp-statusbits->sf
  (b* ((new-x (!fp-statusbits->sf$inline sf x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->sf$inline-of-bfix-sf

(defthm !fp-statusbits->sf$inline-of-bfix-sf
  (equal (!fp-statusbits->sf$inline (bfix sf) x)
         (!fp-statusbits->sf$inline sf x)))

Theorem: !fp-statusbits->sf$inline-bit-equiv-congruence-on-sf

(defthm !fp-statusbits->sf$inline-bit-equiv-congruence-on-sf
  (implies (bit-equiv sf sf-equiv)
           (equal (!fp-statusbits->sf$inline sf x)
                  (!fp-statusbits->sf$inline sf-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->sf$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->sf$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->sf$inline sf (fp-statusbits-fix x))
         (!fp-statusbits->sf$inline sf x)))

Theorem: !fp-statusbits->sf$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      !fp-statusbits->sf$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->sf$inline sf x)
                  (!fp-statusbits->sf$inline sf x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->sf-is-fp-statusbits

(defthm !fp-statusbits->sf-is-fp-statusbits
  (equal (!fp-statusbits->sf sf x)
         (change-fp-statusbits x :sf sf)))

Theorem: fp-statusbits->sf-of-!fp-statusbits->sf

(defthm fp-statusbits->sf-of-!fp-statusbits->sf
  (b* ((?new-x (!fp-statusbits->sf$inline sf x)))
    (equal (fp-statusbits->sf new-x)
           (bfix sf))))

Theorem: !fp-statusbits->sf-equiv-under-mask

(defthm !fp-statusbits->sf-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->sf$inline sf x)))
    (fp-statusbits-equiv-under-mask new-x x -65)))

Function: !fp-statusbits->es$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->es

(defthm fp-statusbits-p-of-!fp-statusbits->es
  (b* ((new-x (!fp-statusbits->es$inline es x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->es$inline-of-bfix-es

(defthm !fp-statusbits->es$inline-of-bfix-es
  (equal (!fp-statusbits->es$inline (bfix es) x)
         (!fp-statusbits->es$inline es x)))

Theorem: !fp-statusbits->es$inline-bit-equiv-congruence-on-es

(defthm !fp-statusbits->es$inline-bit-equiv-congruence-on-es
  (implies (bit-equiv es es-equiv)
           (equal (!fp-statusbits->es$inline es x)
                  (!fp-statusbits->es$inline es-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->es$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->es$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->es$inline es (fp-statusbits-fix x))
         (!fp-statusbits->es$inline es x)))

Theorem: !fp-statusbits->es$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      !fp-statusbits->es$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->es$inline es x)
                  (!fp-statusbits->es$inline es x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->es-is-fp-statusbits

(defthm !fp-statusbits->es-is-fp-statusbits
  (equal (!fp-statusbits->es es x)
         (change-fp-statusbits x :es es)))

Theorem: fp-statusbits->es-of-!fp-statusbits->es

(defthm fp-statusbits->es-of-!fp-statusbits->es
  (b* ((?new-x (!fp-statusbits->es$inline es x)))
    (equal (fp-statusbits->es new-x)
           (bfix es))))

Theorem: !fp-statusbits->es-equiv-under-mask

(defthm !fp-statusbits->es-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->es$inline es x)))
    (fp-statusbits-equiv-under-mask new-x x -129)))

Function: !fp-statusbits->c0$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->c0

(defthm fp-statusbits-p-of-!fp-statusbits->c0
  (b* ((new-x (!fp-statusbits->c0$inline c0 x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->c0$inline-of-bfix-c0

(defthm !fp-statusbits->c0$inline-of-bfix-c0
  (equal (!fp-statusbits->c0$inline (bfix c0) x)
         (!fp-statusbits->c0$inline c0 x)))

Theorem: !fp-statusbits->c0$inline-bit-equiv-congruence-on-c0

(defthm !fp-statusbits->c0$inline-bit-equiv-congruence-on-c0
  (implies (bit-equiv c0 c0-equiv)
           (equal (!fp-statusbits->c0$inline c0 x)
                  (!fp-statusbits->c0$inline c0-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c0$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->c0$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->c0$inline c0 (fp-statusbits-fix x))
         (!fp-statusbits->c0$inline c0 x)))

Theorem: !fp-statusbits->c0$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      !fp-statusbits->c0$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->c0$inline c0 x)
                  (!fp-statusbits->c0$inline c0 x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c0-is-fp-statusbits

(defthm !fp-statusbits->c0-is-fp-statusbits
  (equal (!fp-statusbits->c0 c0 x)
         (change-fp-statusbits x :c0 c0)))

Theorem: fp-statusbits->c0-of-!fp-statusbits->c0

(defthm fp-statusbits->c0-of-!fp-statusbits->c0
  (b* ((?new-x (!fp-statusbits->c0$inline c0 x)))
    (equal (fp-statusbits->c0 new-x)
           (bfix c0))))

Theorem: !fp-statusbits->c0-equiv-under-mask

(defthm !fp-statusbits->c0-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->c0$inline c0 x)))
    (fp-statusbits-equiv-under-mask new-x x -257)))

Function: !fp-statusbits->c1$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->c1

(defthm fp-statusbits-p-of-!fp-statusbits->c1
  (b* ((new-x (!fp-statusbits->c1$inline c1 x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->c1$inline-of-bfix-c1

(defthm !fp-statusbits->c1$inline-of-bfix-c1
  (equal (!fp-statusbits->c1$inline (bfix c1) x)
         (!fp-statusbits->c1$inline c1 x)))

Theorem: !fp-statusbits->c1$inline-bit-equiv-congruence-on-c1

(defthm !fp-statusbits->c1$inline-bit-equiv-congruence-on-c1
  (implies (bit-equiv c1 c1-equiv)
           (equal (!fp-statusbits->c1$inline c1 x)
                  (!fp-statusbits->c1$inline c1-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c1$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->c1$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->c1$inline c1 (fp-statusbits-fix x))
         (!fp-statusbits->c1$inline c1 x)))

Theorem: !fp-statusbits->c1$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      !fp-statusbits->c1$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->c1$inline c1 x)
                  (!fp-statusbits->c1$inline c1 x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c1-is-fp-statusbits

(defthm !fp-statusbits->c1-is-fp-statusbits
  (equal (!fp-statusbits->c1 c1 x)
         (change-fp-statusbits x :c1 c1)))

Theorem: fp-statusbits->c1-of-!fp-statusbits->c1

(defthm fp-statusbits->c1-of-!fp-statusbits->c1
  (b* ((?new-x (!fp-statusbits->c1$inline c1 x)))
    (equal (fp-statusbits->c1 new-x)
           (bfix c1))))

Theorem: !fp-statusbits->c1-equiv-under-mask

(defthm !fp-statusbits->c1-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->c1$inline c1 x)))
    (fp-statusbits-equiv-under-mask new-x x -513)))

Function: !fp-statusbits->c2$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->c2

(defthm fp-statusbits-p-of-!fp-statusbits->c2
  (b* ((new-x (!fp-statusbits->c2$inline c2 x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->c2$inline-of-bfix-c2

(defthm !fp-statusbits->c2$inline-of-bfix-c2
  (equal (!fp-statusbits->c2$inline (bfix c2) x)
         (!fp-statusbits->c2$inline c2 x)))

Theorem: !fp-statusbits->c2$inline-bit-equiv-congruence-on-c2

(defthm !fp-statusbits->c2$inline-bit-equiv-congruence-on-c2
  (implies (bit-equiv c2 c2-equiv)
           (equal (!fp-statusbits->c2$inline c2 x)
                  (!fp-statusbits->c2$inline c2-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c2$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->c2$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->c2$inline c2 (fp-statusbits-fix x))
         (!fp-statusbits->c2$inline c2 x)))

Theorem: !fp-statusbits->c2$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      !fp-statusbits->c2$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->c2$inline c2 x)
                  (!fp-statusbits->c2$inline c2 x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c2-is-fp-statusbits

(defthm !fp-statusbits->c2-is-fp-statusbits
  (equal (!fp-statusbits->c2 c2 x)
         (change-fp-statusbits x :c2 c2)))

Theorem: fp-statusbits->c2-of-!fp-statusbits->c2

(defthm fp-statusbits->c2-of-!fp-statusbits->c2
  (b* ((?new-x (!fp-statusbits->c2$inline c2 x)))
    (equal (fp-statusbits->c2 new-x)
           (bfix c2))))

Theorem: !fp-statusbits->c2-equiv-under-mask

(defthm !fp-statusbits->c2-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->c2$inline c2 x)))
    (fp-statusbits-equiv-under-mask new-x x -1025)))

Function: !fp-statusbits->top$inline

(defun !fp-statusbits->top$inline (top x)
 (declare (xargs :guard (and (3bits-p top)
                             (fp-statusbits-p x))))
 (mbe
     :logic
     (b* ((top (mbe :logic (3bits-fix top) :exec top))
          (x (fp-statusbits-fix x)))
       (part-install top x :width 3 :low 11))
     :exec (the (unsigned-byte 16)
                (logior (the (unsigned-byte 16)
                             (logand (the (unsigned-byte 16) x)
                                     (the (signed-byte 15) -14337)))
                        (the (unsigned-byte 14)
                             (ash (the (unsigned-byte 3) top)
                                  11))))))

Theorem: fp-statusbits-p-of-!fp-statusbits->top

(defthm fp-statusbits-p-of-!fp-statusbits->top
  (b* ((new-x (!fp-statusbits->top$inline top x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->top$inline-of-3bits-fix-top

(defthm !fp-statusbits->top$inline-of-3bits-fix-top
  (equal (!fp-statusbits->top$inline (3bits-fix top)
                                     x)
         (!fp-statusbits->top$inline top x)))

Theorem: !fp-statusbits->top$inline-3bits-equiv-congruence-on-top

(defthm !fp-statusbits->top$inline-3bits-equiv-congruence-on-top
  (implies (3bits-equiv top top-equiv)
           (equal (!fp-statusbits->top$inline top x)
                  (!fp-statusbits->top$inline top-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->top$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->top$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->top$inline top (fp-statusbits-fix x))
         (!fp-statusbits->top$inline top x)))

Theorem: !fp-statusbits->top$inline-fp-statusbits-equiv-congruence-on-x

(defthm
     !fp-statusbits->top$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->top$inline top x)
                  (!fp-statusbits->top$inline top x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->top-is-fp-statusbits

(defthm !fp-statusbits->top-is-fp-statusbits
  (equal (!fp-statusbits->top top x)
         (change-fp-statusbits x :top top)))

Theorem: fp-statusbits->top-of-!fp-statusbits->top

(defthm fp-statusbits->top-of-!fp-statusbits->top
  (b* ((?new-x (!fp-statusbits->top$inline top x)))
    (equal (fp-statusbits->top new-x)
           (3bits-fix top))))

Theorem: !fp-statusbits->top-equiv-under-mask

(defthm !fp-statusbits->top-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->top$inline top x)))
    (fp-statusbits-equiv-under-mask new-x x -14337)))

Function: !fp-statusbits->c3$inline

(defun !fp-statusbits->c3$inline (c3 x)
 (declare (xargs :guard (and (bitp c3) (fp-statusbits-p x))))
 (mbe
    :logic
    (b* ((c3 (mbe :logic (bfix c3) :exec c3))
         (x (fp-statusbits-fix x)))
      (part-install c3 x :width 1 :low 14))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 16) -16385)))
                       (the (unsigned-byte 15)
                            (ash (the (unsigned-byte 1) c3) 14))))))

Theorem: fp-statusbits-p-of-!fp-statusbits->c3

(defthm fp-statusbits-p-of-!fp-statusbits->c3
  (b* ((new-x (!fp-statusbits->c3$inline c3 x)))
    (fp-statusbits-p new-x))
  :rule-classes :rewrite)

Theorem: !fp-statusbits->c3$inline-of-bfix-c3

(defthm !fp-statusbits->c3$inline-of-bfix-c3
  (equal (!fp-statusbits->c3$inline (bfix c3) x)
         (!fp-statusbits->c3$inline c3 x)))

Theorem: !fp-statusbits->c3$inline-bit-equiv-congruence-on-c3

(defthm !fp-statusbits->c3$inline-bit-equiv-congruence-on-c3
  (implies (bit-equiv c3 c3-equiv)
           (equal (!fp-statusbits->c3$inline c3 x)
                  (!fp-statusbits->c3$inline c3-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c3$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->c3$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->c3$inline c3 (fp-statusbits-fix x))
         (!fp-statusbits->c3$inline c3 x)))

Theorem: !fp-statusbits->c3$inline-fp-statusbits-equiv-congruence-on-x

(defthm
      !fp-statusbits->c3$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->c3$inline c3 x)
                  (!fp-statusbits->c3$inline c3 x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->c3-is-fp-statusbits

(defthm !fp-statusbits->c3-is-fp-statusbits
  (equal (!fp-statusbits->c3 c3 x)
         (change-fp-statusbits x :c3 c3)))

Theorem: fp-statusbits->c3-of-!fp-statusbits->c3

(defthm fp-statusbits->c3-of-!fp-statusbits->c3
  (b* ((?new-x (!fp-statusbits->c3$inline c3 x)))
    (equal (fp-statusbits->c3 new-x)
           (bfix c3))))

Theorem: !fp-statusbits->c3-equiv-under-mask

(defthm !fp-statusbits->c3-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->c3$inline c3 x)))
    (fp-statusbits-equiv-under-mask new-x x -16385)))

Function: !fp-statusbits->b$inline

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

Theorem: fp-statusbits-p-of-!fp-statusbits->b

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

Theorem: !fp-statusbits->b$inline-of-bfix-b

(defthm !fp-statusbits->b$inline-of-bfix-b
  (equal (!fp-statusbits->b$inline (bfix b) x)
         (!fp-statusbits->b$inline b x)))

Theorem: !fp-statusbits->b$inline-bit-equiv-congruence-on-b

(defthm !fp-statusbits->b$inline-bit-equiv-congruence-on-b
  (implies (bit-equiv b b-equiv)
           (equal (!fp-statusbits->b$inline b x)
                  (!fp-statusbits->b$inline b-equiv x)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->b$inline-of-fp-statusbits-fix-x

(defthm !fp-statusbits->b$inline-of-fp-statusbits-fix-x
  (equal (!fp-statusbits->b$inline b (fp-statusbits-fix x))
         (!fp-statusbits->b$inline b x)))

Theorem: !fp-statusbits->b$inline-fp-statusbits-equiv-congruence-on-x

(defthm !fp-statusbits->b$inline-fp-statusbits-equiv-congruence-on-x
  (implies (fp-statusbits-equiv x x-equiv)
           (equal (!fp-statusbits->b$inline b x)
                  (!fp-statusbits->b$inline b x-equiv)))
  :rule-classes :congruence)

Theorem: !fp-statusbits->b-is-fp-statusbits

(defthm !fp-statusbits->b-is-fp-statusbits
  (equal (!fp-statusbits->b b x)
         (change-fp-statusbits x :b b)))

Theorem: fp-statusbits->b-of-!fp-statusbits->b

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

Theorem: !fp-statusbits->b-equiv-under-mask

(defthm !fp-statusbits->b-equiv-under-mask
  (b* ((?new-x (!fp-statusbits->b$inline b x)))
    (fp-statusbits-equiv-under-mask new-x x 32767)))

Function: fp-statusbits-debug

(defun fp-statusbits-debug (x)
 (declare (xargs :guard (fp-statusbits-p x)))
 (let ((__function__ 'fp-statusbits-debug))
  (declare (ignorable __function__))
  (b* (((fp-statusbits 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 'sf x.sf)
          (cons
           (cons 'es x.es)
           (cons
            (cons 'c0 x.c0)
            (cons
             (cons 'c1 x.c1)
             (cons
                (cons 'c2 x.c2)
                (cons (cons 'top x.top)
                      (cons (cons 'c3 x.c3)
                            (cons (cons 'b x.b) nil)))))))))))))))))

Subtopics

Fp-statusbits-p

Recognizer for fp-statusbits bit structures.

!fp-statusbits->top

Update the |ACL2|::|TOP| field of a fp-statusbits bit structure.

!fp-statusbits->ze

Update the |X86ISA|::|ZE| field of a fp-statusbits bit structure.

!fp-statusbits->ue

Update the |X86ISA|::|UE| field of a fp-statusbits bit structure.

!fp-statusbits->sf

Update the |X86ISA|::|SF| field of a fp-statusbits bit structure.

!fp-statusbits->pe

Update the |ACL2|::|PE| field of a fp-statusbits bit structure.

!fp-statusbits->oe

Update the |X86ISA|::|OE| field of a fp-statusbits bit structure.

!fp-statusbits->ie

Update the |X86ISA|::|IE| field of a fp-statusbits bit structure.

!fp-statusbits->es

Update the |X86ISA|::|ES| field of a fp-statusbits bit structure.

!fp-statusbits->de

Update the |X86ISA|::|DE| field of a fp-statusbits bit structure.

!fp-statusbits->c3

Update the |X86ISA|::|C3| field of a fp-statusbits bit structure.

!fp-statusbits->c2

Update the |X86ISA|::|C2| field of a fp-statusbits bit structure.

!fp-statusbits->c1

Update the |X86ISA|::|C1| field of a fp-statusbits bit structure.

!fp-statusbits->c0

Update the |X86ISA|::|C0| field of a fp-statusbits bit structure.

!fp-statusbits->b

Update the |ACL2|::|B| field of a fp-statusbits bit structure.

Fp-statusbits->top

Access the |ACL2|::|TOP| field of a fp-statusbits bit structure.

Fp-statusbits-fix

Fixing function for fp-statusbits bit structures.

Fp-statusbits->ze

Access the |X86ISA|::|ZE| field of a fp-statusbits bit structure.

Fp-statusbits->ue

Access the |X86ISA|::|UE| field of a fp-statusbits bit structure.

Fp-statusbits->sf

Access the |X86ISA|::|SF| field of a fp-statusbits bit structure.

Fp-statusbits->pe

Access the |ACL2|::|PE| field of a fp-statusbits bit structure.

Fp-statusbits->oe

Access the |X86ISA|::|OE| field of a fp-statusbits bit structure.

Fp-statusbits->es

Access the |X86ISA|::|ES| field of a fp-statusbits bit structure.

Fp-statusbits->de

Access the |X86ISA|::|DE| field of a fp-statusbits bit structure.

Fp-statusbits->c3

Access the |X86ISA|::|C3| field of a fp-statusbits bit structure.

Fp-statusbits->c2

Access the |X86ISA|::|C2| field of a fp-statusbits bit structure.

Fp-statusbits->c1

Access the |X86ISA|::|C1| field of a fp-statusbits bit structure.

Fp-statusbits->c0

Access the |X86ISA|::|C0| field of a fp-statusbits bit structure.

Fp-statusbits->b

Access the |ACL2|::|B| field of a fp-statusbits bit structure.

Fp-statusbits->ie

Access the |X86ISA|::|IE| field of a fp-statusbits bit structure.