		Search-engine friendly clone of the ACL2 documentation.

Mxcsrbits

!mxcsrbits->rc

Update the |X86ISA|::|RC| field of a mxcsrbits bit structure.

Signature
(!mxcsrbits->rc rc x) → new-x
Arguments: rc — Guard (2bits-p rc).; x — Guard (mxcsrbits-p x).
Returns: new-x — Type (mxcsrbits-p new-x).

Definitions and Theorems

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