		Search-engine friendly clone of the ACL2 documentation.

Structures

Xcr0bits

An 64-bit unsigned bitstruct type.

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

Fields

fpu/mmx-state — bit
sse-state — bit
avx-state — bit
bndreg-state — bit
bndcsr-state — bit
opmask-state — bit
zmm_hi256-state — bit
hi16_zmm-state — bit
res1 — bit
pkru-state — bit
res2 — 7bits
tileconfig-state — bit
tiledata-state — bit
res4 — 45bits

Source: Intel manual, Dec'23, Vol. 3A, Figure 2-8

Definitions and Theorems

Function: xcr0bits-p$inline

(defun xcr0bits-p$inline (x)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 64 x)
       :exec (and (natp x)
                  (< x 18446744073709551616))))

Theorem: xcr0bits-p-when-unsigned-byte-p

(defthm xcr0bits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (xcr0bits-p x)))

Theorem: unsigned-byte-p-when-xcr0bits-p

(defthm unsigned-byte-p-when-xcr0bits-p
  (implies (xcr0bits-p x)
           (unsigned-byte-p 64 x)))

Theorem: xcr0bits-p-compound-recognizer

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

Function: xcr0bits-fix$inline

(defun xcr0bits-fix$inline (x)
  (declare (xargs :guard (xcr0bits-p x)))
  (mbe :logic (loghead 64 x) :exec x))

Theorem: xcr0bits-p-of-xcr0bits-fix

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

Theorem: xcr0bits-fix-when-xcr0bits-p

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

Function: xcr0bits-equiv$inline

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

Theorem: xcr0bits-equiv-is-an-equivalence

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

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

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

Theorem: xcr0bits-fix-under-xcr0bits-equiv

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

Function: xcr0bits$inline

(defun xcr0bits$inline
       (fpu/mmx-state sse-state
                      avx-state bndreg-state bndcsr-state
                      opmask-state zmm_hi256-state
                      hi16_zmm-state res1 pkru-state res2
                      tileconfig-state tiledata-state res4)
 (declare (xargs :guard (and (bitp fpu/mmx-state)
                             (bitp sse-state)
                             (bitp avx-state)
                             (bitp bndreg-state)
                             (bitp bndcsr-state)
                             (bitp opmask-state)
                             (bitp zmm_hi256-state)
                             (bitp hi16_zmm-state)
                             (bitp res1)
                             (bitp pkru-state)
                             (7bits-p res2)
                             (bitp tileconfig-state)
                             (bitp tiledata-state)
                             (45bits-p res4))))
 (b* ((fpu/mmx-state (mbe :logic (bfix fpu/mmx-state)
                          :exec fpu/mmx-state))
      (sse-state (mbe :logic (bfix sse-state)
                      :exec sse-state))
      (avx-state (mbe :logic (bfix avx-state)
                      :exec avx-state))
      (bndreg-state (mbe :logic (bfix bndreg-state)
                         :exec bndreg-state))
      (bndcsr-state (mbe :logic (bfix bndcsr-state)
                         :exec bndcsr-state))
      (opmask-state (mbe :logic (bfix opmask-state)
                         :exec opmask-state))
      (zmm_hi256-state (mbe :logic (bfix zmm_hi256-state)
                            :exec zmm_hi256-state))
      (hi16_zmm-state (mbe :logic (bfix hi16_zmm-state)
                           :exec hi16_zmm-state))
      (res1 (mbe :logic (bfix res1) :exec res1))
      (pkru-state (mbe :logic (bfix pkru-state)
                       :exec pkru-state))
      (res2 (mbe :logic (7bits-fix res2)
                 :exec res2))
      (tileconfig-state (mbe :logic (bfix tileconfig-state)
                             :exec tileconfig-state))
      (tiledata-state (mbe :logic (bfix tiledata-state)
                           :exec tiledata-state))
      (res4 (mbe :logic (45bits-fix res4)
                 :exec res4)))
  (logapp
   1 fpu/mmx-state
   (logapp
    1 sse-state
    (logapp
     1 avx-state
     (logapp
      1 bndreg-state
      (logapp
       1 bndcsr-state
       (logapp
        1 opmask-state
        (logapp
         1 zmm_hi256-state
         (logapp
          1 hi16_zmm-state
          (logapp
           1 res1
           (logapp
            1 pkru-state
            (logapp
                7 res2
                (logapp 1 tileconfig-state
                        (logapp 1 tiledata-state res4)))))))))))))))

Theorem: xcr0bits-p-of-xcr0bits

(defthm xcr0bits-p-of-xcr0bits
  (b* ((xcr0bits
            (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
    (xcr0bits-p xcr0bits))
  :rule-classes :rewrite)

Theorem: xcr0bits$inline-of-bfix-fpu/mmx-state

(defthm xcr0bits$inline-of-bfix-fpu/mmx-state
  (equal (xcr0bits$inline (bfix fpu/mmx-state)
                          sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-fpu/mmx-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-fpu/mmx-state
 (implies
     (bit-equiv fpu/mmx-state fpu/mmx-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state-equiv sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-sse-state

(defthm xcr0bits$inline-of-bfix-sse-state
  (equal (xcr0bits$inline fpu/mmx-state (bfix sse-state)
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-sse-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-sse-state
 (implies
     (bit-equiv sse-state sse-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state-equiv
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-avx-state

(defthm xcr0bits$inline-of-bfix-avx-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state (bfix avx-state)
                          bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-avx-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-avx-state
 (implies
     (bit-equiv avx-state avx-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state-equiv
                             bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-bndreg-state

(defthm xcr0bits$inline-of-bfix-bndreg-state
  (equal (xcr0bits$inline fpu/mmx-state
                          sse-state avx-state (bfix bndreg-state)
                          bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-bndreg-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-bndreg-state
 (implies
     (bit-equiv bndreg-state bndreg-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state
                             bndreg-state-equiv bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-bndcsr-state

(defthm xcr0bits$inline-of-bfix-bndcsr-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state avx-state
                          bndreg-state (bfix bndcsr-state)
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-bndcsr-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-bndcsr-state
 (implies
     (bit-equiv bndcsr-state bndcsr-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state
                             bndreg-state bndcsr-state-equiv
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-opmask-state

(defthm xcr0bits$inline-of-bfix-opmask-state
  (equal (xcr0bits$inline fpu/mmx-state
                          sse-state avx-state bndreg-state
                          bndcsr-state (bfix opmask-state)
                          zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-opmask-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-opmask-state
 (implies
     (bit-equiv opmask-state opmask-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state-equiv zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-zmm_hi256-state

(defthm xcr0bits$inline-of-bfix-zmm_hi256-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state (bfix zmm_hi256-state)
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-zmm_hi256-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-zmm_hi256-state
 (implies
     (bit-equiv zmm_hi256-state zmm_hi256-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state-equiv
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-hi16_zmm-state

(defthm xcr0bits$inline-of-bfix-hi16_zmm-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state avx-state
                          bndreg-state bndcsr-state opmask-state
                          zmm_hi256-state (bfix hi16_zmm-state)
                          res1 pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-hi16_zmm-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-hi16_zmm-state
 (implies
     (bit-equiv hi16_zmm-state hi16_zmm-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state
                             bndreg-state bndcsr-state opmask-state
                             zmm_hi256-state hi16_zmm-state-equiv
                             res1 pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-res1

(defthm xcr0bits$inline-of-bfix-res1
  (equal (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state (bfix res1)
                          pkru-state res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-res1

(defthm xcr0bits$inline-bit-equiv-congruence-on-res1
 (implies
     (bit-equiv res1 res1-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state
                             bndreg-state bndcsr-state opmask-state
                             zmm_hi256-state hi16_zmm-state
                             res1-equiv pkru-state res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-pkru-state

(defthm xcr0bits$inline-of-bfix-pkru-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 (bfix pkru-state)
                          res2
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-pkru-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-pkru-state
 (implies
     (bit-equiv pkru-state pkru-state-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state
                             bndreg-state bndcsr-state opmask-state
                             zmm_hi256-state hi16_zmm-state
                             res1 pkru-state-equiv res2
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-7bits-fix-res2

(defthm xcr0bits$inline-of-7bits-fix-res2
  (equal (xcr0bits$inline fpu/mmx-state sse-state avx-state
                          bndreg-state bndcsr-state opmask-state
                          zmm_hi256-state hi16_zmm-state
                          res1 pkru-state (7bits-fix res2)
                          tileconfig-state tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-7bits-equiv-congruence-on-res2

(defthm xcr0bits$inline-7bits-equiv-congruence-on-res2
 (implies
     (7bits-equiv res2 res2-equiv)
     (equal (xcr0bits$inline fpu/mmx-state sse-state
                             avx-state bndreg-state bndcsr-state
                             opmask-state zmm_hi256-state
                             hi16_zmm-state res1 pkru-state res2
                             tileconfig-state tiledata-state res4)
            (xcr0bits$inline fpu/mmx-state sse-state avx-state
                             bndreg-state bndcsr-state opmask-state
                             zmm_hi256-state hi16_zmm-state
                             res1 pkru-state res2-equiv
                             tileconfig-state tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-tileconfig-state

(defthm xcr0bits$inline-of-bfix-tileconfig-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state avx-state
                          bndreg-state bndcsr-state opmask-state
                          zmm_hi256-state hi16_zmm-state res1
                          pkru-state res2 (bfix tileconfig-state)
                          tiledata-state res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-tileconfig-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-tileconfig-state
 (implies
      (bit-equiv tileconfig-state tileconfig-state-equiv)
      (equal (xcr0bits$inline fpu/mmx-state sse-state
                              avx-state bndreg-state bndcsr-state
                              opmask-state zmm_hi256-state
                              hi16_zmm-state res1 pkru-state res2
                              tileconfig-state tiledata-state res4)
             (xcr0bits$inline fpu/mmx-state sse-state avx-state
                              bndreg-state bndcsr-state opmask-state
                              zmm_hi256-state hi16_zmm-state res1
                              pkru-state res2 tileconfig-state-equiv
                              tiledata-state res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-bfix-tiledata-state

(defthm xcr0bits$inline-of-bfix-tiledata-state
  (equal (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state (bfix tiledata-state)
                          res4)
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-bit-equiv-congruence-on-tiledata-state

(defthm xcr0bits$inline-bit-equiv-congruence-on-tiledata-state
 (implies
      (bit-equiv tiledata-state tiledata-state-equiv)
      (equal (xcr0bits$inline fpu/mmx-state sse-state
                              avx-state bndreg-state bndcsr-state
                              opmask-state zmm_hi256-state
                              hi16_zmm-state res1 pkru-state res2
                              tileconfig-state tiledata-state res4)
             (xcr0bits$inline fpu/mmx-state sse-state avx-state
                              bndreg-state bndcsr-state opmask-state
                              zmm_hi256-state hi16_zmm-state
                              res1 pkru-state res2 tileconfig-state
                              tiledata-state-equiv res4)))
 :rule-classes :congruence)

Theorem: xcr0bits$inline-of-45bits-fix-res4

(defthm xcr0bits$inline-of-45bits-fix-res4
  (equal (xcr0bits$inline fpu/mmx-state sse-state avx-state
                          bndreg-state bndcsr-state opmask-state
                          zmm_hi256-state hi16_zmm-state
                          res1 pkru-state res2 tileconfig-state
                          tiledata-state (45bits-fix res4))
         (xcr0bits$inline fpu/mmx-state sse-state
                          avx-state bndreg-state bndcsr-state
                          opmask-state zmm_hi256-state
                          hi16_zmm-state res1 pkru-state res2
                          tileconfig-state tiledata-state res4)))

Theorem: xcr0bits$inline-45bits-equiv-congruence-on-res4

(defthm xcr0bits$inline-45bits-equiv-congruence-on-res4
 (implies
      (45bits-equiv res4 res4-equiv)
      (equal (xcr0bits$inline fpu/mmx-state sse-state
                              avx-state bndreg-state bndcsr-state
                              opmask-state zmm_hi256-state
                              hi16_zmm-state res1 pkru-state res2
                              tileconfig-state tiledata-state res4)
             (xcr0bits$inline fpu/mmx-state sse-state avx-state
                              bndreg-state bndcsr-state opmask-state
                              zmm_hi256-state hi16_zmm-state
                              res1 pkru-state res2 tileconfig-state
                              tiledata-state res4-equiv)))
 :rule-classes :congruence)

Function: xcr0bits-equiv-under-mask$inline

(defun xcr0bits-equiv-under-mask$inline (x x1 mask)
  (declare (xargs :guard (and (xcr0bits-p x)
                              (xcr0bits-p x1)
                              (integerp mask))))
  (fty::int-equiv-under-mask (xcr0bits-fix x)
                             (xcr0bits-fix x1)
                             mask))

Function: xcr0bits->fpu/mmx-state$inline

(defun xcr0bits->fpu/mmx-state$inline (x)
  (declare (xargs :guard (xcr0bits-p x)))
  (mbe :logic
       (let ((x (xcr0bits-fix x)))
         (part-select x :low 0 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 64) x)))))

Theorem: bitp-of-xcr0bits->fpu/mmx-state

(defthm bitp-of-xcr0bits->fpu/mmx-state
  (b* ((fpu/mmx-state (xcr0bits->fpu/mmx-state$inline x)))
    (bitp fpu/mmx-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->fpu/mmx-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->fpu/mmx-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->fpu/mmx-state$inline (xcr0bits-fix x))
         (xcr0bits->fpu/mmx-state$inline x)))

Theorem: xcr0bits->fpu/mmx-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
      xcr0bits->fpu/mmx-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->fpu/mmx-state$inline x)
                  (xcr0bits->fpu/mmx-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->fpu/mmx-state-of-xcr0bits

(defthm xcr0bits->fpu/mmx-state-of-xcr0bits
  (equal (xcr0bits->fpu/mmx-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix fpu/mmx-state)))

Theorem: xcr0bits->fpu/mmx-state-of-write-with-mask

(defthm xcr0bits->fpu/mmx-state-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x xcr0bits-equiv-under-mask)
   (xcr0bits-equiv-under-mask x y fty::mask)
   (equal (logand (lognot fty::mask) 1) 0))
  (equal (xcr0bits->fpu/mmx-state x)
         (xcr0bits->fpu/mmx-state y))))

Function: xcr0bits->sse-state$inline

(defun xcr0bits->sse-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 1 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 63)
                            (ash (the (unsigned-byte 64) x) -1))))))

Theorem: bitp-of-xcr0bits->sse-state

(defthm bitp-of-xcr0bits->sse-state
  (b* ((sse-state (xcr0bits->sse-state$inline x)))
    (bitp sse-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->sse-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->sse-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->sse-state$inline (xcr0bits-fix x))
         (xcr0bits->sse-state$inline x)))

Theorem: xcr0bits->sse-state$inline-xcr0bits-equiv-congruence-on-x

(defthm xcr0bits->sse-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->sse-state$inline x)
                  (xcr0bits->sse-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->sse-state-of-xcr0bits

(defthm xcr0bits->sse-state-of-xcr0bits
  (equal (xcr0bits->sse-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix sse-state)))

Theorem: xcr0bits->sse-state-of-write-with-mask

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

Function: xcr0bits->avx-state$inline

(defun xcr0bits->avx-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 2 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 62)
                            (ash (the (unsigned-byte 64) x) -2))))))

Theorem: bitp-of-xcr0bits->avx-state

(defthm bitp-of-xcr0bits->avx-state
  (b* ((avx-state (xcr0bits->avx-state$inline x)))
    (bitp avx-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->avx-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->avx-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->avx-state$inline (xcr0bits-fix x))
         (xcr0bits->avx-state$inline x)))

Theorem: xcr0bits->avx-state$inline-xcr0bits-equiv-congruence-on-x

(defthm xcr0bits->avx-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->avx-state$inline x)
                  (xcr0bits->avx-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->avx-state-of-xcr0bits

(defthm xcr0bits->avx-state-of-xcr0bits
  (equal (xcr0bits->avx-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix avx-state)))

Theorem: xcr0bits->avx-state-of-write-with-mask

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

Function: xcr0bits->bndreg-state$inline

(defun xcr0bits->bndreg-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 3 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 61)
                            (ash (the (unsigned-byte 64) x) -3))))))

Theorem: bitp-of-xcr0bits->bndreg-state

(defthm bitp-of-xcr0bits->bndreg-state
  (b* ((bndreg-state (xcr0bits->bndreg-state$inline x)))
    (bitp bndreg-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->bndreg-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->bndreg-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->bndreg-state$inline (xcr0bits-fix x))
         (xcr0bits->bndreg-state$inline x)))

Theorem: xcr0bits->bndreg-state$inline-xcr0bits-equiv-congruence-on-x

(defthm xcr0bits->bndreg-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->bndreg-state$inline x)
                  (xcr0bits->bndreg-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->bndreg-state-of-xcr0bits

(defthm xcr0bits->bndreg-state-of-xcr0bits
  (equal (xcr0bits->bndreg-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix bndreg-state)))

Theorem: xcr0bits->bndreg-state-of-write-with-mask

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

Function: xcr0bits->bndcsr-state$inline

(defun xcr0bits->bndcsr-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 4 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 60)
                            (ash (the (unsigned-byte 64) x) -4))))))

Theorem: bitp-of-xcr0bits->bndcsr-state

(defthm bitp-of-xcr0bits->bndcsr-state
  (b* ((bndcsr-state (xcr0bits->bndcsr-state$inline x)))
    (bitp bndcsr-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->bndcsr-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->bndcsr-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->bndcsr-state$inline (xcr0bits-fix x))
         (xcr0bits->bndcsr-state$inline x)))

Theorem: xcr0bits->bndcsr-state$inline-xcr0bits-equiv-congruence-on-x

(defthm xcr0bits->bndcsr-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->bndcsr-state$inline x)
                  (xcr0bits->bndcsr-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->bndcsr-state-of-xcr0bits

(defthm xcr0bits->bndcsr-state-of-xcr0bits
  (equal (xcr0bits->bndcsr-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix bndcsr-state)))

Theorem: xcr0bits->bndcsr-state-of-write-with-mask

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

Function: xcr0bits->opmask-state$inline

(defun xcr0bits->opmask-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 5 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 59)
                            (ash (the (unsigned-byte 64) x) -5))))))

Theorem: bitp-of-xcr0bits->opmask-state

(defthm bitp-of-xcr0bits->opmask-state
  (b* ((opmask-state (xcr0bits->opmask-state$inline x)))
    (bitp opmask-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->opmask-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->opmask-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->opmask-state$inline (xcr0bits-fix x))
         (xcr0bits->opmask-state$inline x)))

Theorem: xcr0bits->opmask-state$inline-xcr0bits-equiv-congruence-on-x

(defthm xcr0bits->opmask-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->opmask-state$inline x)
                  (xcr0bits->opmask-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->opmask-state-of-xcr0bits

(defthm xcr0bits->opmask-state-of-xcr0bits
  (equal (xcr0bits->opmask-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix opmask-state)))

Theorem: xcr0bits->opmask-state-of-write-with-mask

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

Function: xcr0bits->zmm_hi256-state$inline

(defun xcr0bits->zmm_hi256-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 6 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 58)
                            (ash (the (unsigned-byte 64) x) -6))))))

Theorem: bitp-of-xcr0bits->zmm_hi256-state

(defthm bitp-of-xcr0bits->zmm_hi256-state
  (b* ((zmm_hi256-state (xcr0bits->zmm_hi256-state$inline x)))
    (bitp zmm_hi256-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->zmm_hi256-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->zmm_hi256-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->zmm_hi256-state$inline (xcr0bits-fix x))
         (xcr0bits->zmm_hi256-state$inline x)))

Theorem: xcr0bits->zmm_hi256-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
    xcr0bits->zmm_hi256-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->zmm_hi256-state$inline x)
                  (xcr0bits->zmm_hi256-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->zmm_hi256-state-of-xcr0bits

(defthm xcr0bits->zmm_hi256-state-of-xcr0bits
  (equal (xcr0bits->zmm_hi256-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix zmm_hi256-state)))

Theorem: xcr0bits->zmm_hi256-state-of-write-with-mask

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

Function: xcr0bits->hi16_zmm-state$inline

(defun xcr0bits->hi16_zmm-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 7 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 57)
                            (ash (the (unsigned-byte 64) x) -7))))))

Theorem: bitp-of-xcr0bits->hi16_zmm-state

(defthm bitp-of-xcr0bits->hi16_zmm-state
  (b* ((hi16_zmm-state (xcr0bits->hi16_zmm-state$inline x)))
    (bitp hi16_zmm-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->hi16_zmm-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->hi16_zmm-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->hi16_zmm-state$inline (xcr0bits-fix x))
         (xcr0bits->hi16_zmm-state$inline x)))

Theorem: xcr0bits->hi16_zmm-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
     xcr0bits->hi16_zmm-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->hi16_zmm-state$inline x)
                  (xcr0bits->hi16_zmm-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->hi16_zmm-state-of-xcr0bits

(defthm xcr0bits->hi16_zmm-state-of-xcr0bits
  (equal (xcr0bits->hi16_zmm-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix hi16_zmm-state)))

Theorem: xcr0bits->hi16_zmm-state-of-write-with-mask

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

Function: xcr0bits->res1$inline

(defun xcr0bits->res1$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 8 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 56)
                            (ash (the (unsigned-byte 64) x) -8))))))

Theorem: bitp-of-xcr0bits->res1

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

Theorem: xcr0bits->res1$inline-of-xcr0bits-fix-x

(defthm xcr0bits->res1$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->res1$inline (xcr0bits-fix x))
         (xcr0bits->res1$inline x)))

Theorem: xcr0bits->res1$inline-xcr0bits-equiv-congruence-on-x

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

Theorem: xcr0bits->res1-of-xcr0bits

(defthm xcr0bits->res1-of-xcr0bits
 (equal
    (xcr0bits->res1 (xcr0bits fpu/mmx-state sse-state
                              avx-state bndreg-state bndcsr-state
                              opmask-state zmm_hi256-state
                              hi16_zmm-state res1 pkru-state res2
                              tileconfig-state tiledata-state res4))
    (bfix res1)))

Theorem: xcr0bits->res1-of-write-with-mask

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

Function: xcr0bits->pkru-state$inline

(defun xcr0bits->pkru-state$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (mbe
    :logic
    (let ((x (xcr0bits-fix x)))
      (part-select x :low 9 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 55)
                            (ash (the (unsigned-byte 64) x) -9))))))

Theorem: bitp-of-xcr0bits->pkru-state

(defthm bitp-of-xcr0bits->pkru-state
  (b* ((pkru-state (xcr0bits->pkru-state$inline x)))
    (bitp pkru-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->pkru-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->pkru-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->pkru-state$inline (xcr0bits-fix x))
         (xcr0bits->pkru-state$inline x)))

Theorem: xcr0bits->pkru-state$inline-xcr0bits-equiv-congruence-on-x

(defthm xcr0bits->pkru-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->pkru-state$inline x)
                  (xcr0bits->pkru-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->pkru-state-of-xcr0bits

(defthm xcr0bits->pkru-state-of-xcr0bits
  (equal (xcr0bits->pkru-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix pkru-state)))

Theorem: xcr0bits->pkru-state-of-write-with-mask

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

Function: xcr0bits->res2$inline

(defun xcr0bits->res2$inline (x)
  (declare (xargs :guard (xcr0bits-p x)))
  (mbe :logic
       (let ((x (xcr0bits-fix x)))
         (part-select x :low 10 :width 7))
       :exec (the (unsigned-byte 7)
                  (logand (the (unsigned-byte 7) 127)
                          (the (unsigned-byte 54)
                               (ash (the (unsigned-byte 64) x)
                                    -10))))))

Theorem: 7bits-p-of-xcr0bits->res2

(defthm 7bits-p-of-xcr0bits->res2
  (b* ((res2 (xcr0bits->res2$inline x)))
    (7bits-p res2))
  :rule-classes :rewrite)

Theorem: xcr0bits->res2$inline-of-xcr0bits-fix-x

(defthm xcr0bits->res2$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->res2$inline (xcr0bits-fix x))
         (xcr0bits->res2$inline x)))

Theorem: xcr0bits->res2$inline-xcr0bits-equiv-congruence-on-x

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

Theorem: xcr0bits->res2-of-xcr0bits

(defthm xcr0bits->res2-of-xcr0bits
 (equal
    (xcr0bits->res2 (xcr0bits fpu/mmx-state sse-state
                              avx-state bndreg-state bndcsr-state
                              opmask-state zmm_hi256-state
                              hi16_zmm-state res1 pkru-state res2
                              tileconfig-state tiledata-state res4))
    (7bits-fix res2)))

Theorem: xcr0bits->res2-of-write-with-mask

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

Function: xcr0bits->tileconfig-state$inline

(defun xcr0bits->tileconfig-state$inline (x)
  (declare (xargs :guard (xcr0bits-p x)))
  (mbe :logic
       (let ((x (xcr0bits-fix x)))
         (part-select x :low 17 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 47)
                               (ash (the (unsigned-byte 64) x)
                                    -17))))))

Theorem: bitp-of-xcr0bits->tileconfig-state

(defthm bitp-of-xcr0bits->tileconfig-state
  (b* ((tileconfig-state (xcr0bits->tileconfig-state$inline x)))
    (bitp tileconfig-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->tileconfig-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->tileconfig-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->tileconfig-state$inline (xcr0bits-fix x))
         (xcr0bits->tileconfig-state$inline x)))

Theorem: xcr0bits->tileconfig-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
   xcr0bits->tileconfig-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->tileconfig-state$inline x)
                  (xcr0bits->tileconfig-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->tileconfig-state-of-xcr0bits

(defthm xcr0bits->tileconfig-state-of-xcr0bits
  (equal (xcr0bits->tileconfig-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix tileconfig-state)))

Theorem: xcr0bits->tileconfig-state-of-write-with-mask

(defthm xcr0bits->tileconfig-state-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x xcr0bits-equiv-under-mask)
   (xcr0bits-equiv-under-mask x y fty::mask)
   (equal (logand (lognot fty::mask) 131072)
          0))
  (equal (xcr0bits->tileconfig-state x)
         (xcr0bits->tileconfig-state y))))

Function: xcr0bits->tiledata-state$inline

(defun xcr0bits->tiledata-state$inline (x)
  (declare (xargs :guard (xcr0bits-p x)))
  (mbe :logic
       (let ((x (xcr0bits-fix x)))
         (part-select x :low 18 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 46)
                               (ash (the (unsigned-byte 64) x)
                                    -18))))))

Theorem: bitp-of-xcr0bits->tiledata-state

(defthm bitp-of-xcr0bits->tiledata-state
  (b* ((tiledata-state (xcr0bits->tiledata-state$inline x)))
    (bitp tiledata-state))
  :rule-classes :rewrite)

Theorem: xcr0bits->tiledata-state$inline-of-xcr0bits-fix-x

(defthm xcr0bits->tiledata-state$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->tiledata-state$inline (xcr0bits-fix x))
         (xcr0bits->tiledata-state$inline x)))

Theorem: xcr0bits->tiledata-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
     xcr0bits->tiledata-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (xcr0bits->tiledata-state$inline x)
                  (xcr0bits->tiledata-state$inline x-equiv)))
  :rule-classes :congruence)

Theorem: xcr0bits->tiledata-state-of-xcr0bits

(defthm xcr0bits->tiledata-state-of-xcr0bits
  (equal (xcr0bits->tiledata-state
              (xcr0bits fpu/mmx-state sse-state
                        avx-state bndreg-state bndcsr-state
                        opmask-state zmm_hi256-state
                        hi16_zmm-state res1 pkru-state res2
                        tileconfig-state tiledata-state res4))
         (bfix tiledata-state)))

Theorem: xcr0bits->tiledata-state-of-write-with-mask

(defthm xcr0bits->tiledata-state-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x xcr0bits-equiv-under-mask)
   (xcr0bits-equiv-under-mask x y fty::mask)
   (equal (logand (lognot fty::mask) 262144)
          0))
  (equal (xcr0bits->tiledata-state x)
         (xcr0bits->tiledata-state y))))

Function: xcr0bits->res4$inline

(defun xcr0bits->res4$inline (x)
  (declare (xargs :guard (xcr0bits-p x)))
  (mbe :logic
       (let ((x (xcr0bits-fix x)))
         (part-select x :low 19 :width 45))
       :exec (the (unsigned-byte 45)
                  (logand (the (unsigned-byte 45) 35184372088831)
                          (the (unsigned-byte 45)
                               (ash (the (unsigned-byte 64) x)
                                    -19))))))

Theorem: 45bits-p-of-xcr0bits->res4

(defthm 45bits-p-of-xcr0bits->res4
  (b* ((res4 (xcr0bits->res4$inline x)))
    (45bits-p res4))
  :rule-classes :rewrite)

Theorem: xcr0bits->res4$inline-of-xcr0bits-fix-x

(defthm xcr0bits->res4$inline-of-xcr0bits-fix-x
  (equal (xcr0bits->res4$inline (xcr0bits-fix x))
         (xcr0bits->res4$inline x)))

Theorem: xcr0bits->res4$inline-xcr0bits-equiv-congruence-on-x

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

Theorem: xcr0bits->res4-of-xcr0bits

(defthm xcr0bits->res4-of-xcr0bits
 (equal
    (xcr0bits->res4 (xcr0bits fpu/mmx-state sse-state
                              avx-state bndreg-state bndcsr-state
                              opmask-state zmm_hi256-state
                              hi16_zmm-state res1 pkru-state res2
                              tileconfig-state tiledata-state res4))
    (45bits-fix res4)))

Theorem: xcr0bits->res4-of-write-with-mask

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

Theorem: xcr0bits-fix-in-terms-of-xcr0bits

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

Function: !xcr0bits->fpu/mmx-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->fpu/mmx-state

(defthm xcr0bits-p-of-!xcr0bits->fpu/mmx-state
  (b* ((new-x (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->fpu/mmx-state$inline-of-bfix-fpu/mmx-state

(defthm !xcr0bits->fpu/mmx-state$inline-of-bfix-fpu/mmx-state
  (equal (!xcr0bits->fpu/mmx-state$inline (bfix fpu/mmx-state)
                                          x)
         (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)))

Theorem: !xcr0bits->fpu/mmx-state$inline-bit-equiv-congruence-on-fpu/mmx-state

(defthm
 !xcr0bits->fpu/mmx-state$inline-bit-equiv-congruence-on-fpu/mmx-state
 (implies
    (bit-equiv fpu/mmx-state fpu/mmx-state-equiv)
    (equal (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)
           (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->fpu/mmx-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->fpu/mmx-state$inline-of-xcr0bits-fix-x
 (equal
    (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state (xcr0bits-fix x))
    (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)))

Theorem: !xcr0bits->fpu/mmx-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
     !xcr0bits->fpu/mmx-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
    (xcr0bits-equiv x x-equiv)
    (equal (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)
           (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->fpu/mmx-state-is-xcr0bits

(defthm !xcr0bits->fpu/mmx-state-is-xcr0bits
  (equal (!xcr0bits->fpu/mmx-state fpu/mmx-state x)
         (change-xcr0bits x
                          :fpu/mmx-state fpu/mmx-state)))

Theorem: xcr0bits->fpu/mmx-state-of-!xcr0bits->fpu/mmx-state

(defthm xcr0bits->fpu/mmx-state-of-!xcr0bits->fpu/mmx-state
  (b* ((?new-x (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)))
    (equal (xcr0bits->fpu/mmx-state new-x)
           (bfix fpu/mmx-state))))

Theorem: !xcr0bits->fpu/mmx-state-equiv-under-mask

(defthm !xcr0bits->fpu/mmx-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->fpu/mmx-state$inline fpu/mmx-state x)))
    (xcr0bits-equiv-under-mask new-x x -2)))

Function: !xcr0bits->sse-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->sse-state

(defthm xcr0bits-p-of-!xcr0bits->sse-state
  (b* ((new-x (!xcr0bits->sse-state$inline sse-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->sse-state$inline-of-bfix-sse-state

(defthm !xcr0bits->sse-state$inline-of-bfix-sse-state
  (equal (!xcr0bits->sse-state$inline (bfix sse-state)
                                      x)
         (!xcr0bits->sse-state$inline sse-state x)))

Theorem: !xcr0bits->sse-state$inline-bit-equiv-congruence-on-sse-state

(defthm
      !xcr0bits->sse-state$inline-bit-equiv-congruence-on-sse-state
  (implies (bit-equiv sse-state sse-state-equiv)
           (equal (!xcr0bits->sse-state$inline sse-state x)
                  (!xcr0bits->sse-state$inline sse-state-equiv x)))
  :rule-classes :congruence)

Theorem: !xcr0bits->sse-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->sse-state$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->sse-state$inline sse-state (xcr0bits-fix x))
         (!xcr0bits->sse-state$inline sse-state x)))

Theorem: !xcr0bits->sse-state$inline-xcr0bits-equiv-congruence-on-x

(defthm !xcr0bits->sse-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (!xcr0bits->sse-state$inline sse-state x)
                  (!xcr0bits->sse-state$inline sse-state x-equiv)))
  :rule-classes :congruence)

Theorem: !xcr0bits->sse-state-is-xcr0bits

(defthm !xcr0bits->sse-state-is-xcr0bits
  (equal (!xcr0bits->sse-state sse-state x)
         (change-xcr0bits x
                          :sse-state sse-state)))

Theorem: xcr0bits->sse-state-of-!xcr0bits->sse-state

(defthm xcr0bits->sse-state-of-!xcr0bits->sse-state
  (b* ((?new-x (!xcr0bits->sse-state$inline sse-state x)))
    (equal (xcr0bits->sse-state new-x)
           (bfix sse-state))))

Theorem: !xcr0bits->sse-state-equiv-under-mask

(defthm !xcr0bits->sse-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->sse-state$inline sse-state x)))
    (xcr0bits-equiv-under-mask new-x x -3)))

Function: !xcr0bits->avx-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->avx-state

(defthm xcr0bits-p-of-!xcr0bits->avx-state
  (b* ((new-x (!xcr0bits->avx-state$inline avx-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->avx-state$inline-of-bfix-avx-state

(defthm !xcr0bits->avx-state$inline-of-bfix-avx-state
  (equal (!xcr0bits->avx-state$inline (bfix avx-state)
                                      x)
         (!xcr0bits->avx-state$inline avx-state x)))

Theorem: !xcr0bits->avx-state$inline-bit-equiv-congruence-on-avx-state

(defthm
      !xcr0bits->avx-state$inline-bit-equiv-congruence-on-avx-state
  (implies (bit-equiv avx-state avx-state-equiv)
           (equal (!xcr0bits->avx-state$inline avx-state x)
                  (!xcr0bits->avx-state$inline avx-state-equiv x)))
  :rule-classes :congruence)

Theorem: !xcr0bits->avx-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->avx-state$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->avx-state$inline avx-state (xcr0bits-fix x))
         (!xcr0bits->avx-state$inline avx-state x)))

Theorem: !xcr0bits->avx-state$inline-xcr0bits-equiv-congruence-on-x

(defthm !xcr0bits->avx-state$inline-xcr0bits-equiv-congruence-on-x
  (implies (xcr0bits-equiv x x-equiv)
           (equal (!xcr0bits->avx-state$inline avx-state x)
                  (!xcr0bits->avx-state$inline avx-state x-equiv)))
  :rule-classes :congruence)

Theorem: !xcr0bits->avx-state-is-xcr0bits

(defthm !xcr0bits->avx-state-is-xcr0bits
  (equal (!xcr0bits->avx-state avx-state x)
         (change-xcr0bits x
                          :avx-state avx-state)))

Theorem: xcr0bits->avx-state-of-!xcr0bits->avx-state

(defthm xcr0bits->avx-state-of-!xcr0bits->avx-state
  (b* ((?new-x (!xcr0bits->avx-state$inline avx-state x)))
    (equal (xcr0bits->avx-state new-x)
           (bfix avx-state))))

Theorem: !xcr0bits->avx-state-equiv-under-mask

(defthm !xcr0bits->avx-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->avx-state$inline avx-state x)))
    (xcr0bits-equiv-under-mask new-x x -5)))

Function: !xcr0bits->bndreg-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->bndreg-state

(defthm xcr0bits-p-of-!xcr0bits->bndreg-state
  (b* ((new-x (!xcr0bits->bndreg-state$inline bndreg-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->bndreg-state$inline-of-bfix-bndreg-state

(defthm !xcr0bits->bndreg-state$inline-of-bfix-bndreg-state
  (equal (!xcr0bits->bndreg-state$inline (bfix bndreg-state)
                                         x)
         (!xcr0bits->bndreg-state$inline bndreg-state x)))

Theorem: !xcr0bits->bndreg-state$inline-bit-equiv-congruence-on-bndreg-state

(defthm
 !xcr0bits->bndreg-state$inline-bit-equiv-congruence-on-bndreg-state
 (implies
      (bit-equiv bndreg-state bndreg-state-equiv)
      (equal (!xcr0bits->bndreg-state$inline bndreg-state x)
             (!xcr0bits->bndreg-state$inline bndreg-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->bndreg-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->bndreg-state$inline-of-xcr0bits-fix-x
 (equal
      (!xcr0bits->bndreg-state$inline bndreg-state (xcr0bits-fix x))
      (!xcr0bits->bndreg-state$inline bndreg-state x)))

Theorem: !xcr0bits->bndreg-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
      !xcr0bits->bndreg-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
      (xcr0bits-equiv x x-equiv)
      (equal (!xcr0bits->bndreg-state$inline bndreg-state x)
             (!xcr0bits->bndreg-state$inline bndreg-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->bndreg-state-is-xcr0bits

(defthm !xcr0bits->bndreg-state-is-xcr0bits
  (equal (!xcr0bits->bndreg-state bndreg-state x)
         (change-xcr0bits x
                          :bndreg-state bndreg-state)))

Theorem: xcr0bits->bndreg-state-of-!xcr0bits->bndreg-state

(defthm xcr0bits->bndreg-state-of-!xcr0bits->bndreg-state
  (b* ((?new-x (!xcr0bits->bndreg-state$inline bndreg-state x)))
    (equal (xcr0bits->bndreg-state new-x)
           (bfix bndreg-state))))

Theorem: !xcr0bits->bndreg-state-equiv-under-mask

(defthm !xcr0bits->bndreg-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->bndreg-state$inline bndreg-state x)))
    (xcr0bits-equiv-under-mask new-x x -9)))

Function: !xcr0bits->bndcsr-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->bndcsr-state

(defthm xcr0bits-p-of-!xcr0bits->bndcsr-state
  (b* ((new-x (!xcr0bits->bndcsr-state$inline bndcsr-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->bndcsr-state$inline-of-bfix-bndcsr-state

(defthm !xcr0bits->bndcsr-state$inline-of-bfix-bndcsr-state
  (equal (!xcr0bits->bndcsr-state$inline (bfix bndcsr-state)
                                         x)
         (!xcr0bits->bndcsr-state$inline bndcsr-state x)))

Theorem: !xcr0bits->bndcsr-state$inline-bit-equiv-congruence-on-bndcsr-state

(defthm
 !xcr0bits->bndcsr-state$inline-bit-equiv-congruence-on-bndcsr-state
 (implies
      (bit-equiv bndcsr-state bndcsr-state-equiv)
      (equal (!xcr0bits->bndcsr-state$inline bndcsr-state x)
             (!xcr0bits->bndcsr-state$inline bndcsr-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->bndcsr-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->bndcsr-state$inline-of-xcr0bits-fix-x
 (equal
      (!xcr0bits->bndcsr-state$inline bndcsr-state (xcr0bits-fix x))
      (!xcr0bits->bndcsr-state$inline bndcsr-state x)))

Theorem: !xcr0bits->bndcsr-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
      !xcr0bits->bndcsr-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
      (xcr0bits-equiv x x-equiv)
      (equal (!xcr0bits->bndcsr-state$inline bndcsr-state x)
             (!xcr0bits->bndcsr-state$inline bndcsr-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->bndcsr-state-is-xcr0bits

(defthm !xcr0bits->bndcsr-state-is-xcr0bits
  (equal (!xcr0bits->bndcsr-state bndcsr-state x)
         (change-xcr0bits x
                          :bndcsr-state bndcsr-state)))

Theorem: xcr0bits->bndcsr-state-of-!xcr0bits->bndcsr-state

(defthm xcr0bits->bndcsr-state-of-!xcr0bits->bndcsr-state
  (b* ((?new-x (!xcr0bits->bndcsr-state$inline bndcsr-state x)))
    (equal (xcr0bits->bndcsr-state new-x)
           (bfix bndcsr-state))))

Theorem: !xcr0bits->bndcsr-state-equiv-under-mask

(defthm !xcr0bits->bndcsr-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->bndcsr-state$inline bndcsr-state x)))
    (xcr0bits-equiv-under-mask new-x x -17)))

Function: !xcr0bits->opmask-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->opmask-state

(defthm xcr0bits-p-of-!xcr0bits->opmask-state
  (b* ((new-x (!xcr0bits->opmask-state$inline opmask-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->opmask-state$inline-of-bfix-opmask-state

(defthm !xcr0bits->opmask-state$inline-of-bfix-opmask-state
  (equal (!xcr0bits->opmask-state$inline (bfix opmask-state)
                                         x)
         (!xcr0bits->opmask-state$inline opmask-state x)))

Theorem: !xcr0bits->opmask-state$inline-bit-equiv-congruence-on-opmask-state

(defthm
 !xcr0bits->opmask-state$inline-bit-equiv-congruence-on-opmask-state
 (implies
      (bit-equiv opmask-state opmask-state-equiv)
      (equal (!xcr0bits->opmask-state$inline opmask-state x)
             (!xcr0bits->opmask-state$inline opmask-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->opmask-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->opmask-state$inline-of-xcr0bits-fix-x
 (equal
      (!xcr0bits->opmask-state$inline opmask-state (xcr0bits-fix x))
      (!xcr0bits->opmask-state$inline opmask-state x)))

Theorem: !xcr0bits->opmask-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
      !xcr0bits->opmask-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
      (xcr0bits-equiv x x-equiv)
      (equal (!xcr0bits->opmask-state$inline opmask-state x)
             (!xcr0bits->opmask-state$inline opmask-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->opmask-state-is-xcr0bits

(defthm !xcr0bits->opmask-state-is-xcr0bits
  (equal (!xcr0bits->opmask-state opmask-state x)
         (change-xcr0bits x
                          :opmask-state opmask-state)))

Theorem: xcr0bits->opmask-state-of-!xcr0bits->opmask-state

(defthm xcr0bits->opmask-state-of-!xcr0bits->opmask-state
  (b* ((?new-x (!xcr0bits->opmask-state$inline opmask-state x)))
    (equal (xcr0bits->opmask-state new-x)
           (bfix opmask-state))))

Theorem: !xcr0bits->opmask-state-equiv-under-mask

(defthm !xcr0bits->opmask-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->opmask-state$inline opmask-state x)))
    (xcr0bits-equiv-under-mask new-x x -33)))

Function: !xcr0bits->zmm_hi256-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->zmm_hi256-state

(defthm xcr0bits-p-of-!xcr0bits->zmm_hi256-state
 (b* ((new-x (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)))
   (xcr0bits-p new-x))
 :rule-classes :rewrite)

Theorem: !xcr0bits->zmm_hi256-state$inline-of-bfix-zmm_hi256-state

(defthm !xcr0bits->zmm_hi256-state$inline-of-bfix-zmm_hi256-state
  (equal (!xcr0bits->zmm_hi256-state$inline (bfix zmm_hi256-state)
                                            x)
         (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)))

Theorem: !xcr0bits->zmm_hi256-state$inline-bit-equiv-congruence-on-zmm_hi256-state

(defthm
 !xcr0bits->zmm_hi256-state$inline-bit-equiv-congruence-on-zmm_hi256-state
 (implies
  (bit-equiv zmm_hi256-state zmm_hi256-state-equiv)
  (equal
       (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)
       (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->zmm_hi256-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->zmm_hi256-state$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->zmm_hi256-state$inline
              zmm_hi256-state (xcr0bits-fix x))
         (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)))

Theorem: !xcr0bits->zmm_hi256-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
   !xcr0bits->zmm_hi256-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
  (xcr0bits-equiv x x-equiv)
  (equal
       (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)
       (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->zmm_hi256-state-is-xcr0bits

(defthm !xcr0bits->zmm_hi256-state-is-xcr0bits
  (equal (!xcr0bits->zmm_hi256-state zmm_hi256-state x)
         (change-xcr0bits x
                          :zmm_hi256-state zmm_hi256-state)))

Theorem: xcr0bits->zmm_hi256-state-of-!xcr0bits->zmm_hi256-state

(defthm xcr0bits->zmm_hi256-state-of-!xcr0bits->zmm_hi256-state
  (b*
    ((?new-x (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)))
    (equal (xcr0bits->zmm_hi256-state new-x)
           (bfix zmm_hi256-state))))

Theorem: !xcr0bits->zmm_hi256-state-equiv-under-mask

(defthm !xcr0bits->zmm_hi256-state-equiv-under-mask
  (b*
    ((?new-x (!xcr0bits->zmm_hi256-state$inline zmm_hi256-state x)))
    (xcr0bits-equiv-under-mask new-x x -65)))

Function: !xcr0bits->hi16_zmm-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->hi16_zmm-state

(defthm xcr0bits-p-of-!xcr0bits->hi16_zmm-state
  (b* ((new-x (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->hi16_zmm-state$inline-of-bfix-hi16_zmm-state

(defthm !xcr0bits->hi16_zmm-state$inline-of-bfix-hi16_zmm-state
  (equal (!xcr0bits->hi16_zmm-state$inline (bfix hi16_zmm-state)
                                           x)
         (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)))

Theorem: !xcr0bits->hi16_zmm-state$inline-bit-equiv-congruence-on-hi16_zmm-state

(defthm
 !xcr0bits->hi16_zmm-state$inline-bit-equiv-congruence-on-hi16_zmm-state
 (implies
  (bit-equiv hi16_zmm-state hi16_zmm-state-equiv)
  (equal (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)
         (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->hi16_zmm-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->hi16_zmm-state$inline-of-xcr0bits-fix-x
 (equal
  (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state (xcr0bits-fix x))
  (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)))

Theorem: !xcr0bits->hi16_zmm-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
    !xcr0bits->hi16_zmm-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
  (xcr0bits-equiv x x-equiv)
  (equal (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)
         (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->hi16_zmm-state-is-xcr0bits

(defthm !xcr0bits->hi16_zmm-state-is-xcr0bits
  (equal (!xcr0bits->hi16_zmm-state hi16_zmm-state x)
         (change-xcr0bits x
                          :hi16_zmm-state hi16_zmm-state)))

Theorem: xcr0bits->hi16_zmm-state-of-!xcr0bits->hi16_zmm-state

(defthm xcr0bits->hi16_zmm-state-of-!xcr0bits->hi16_zmm-state
  (b* ((?new-x (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)))
    (equal (xcr0bits->hi16_zmm-state new-x)
           (bfix hi16_zmm-state))))

Theorem: !xcr0bits->hi16_zmm-state-equiv-under-mask

(defthm !xcr0bits->hi16_zmm-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->hi16_zmm-state$inline hi16_zmm-state x)))
    (xcr0bits-equiv-under-mask new-x x -129)))

Function: !xcr0bits->res1$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->res1

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

Theorem: !xcr0bits->res1$inline-of-bfix-res1

(defthm !xcr0bits->res1$inline-of-bfix-res1
  (equal (!xcr0bits->res1$inline (bfix res1) x)
         (!xcr0bits->res1$inline res1 x)))

Theorem: !xcr0bits->res1$inline-bit-equiv-congruence-on-res1

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

Theorem: !xcr0bits->res1$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->res1$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->res1$inline res1 (xcr0bits-fix x))
         (!xcr0bits->res1$inline res1 x)))

Theorem: !xcr0bits->res1$inline-xcr0bits-equiv-congruence-on-x

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

Theorem: !xcr0bits->res1-is-xcr0bits

(defthm !xcr0bits->res1-is-xcr0bits
  (equal (!xcr0bits->res1 res1 x)
         (change-xcr0bits x :res1 res1)))

Theorem: xcr0bits->res1-of-!xcr0bits->res1

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

Theorem: !xcr0bits->res1-equiv-under-mask

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

Function: !xcr0bits->pkru-state$inline

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

Theorem: xcr0bits-p-of-!xcr0bits->pkru-state

(defthm xcr0bits-p-of-!xcr0bits->pkru-state
  (b* ((new-x (!xcr0bits->pkru-state$inline pkru-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->pkru-state$inline-of-bfix-pkru-state

(defthm !xcr0bits->pkru-state$inline-of-bfix-pkru-state
  (equal (!xcr0bits->pkru-state$inline (bfix pkru-state)
                                       x)
         (!xcr0bits->pkru-state$inline pkru-state x)))

Theorem: !xcr0bits->pkru-state$inline-bit-equiv-congruence-on-pkru-state

(defthm
    !xcr0bits->pkru-state$inline-bit-equiv-congruence-on-pkru-state
 (implies (bit-equiv pkru-state pkru-state-equiv)
          (equal (!xcr0bits->pkru-state$inline pkru-state x)
                 (!xcr0bits->pkru-state$inline pkru-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->pkru-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->pkru-state$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->pkru-state$inline pkru-state (xcr0bits-fix x))
         (!xcr0bits->pkru-state$inline pkru-state x)))

Theorem: !xcr0bits->pkru-state$inline-xcr0bits-equiv-congruence-on-x

(defthm !xcr0bits->pkru-state$inline-xcr0bits-equiv-congruence-on-x
 (implies (xcr0bits-equiv x x-equiv)
          (equal (!xcr0bits->pkru-state$inline pkru-state x)
                 (!xcr0bits->pkru-state$inline pkru-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->pkru-state-is-xcr0bits

(defthm !xcr0bits->pkru-state-is-xcr0bits
  (equal (!xcr0bits->pkru-state pkru-state x)
         (change-xcr0bits x
                          :pkru-state pkru-state)))

Theorem: xcr0bits->pkru-state-of-!xcr0bits->pkru-state

(defthm xcr0bits->pkru-state-of-!xcr0bits->pkru-state
  (b* ((?new-x (!xcr0bits->pkru-state$inline pkru-state x)))
    (equal (xcr0bits->pkru-state new-x)
           (bfix pkru-state))))

Theorem: !xcr0bits->pkru-state-equiv-under-mask

(defthm !xcr0bits->pkru-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->pkru-state$inline pkru-state x)))
    (xcr0bits-equiv-under-mask new-x x -513)))

Function: !xcr0bits->res2$inline

(defun !xcr0bits->res2$inline (res2 x)
 (declare (xargs :guard (and (7bits-p res2) (xcr0bits-p x))))
 (mbe
    :logic
    (b* ((res2 (mbe :logic (7bits-fix res2)
                    :exec res2))
         (x (xcr0bits-fix x)))
      (part-install res2 x :width 7 :low 10))
    :exec (the (unsigned-byte 64)
               (logior (the (unsigned-byte 64)
                            (logand (the (unsigned-byte 64) x)
                                    (the (signed-byte 18) -130049)))
                       (the (unsigned-byte 17)
                            (ash (the (unsigned-byte 7) res2)
                                 10))))))

Theorem: xcr0bits-p-of-!xcr0bits->res2

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

Theorem: !xcr0bits->res2$inline-of-7bits-fix-res2

(defthm !xcr0bits->res2$inline-of-7bits-fix-res2
  (equal (!xcr0bits->res2$inline (7bits-fix res2)
                                 x)
         (!xcr0bits->res2$inline res2 x)))

Theorem: !xcr0bits->res2$inline-7bits-equiv-congruence-on-res2

(defthm !xcr0bits->res2$inline-7bits-equiv-congruence-on-res2
  (implies (7bits-equiv res2 res2-equiv)
           (equal (!xcr0bits->res2$inline res2 x)
                  (!xcr0bits->res2$inline res2-equiv x)))
  :rule-classes :congruence)

Theorem: !xcr0bits->res2$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->res2$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->res2$inline res2 (xcr0bits-fix x))
         (!xcr0bits->res2$inline res2 x)))

Theorem: !xcr0bits->res2$inline-xcr0bits-equiv-congruence-on-x

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

Theorem: !xcr0bits->res2-is-xcr0bits

(defthm !xcr0bits->res2-is-xcr0bits
  (equal (!xcr0bits->res2 res2 x)
         (change-xcr0bits x :res2 res2)))

Theorem: xcr0bits->res2-of-!xcr0bits->res2

(defthm xcr0bits->res2-of-!xcr0bits->res2
  (b* ((?new-x (!xcr0bits->res2$inline res2 x)))
    (equal (xcr0bits->res2 new-x)
           (7bits-fix res2))))

Theorem: !xcr0bits->res2-equiv-under-mask

(defthm !xcr0bits->res2-equiv-under-mask
  (b* ((?new-x (!xcr0bits->res2$inline res2 x)))
    (xcr0bits-equiv-under-mask new-x x -130049)))

Function: !xcr0bits->tileconfig-state$inline

(defun !xcr0bits->tileconfig-state$inline (tileconfig-state x)
 (declare (xargs :guard (and (bitp tileconfig-state)
                             (xcr0bits-p x))))
 (mbe
     :logic
     (b* ((tileconfig-state (mbe :logic (bfix tileconfig-state)
                                 :exec tileconfig-state))
          (x (xcr0bits-fix x)))
       (part-install tileconfig-state x
                     :width 1
                     :low 17))
     :exec
     (the (unsigned-byte 64)
          (logior (the (unsigned-byte 64)
                       (logand (the (unsigned-byte 64) x)
                               (the (signed-byte 19) -131073)))
                  (the (unsigned-byte 18)
                       (ash (the (unsigned-byte 1) tileconfig-state)
                            17))))))

Theorem: xcr0bits-p-of-!xcr0bits->tileconfig-state

(defthm xcr0bits-p-of-!xcr0bits->tileconfig-state
  (b*
   ((new-x (!xcr0bits->tileconfig-state$inline tileconfig-state x)))
   (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->tileconfig-state$inline-of-bfix-tileconfig-state

(defthm !xcr0bits->tileconfig-state$inline-of-bfix-tileconfig-state
  (equal (!xcr0bits->tileconfig-state$inline (bfix tileconfig-state)
                                             x)
         (!xcr0bits->tileconfig-state$inline tileconfig-state x)))

Theorem: !xcr0bits->tileconfig-state$inline-bit-equiv-congruence-on-tileconfig-state

(defthm
 !xcr0bits->tileconfig-state$inline-bit-equiv-congruence-on-tileconfig-state
 (implies
  (bit-equiv tileconfig-state tileconfig-state-equiv)
  (equal
     (!xcr0bits->tileconfig-state$inline tileconfig-state x)
     (!xcr0bits->tileconfig-state$inline tileconfig-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->tileconfig-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->tileconfig-state$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->tileconfig-state$inline
              tileconfig-state (xcr0bits-fix x))
         (!xcr0bits->tileconfig-state$inline tileconfig-state x)))

Theorem: !xcr0bits->tileconfig-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
  !xcr0bits->tileconfig-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
  (xcr0bits-equiv x x-equiv)
  (equal
     (!xcr0bits->tileconfig-state$inline tileconfig-state x)
     (!xcr0bits->tileconfig-state$inline tileconfig-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->tileconfig-state-is-xcr0bits

(defthm !xcr0bits->tileconfig-state-is-xcr0bits
  (equal (!xcr0bits->tileconfig-state tileconfig-state x)
         (change-xcr0bits x
                          :tileconfig-state tileconfig-state)))

Theorem: xcr0bits->tileconfig-state-of-!xcr0bits->tileconfig-state

(defthm xcr0bits->tileconfig-state-of-!xcr0bits->tileconfig-state
 (b*
  ((?new-x (!xcr0bits->tileconfig-state$inline tileconfig-state x)))
  (equal (xcr0bits->tileconfig-state new-x)
         (bfix tileconfig-state))))

Theorem: !xcr0bits->tileconfig-state-equiv-under-mask

(defthm !xcr0bits->tileconfig-state-equiv-under-mask
 (b*
  ((?new-x (!xcr0bits->tileconfig-state$inline tileconfig-state x)))
  (xcr0bits-equiv-under-mask new-x x -131073)))

Function: !xcr0bits->tiledata-state$inline

(defun !xcr0bits->tiledata-state$inline (tiledata-state x)
  (declare (xargs :guard (and (bitp tiledata-state)
                              (xcr0bits-p x))))
  (mbe :logic
       (b* ((tiledata-state (mbe :logic (bfix tiledata-state)
                                 :exec tiledata-state))
            (x (xcr0bits-fix x)))
         (part-install tiledata-state x
                       :width 1
                       :low 18))
       :exec
       (the (unsigned-byte 64)
            (logior (the (unsigned-byte 64)
                         (logand (the (unsigned-byte 64) x)
                                 (the (signed-byte 20) -262145)))
                    (the (unsigned-byte 19)
                         (ash (the (unsigned-byte 1) tiledata-state)
                              18))))))

Theorem: xcr0bits-p-of-!xcr0bits->tiledata-state

(defthm xcr0bits-p-of-!xcr0bits->tiledata-state
  (b* ((new-x (!xcr0bits->tiledata-state$inline tiledata-state x)))
    (xcr0bits-p new-x))
  :rule-classes :rewrite)

Theorem: !xcr0bits->tiledata-state$inline-of-bfix-tiledata-state

(defthm !xcr0bits->tiledata-state$inline-of-bfix-tiledata-state
  (equal (!xcr0bits->tiledata-state$inline (bfix tiledata-state)
                                           x)
         (!xcr0bits->tiledata-state$inline tiledata-state x)))

Theorem: !xcr0bits->tiledata-state$inline-bit-equiv-congruence-on-tiledata-state

(defthm
 !xcr0bits->tiledata-state$inline-bit-equiv-congruence-on-tiledata-state
 (implies
  (bit-equiv tiledata-state tiledata-state-equiv)
  (equal (!xcr0bits->tiledata-state$inline tiledata-state x)
         (!xcr0bits->tiledata-state$inline tiledata-state-equiv x)))
 :rule-classes :congruence)

Theorem: !xcr0bits->tiledata-state$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->tiledata-state$inline-of-xcr0bits-fix-x
 (equal
  (!xcr0bits->tiledata-state$inline tiledata-state (xcr0bits-fix x))
  (!xcr0bits->tiledata-state$inline tiledata-state x)))

Theorem: !xcr0bits->tiledata-state$inline-xcr0bits-equiv-congruence-on-x

(defthm
    !xcr0bits->tiledata-state$inline-xcr0bits-equiv-congruence-on-x
 (implies
  (xcr0bits-equiv x x-equiv)
  (equal (!xcr0bits->tiledata-state$inline tiledata-state x)
         (!xcr0bits->tiledata-state$inline tiledata-state x-equiv)))
 :rule-classes :congruence)

Theorem: !xcr0bits->tiledata-state-is-xcr0bits

(defthm !xcr0bits->tiledata-state-is-xcr0bits
  (equal (!xcr0bits->tiledata-state tiledata-state x)
         (change-xcr0bits x
                          :tiledata-state tiledata-state)))

Theorem: xcr0bits->tiledata-state-of-!xcr0bits->tiledata-state

(defthm xcr0bits->tiledata-state-of-!xcr0bits->tiledata-state
  (b* ((?new-x (!xcr0bits->tiledata-state$inline tiledata-state x)))
    (equal (xcr0bits->tiledata-state new-x)
           (bfix tiledata-state))))

Theorem: !xcr0bits->tiledata-state-equiv-under-mask

(defthm !xcr0bits->tiledata-state-equiv-under-mask
  (b* ((?new-x (!xcr0bits->tiledata-state$inline tiledata-state x)))
    (xcr0bits-equiv-under-mask new-x x -262145)))

Function: !xcr0bits->res4$inline

(defun !xcr0bits->res4$inline (res4 x)
  (declare (xargs :guard (and (45bits-p res4) (xcr0bits-p x))))
  (mbe :logic
       (b* ((res4 (mbe :logic (45bits-fix res4)
                       :exec res4))
            (x (xcr0bits-fix x)))
         (part-install res4 x :width 45 :low 19))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 65)
                                            -18446744073709027329)))
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 45) res4)
                                    19))))))

Theorem: xcr0bits-p-of-!xcr0bits->res4

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

Theorem: !xcr0bits->res4$inline-of-45bits-fix-res4

(defthm !xcr0bits->res4$inline-of-45bits-fix-res4
  (equal (!xcr0bits->res4$inline (45bits-fix res4)
                                 x)
         (!xcr0bits->res4$inline res4 x)))

Theorem: !xcr0bits->res4$inline-45bits-equiv-congruence-on-res4

(defthm !xcr0bits->res4$inline-45bits-equiv-congruence-on-res4
  (implies (45bits-equiv res4 res4-equiv)
           (equal (!xcr0bits->res4$inline res4 x)
                  (!xcr0bits->res4$inline res4-equiv x)))
  :rule-classes :congruence)

Theorem: !xcr0bits->res4$inline-of-xcr0bits-fix-x

(defthm !xcr0bits->res4$inline-of-xcr0bits-fix-x
  (equal (!xcr0bits->res4$inline res4 (xcr0bits-fix x))
         (!xcr0bits->res4$inline res4 x)))

Theorem: !xcr0bits->res4$inline-xcr0bits-equiv-congruence-on-x

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

Theorem: !xcr0bits->res4-is-xcr0bits

(defthm !xcr0bits->res4-is-xcr0bits
  (equal (!xcr0bits->res4 res4 x)
         (change-xcr0bits x :res4 res4)))

Theorem: xcr0bits->res4-of-!xcr0bits->res4

(defthm xcr0bits->res4-of-!xcr0bits->res4
  (b* ((?new-x (!xcr0bits->res4$inline res4 x)))
    (equal (xcr0bits->res4 new-x)
           (45bits-fix res4))))

Theorem: !xcr0bits->res4-equiv-under-mask

(defthm !xcr0bits->res4-equiv-under-mask
  (b* ((?new-x (!xcr0bits->res4$inline res4 x)))
    (xcr0bits-equiv-under-mask new-x x 524287)))

Function: xcr0bits-debug$inline

(defun xcr0bits-debug$inline (x)
 (declare (xargs :guard (xcr0bits-p x)))
 (b* (((xcr0bits x)))
  (cons
   (cons 'fpu/mmx-state x.fpu/mmx-state)
   (cons
    (cons 'sse-state x.sse-state)
    (cons
     (cons 'avx-state x.avx-state)
     (cons
      (cons 'bndreg-state x.bndreg-state)
      (cons
       (cons 'bndcsr-state x.bndcsr-state)
       (cons
        (cons 'opmask-state x.opmask-state)
        (cons
         (cons 'zmm_hi256-state
               x.zmm_hi256-state)
         (cons
          (cons 'hi16_zmm-state x.hi16_zmm-state)
          (cons
           (cons 'res1 x.res1)
           (cons
            (cons 'pkru-state x.pkru-state)
            (cons
                 (cons 'res2 x.res2)
                 (cons (cons 'tileconfig-state
                             x.tileconfig-state)
                       (cons (cons 'tiledata-state x.tiledata-state)
                             (cons (cons 'res4 x.res4)
                                   nil))))))))))))))))

Subtopics

Xcr0bits-p: Recognizer for xcr0bits bit structures.
!xcr0bits->tileconfig-state: Update the |X86ISA|::|TILECONFIG-STATE| field of a xcr0bits bit structure.
!xcr0bits->zmm_hi256-state: Update the |X86ISA|::|ZMM_HI256-STATE| field of a xcr0bits bit structure.
!xcr0bits->tiledata-state: Update the |X86ISA|::|TILEDATA-STATE| field of a xcr0bits bit structure.
!xcr0bits->hi16_zmm-state: Update the |X86ISA|::|HI16_ZMM-STATE| field of a xcr0bits bit structure.
!xcr0bits->fpu/mmx-state: Update the |X86ISA|::|FPU/MMX-STATE| field of a xcr0bits bit structure.
!xcr0bits->opmask-state: Update the |X86ISA|::|OPMASK-STATE| field of a xcr0bits bit structure.
!xcr0bits->bndreg-state: Update the |X86ISA|::|BNDREG-STATE| field of a xcr0bits bit structure.
!xcr0bits->bndcsr-state: Update the |X86ISA|::|BNDCSR-STATE| field of a xcr0bits bit structure.
!xcr0bits->pkru-state: Update the |X86ISA|::|PKRU-STATE| field of a xcr0bits bit structure.
!xcr0bits->sse-state: Update the |X86ISA|::|SSE-STATE| field of a xcr0bits bit structure.
!xcr0bits->avx-state: Update the |X86ISA|::|AVX-STATE| field of a xcr0bits bit structure.
!xcr0bits->res4: Update the |X86ISA|::|RES4| field of a xcr0bits bit structure.
!xcr0bits->res2: Update the |X86ISA|::|RES2| field of a xcr0bits bit structure.
!xcr0bits->res1: Update the |X86ISA|::|RES1| field of a xcr0bits bit structure.
Xcr0bits->tileconfig-state: Access the |X86ISA|::|TILECONFIG-STATE| field of a xcr0bits bit structure.
Xcr0bits->zmm_hi256-state: Access the |X86ISA|::|ZMM_HI256-STATE| field of a xcr0bits bit structure.
Xcr0bits->tiledata-state: Access the |X86ISA|::|TILEDATA-STATE| field of a xcr0bits bit structure.
Xcr0bits->hi16_zmm-state: Access the |X86ISA|::|HI16_ZMM-STATE| field of a xcr0bits bit structure.
Xcr0bits->pkru-state: Access the |X86ISA|::|PKRU-STATE| field of a xcr0bits bit structure.
Xcr0bits->opmask-state: Access the |X86ISA|::|OPMASK-STATE| field of a xcr0bits bit structure.
Xcr0bits->fpu/mmx-state: Access the |X86ISA|::|FPU/MMX-STATE| field of a xcr0bits bit structure.
Xcr0bits->bndreg-state: Access the |X86ISA|::|BNDREG-STATE| field of a xcr0bits bit structure.
Xcr0bits->bndcsr-state: Access the |X86ISA|::|BNDCSR-STATE| field of a xcr0bits bit structure.
Xcr0bits->sse-state: Access the |X86ISA|::|SSE-STATE| field of a xcr0bits bit structure.
Xcr0bits->res4: Access the |X86ISA|::|RES4| field of a xcr0bits bit structure.
Xcr0bits->avx-state: Access the |X86ISA|::|AVX-STATE| field of a xcr0bits bit structure.
Xcr0bits->res2: Access the |X86ISA|::|RES2| field of a xcr0bits bit structure.
Xcr0bits->res1: Access the |X86ISA|::|RES1| field of a xcr0bits bit structure.
Xcr0bits-fix: Fixing function for xcr0bits bit structures.