Update the |X86ISA|::|FZ| field of a mxcsrbits bit structure.
(!mxcsrbits->fz fz x) → new-x
Function:
(defun !mxcsrbits->fz$inline (fz x) (declare (xargs :guard (and (bitp fz) (mxcsrbits-p x)))) (mbe :logic (b* ((fz (mbe :logic (bfix fz) :exec fz)) (x (mxcsrbits-fix x))) (part-install fz 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) fz) 15))))))
Theorem:
(defthm mxcsrbits-p-of-!mxcsrbits->fz (b* ((new-x (!mxcsrbits->fz$inline fz x))) (mxcsrbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !mxcsrbits->fz$inline-of-bfix-fz (equal (!mxcsrbits->fz$inline (bfix fz) x) (!mxcsrbits->fz$inline fz x)))
Theorem:
(defthm !mxcsrbits->fz$inline-bit-equiv-congruence-on-fz (implies (bit-equiv fz fz-equiv) (equal (!mxcsrbits->fz$inline fz x) (!mxcsrbits->fz$inline fz-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !mxcsrbits->fz$inline-of-mxcsrbits-fix-x (equal (!mxcsrbits->fz$inline fz (mxcsrbits-fix x)) (!mxcsrbits->fz$inline fz x)))
Theorem:
(defthm !mxcsrbits->fz$inline-mxcsrbits-equiv-congruence-on-x (implies (mxcsrbits-equiv x x-equiv) (equal (!mxcsrbits->fz$inline fz x) (!mxcsrbits->fz$inline fz x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !mxcsrbits->fz-is-mxcsrbits (equal (!mxcsrbits->fz fz x) (change-mxcsrbits x :fz fz)))
Theorem:
(defthm mxcsrbits->fz-of-!mxcsrbits->fz (b* ((?new-x (!mxcsrbits->fz$inline fz x))) (equal (mxcsrbits->fz new-x) (bfix fz))))
Theorem:
(defthm !mxcsrbits->fz-equiv-under-mask (b* ((?new-x (!mxcsrbits->fz$inline fz x))) (mxcsrbits-equiv-under-mask new-x x -32769)))