		Search-engine friendly clone of the ACL2 documentation.

Structures

Cr0bits

An 32-bit unsigned bitstruct type.

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

Fields

pe — bit: Protection Enable
mp — bit: Monitor coProcessor
em — bit: Emulation Bit
ts — bit: Task Switched
et — bit: Extension Type
ne — bit: Numeric Error
res1 — 10bits: 0 (Reserved)
wp — bit: Write Protect
res2 — bit: 0 (Reserved)
am — bit: Alignment Mask
res3 — 10bits: 0 (Reserved)
nw — bit: Not Write-through
cd — bit: Cache Disable
pg — bit: Paging Bit

Source: Intel Manual, Dec-23, Vol. 3A, Section 2.5

Definitions and Theorems

Function: cr0bits-p$inline

(defun cr0bits-p$inline (x)
  (declare (xargs :guard t))
  (mbe :logic (unsigned-byte-p 32 x)
       :exec (and (natp x) (< x 4294967296))))

Theorem: cr0bits-p-when-unsigned-byte-p

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

Theorem: unsigned-byte-p-when-cr0bits-p

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

Theorem: cr0bits-p-compound-recognizer

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

Function: cr0bits-fix$inline

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

Theorem: cr0bits-p-of-cr0bits-fix

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

Theorem: cr0bits-fix-when-cr0bits-p

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

Function: cr0bits-equiv$inline

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

Theorem: cr0bits-equiv-is-an-equivalence

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

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

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

Theorem: cr0bits-fix-under-cr0bits-equiv

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

Function: cr0bits$inline

(defun cr0bits$inline (pe mp em
                          ts et ne res1 wp res2 am res3 nw cd pg)
 (declare (xargs :guard (and (bitp pe)
                             (bitp mp)
                             (bitp em)
                             (bitp ts)
                             (bitp et)
                             (bitp ne)
                             (10bits-p res1)
                             (bitp wp)
                             (bitp res2)
                             (bitp am)
                             (10bits-p res3)
                             (bitp nw)
                             (bitp cd)
                             (bitp pg))))
 (b* ((pe (mbe :logic (bfix pe) :exec pe))
      (mp (mbe :logic (bfix mp) :exec mp))
      (em (mbe :logic (bfix em) :exec em))
      (ts (mbe :logic (bfix ts) :exec ts))
      (et (mbe :logic (bfix et) :exec et))
      (ne (mbe :logic (bfix ne) :exec ne))
      (res1 (mbe :logic (10bits-fix res1)
                 :exec res1))
      (wp (mbe :logic (bfix wp) :exec wp))
      (res2 (mbe :logic (bfix res2) :exec res2))
      (am (mbe :logic (bfix am) :exec am))
      (res3 (mbe :logic (10bits-fix res3)
                 :exec res3))
      (nw (mbe :logic (bfix nw) :exec nw))
      (cd (mbe :logic (bfix cd) :exec cd))
      (pg (mbe :logic (bfix pg) :exec pg)))
  (logapp
   1 pe
   (logapp
    1 mp
    (logapp
     1 em
     (logapp
      1 ts
      (logapp
       1 et
       (logapp
        1 ne
        (logapp
         10 res1
         (logapp
          1 wp
          (logapp
            1 res2
            (logapp
                 1 am
                 (logapp 10 res3
                         (logapp 1 nw (logapp 1 cd pg)))))))))))))))

Theorem: cr0bits-p-of-cr0bits

(defthm cr0bits-p-of-cr0bits
  (b*
    ((cr0bits (cr0bits$inline pe mp em ts
                              et ne res1 wp res2 am res3 nw cd pg)))
    (cr0bits-p cr0bits))
  :rule-classes :rewrite)

Theorem: cr0bits$inline-of-bfix-pe

(defthm cr0bits$inline-of-bfix-pe
  (equal (cr0bits$inline (bfix pe)
                         mp em
                         ts et ne res1 wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-pe

(defthm cr0bits$inline-bit-equiv-congruence-on-pe
 (implies
      (bit-equiv pe pe-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe-equiv mp em ts
                             et ne res1 wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-mp

(defthm cr0bits$inline-of-bfix-mp
  (equal (cr0bits$inline pe (bfix mp)
                         em
                         ts et ne res1 wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-mp

(defthm cr0bits$inline-bit-equiv-congruence-on-mp
 (implies
      (bit-equiv mp mp-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp-equiv em ts
                             et ne res1 wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-em

(defthm cr0bits$inline-of-bfix-em
  (equal (cr0bits$inline pe mp (bfix em)
                         ts et ne res1 wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-em

(defthm cr0bits$inline-bit-equiv-congruence-on-em
 (implies
      (bit-equiv em em-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em-equiv ts
                             et ne res1 wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-ts

(defthm cr0bits$inline-of-bfix-ts
  (equal (cr0bits$inline pe mp em (bfix ts)
                         et ne res1 wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-ts

(defthm cr0bits$inline-bit-equiv-congruence-on-ts
 (implies
      (bit-equiv ts ts-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts-equiv
                             et ne res1 wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-et

(defthm cr0bits$inline-of-bfix-et
  (equal (cr0bits$inline pe mp em ts (bfix et)
                         ne res1 wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-et

(defthm cr0bits$inline-bit-equiv-congruence-on-et
 (implies
      (bit-equiv et et-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et-equiv
                             ne res1 wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-ne

(defthm cr0bits$inline-of-bfix-ne
  (equal (cr0bits$inline pe mp em ts et (bfix ne)
                         res1 wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-ne

(defthm cr0bits$inline-bit-equiv-congruence-on-ne
 (implies
      (bit-equiv ne ne-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne-equiv
                             res1 wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-10bits-fix-res1

(defthm cr0bits$inline-of-10bits-fix-res1
  (equal (cr0bits$inline pe mp em ts et ne (10bits-fix res1)
                         wp res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-10bits-equiv-congruence-on-res1

(defthm cr0bits$inline-10bits-equiv-congruence-on-res1
 (implies
      (10bits-equiv res1 res1-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1-equiv wp res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-wp

(defthm cr0bits$inline-of-bfix-wp
  (equal (cr0bits$inline pe mp em ts et ne res1 (bfix wp)
                         res2 am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-wp

(defthm cr0bits$inline-bit-equiv-congruence-on-wp
 (implies
      (bit-equiv wp wp-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp-equiv res2 am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-res2

(defthm cr0bits$inline-of-bfix-res2
  (equal (cr0bits$inline pe mp em ts et ne res1 wp (bfix res2)
                         am res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-res2

(defthm cr0bits$inline-bit-equiv-congruence-on-res2
 (implies
      (bit-equiv res2 res2-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp res2-equiv am res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-am

(defthm cr0bits$inline-of-bfix-am
  (equal (cr0bits$inline pe mp em ts et ne res1 wp res2 (bfix am)
                         res3 nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-am

(defthm cr0bits$inline-bit-equiv-congruence-on-am
 (implies
      (bit-equiv am am-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp res2 am-equiv res3 nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-10bits-fix-res3

(defthm cr0bits$inline-of-10bits-fix-res3
  (equal (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am (10bits-fix res3)
                         nw cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-10bits-equiv-congruence-on-res3

(defthm cr0bits$inline-10bits-equiv-congruence-on-res3
 (implies
      (10bits-equiv res3 res3-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp res2 am res3-equiv nw cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-nw

(defthm cr0bits$inline-of-bfix-nw
  (equal (cr0bits$inline pe mp em
                         ts et ne res1 wp res2 am res3 (bfix nw)
                         cd pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-nw

(defthm cr0bits$inline-bit-equiv-congruence-on-nw
 (implies
      (bit-equiv nw nw-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp res2 am res3 nw-equiv cd pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-cd

(defthm cr0bits$inline-of-bfix-cd
  (equal (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw (bfix cd)
                         pg)
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-cd

(defthm cr0bits$inline-bit-equiv-congruence-on-cd
 (implies
      (bit-equiv cd cd-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp res2 am res3 nw cd-equiv pg)))
 :rule-classes :congruence)

Theorem: cr0bits$inline-of-bfix-pg

(defthm cr0bits$inline-of-bfix-pg
  (equal (cr0bits$inline pe mp em ts et
                         ne res1 wp res2 am res3 nw cd (bfix pg))
         (cr0bits$inline pe mp em ts
                         et ne res1 wp res2 am res3 nw cd pg)))

Theorem: cr0bits$inline-bit-equiv-congruence-on-pg

(defthm cr0bits$inline-bit-equiv-congruence-on-pg
 (implies
      (bit-equiv pg pg-equiv)
      (equal (cr0bits$inline pe mp em
                             ts et ne res1 wp res2 am res3 nw cd pg)
             (cr0bits$inline pe mp em ts et ne
                             res1 wp res2 am res3 nw cd pg-equiv)))
 :rule-classes :congruence)

Function: cr0bits-equiv-under-mask$inline

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

Function: cr0bits->pe$inline

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

Theorem: bitp-of-cr0bits->pe

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

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

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

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

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

Theorem: cr0bits->pe-of-cr0bits

(defthm cr0bits->pe-of-cr0bits
 (equal
      (cr0bits->pe (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix pe)))

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

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

Function: cr0bits->mp$inline

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

Theorem: bitp-of-cr0bits->mp

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

Theorem: cr0bits->mp$inline-of-cr0bits-fix-x

(defthm cr0bits->mp$inline-of-cr0bits-fix-x
  (equal (cr0bits->mp$inline (cr0bits-fix x))
         (cr0bits->mp$inline x)))

Theorem: cr0bits->mp$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->mp-of-cr0bits

(defthm cr0bits->mp-of-cr0bits
 (equal
      (cr0bits->mp (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix mp)))

Theorem: cr0bits->mp-of-write-with-mask

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

Function: cr0bits->em$inline

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

Theorem: bitp-of-cr0bits->em

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

Theorem: cr0bits->em$inline-of-cr0bits-fix-x

(defthm cr0bits->em$inline-of-cr0bits-fix-x
  (equal (cr0bits->em$inline (cr0bits-fix x))
         (cr0bits->em$inline x)))

Theorem: cr0bits->em$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->em-of-cr0bits

(defthm cr0bits->em-of-cr0bits
 (equal
      (cr0bits->em (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix em)))

Theorem: cr0bits->em-of-write-with-mask

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

Function: cr0bits->ts$inline

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

Theorem: bitp-of-cr0bits->ts

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

Theorem: cr0bits->ts$inline-of-cr0bits-fix-x

(defthm cr0bits->ts$inline-of-cr0bits-fix-x
  (equal (cr0bits->ts$inline (cr0bits-fix x))
         (cr0bits->ts$inline x)))

Theorem: cr0bits->ts$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->ts-of-cr0bits

(defthm cr0bits->ts-of-cr0bits
 (equal
      (cr0bits->ts (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix ts)))

Theorem: cr0bits->ts-of-write-with-mask

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

Function: cr0bits->et$inline

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

Theorem: bitp-of-cr0bits->et

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

Theorem: cr0bits->et$inline-of-cr0bits-fix-x

(defthm cr0bits->et$inline-of-cr0bits-fix-x
  (equal (cr0bits->et$inline (cr0bits-fix x))
         (cr0bits->et$inline x)))

Theorem: cr0bits->et$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->et-of-cr0bits

(defthm cr0bits->et-of-cr0bits
 (equal
      (cr0bits->et (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix et)))

Theorem: cr0bits->et-of-write-with-mask

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

Function: cr0bits->ne$inline

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

Theorem: bitp-of-cr0bits->ne

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

Theorem: cr0bits->ne$inline-of-cr0bits-fix-x

(defthm cr0bits->ne$inline-of-cr0bits-fix-x
  (equal (cr0bits->ne$inline (cr0bits-fix x))
         (cr0bits->ne$inline x)))

Theorem: cr0bits->ne$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->ne-of-cr0bits

(defthm cr0bits->ne-of-cr0bits
 (equal
      (cr0bits->ne (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix ne)))

Theorem: cr0bits->ne-of-write-with-mask

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

Function: cr0bits->res1$inline

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

Theorem: 10bits-p-of-cr0bits->res1

(defthm 10bits-p-of-cr0bits->res1
  (b* ((res1 (cr0bits->res1$inline x)))
    (10bits-p res1))
  :rule-classes :rewrite)

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

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

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

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

Theorem: cr0bits->res1-of-cr0bits

(defthm cr0bits->res1-of-cr0bits
 (equal
    (cr0bits->res1 (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
    (10bits-fix res1)))

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

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

Function: cr0bits->wp$inline

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

Theorem: bitp-of-cr0bits->wp

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

Theorem: cr0bits->wp$inline-of-cr0bits-fix-x

(defthm cr0bits->wp$inline-of-cr0bits-fix-x
  (equal (cr0bits->wp$inline (cr0bits-fix x))
         (cr0bits->wp$inline x)))

Theorem: cr0bits->wp$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->wp-of-cr0bits

(defthm cr0bits->wp-of-cr0bits
 (equal
      (cr0bits->wp (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix wp)))

Theorem: cr0bits->wp-of-write-with-mask

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

Function: cr0bits->res2$inline

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

Theorem: bitp-of-cr0bits->res2

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

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

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

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

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

Theorem: cr0bits->res2-of-cr0bits

(defthm cr0bits->res2-of-cr0bits
 (equal
    (cr0bits->res2 (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
    (bfix res2)))

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

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

Function: cr0bits->am$inline

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

Theorem: bitp-of-cr0bits->am

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

Theorem: cr0bits->am$inline-of-cr0bits-fix-x

(defthm cr0bits->am$inline-of-cr0bits-fix-x
  (equal (cr0bits->am$inline (cr0bits-fix x))
         (cr0bits->am$inline x)))

Theorem: cr0bits->am$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->am-of-cr0bits

(defthm cr0bits->am-of-cr0bits
 (equal
      (cr0bits->am (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix am)))

Theorem: cr0bits->am-of-write-with-mask

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

Function: cr0bits->res3$inline

(defun cr0bits->res3$inline (x)
  (declare (xargs :guard (cr0bits-p x)))
  (mbe :logic
       (let ((x (cr0bits-fix x)))
         (part-select x :low 19 :width 10))
       :exec (the (unsigned-byte 10)
                  (logand (the (unsigned-byte 10) 1023)
                          (the (unsigned-byte 13)
                               (ash (the (unsigned-byte 32) x)
                                    -19))))))

Theorem: 10bits-p-of-cr0bits->res3

(defthm 10bits-p-of-cr0bits->res3
  (b* ((res3 (cr0bits->res3$inline x)))
    (10bits-p res3))
  :rule-classes :rewrite)

Theorem: cr0bits->res3$inline-of-cr0bits-fix-x

(defthm cr0bits->res3$inline-of-cr0bits-fix-x
  (equal (cr0bits->res3$inline (cr0bits-fix x))
         (cr0bits->res3$inline x)))

Theorem: cr0bits->res3$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->res3-of-cr0bits

(defthm cr0bits->res3-of-cr0bits
 (equal
    (cr0bits->res3 (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
    (10bits-fix res3)))

Theorem: cr0bits->res3-of-write-with-mask

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

Function: cr0bits->nw$inline

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

Theorem: bitp-of-cr0bits->nw

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

Theorem: cr0bits->nw$inline-of-cr0bits-fix-x

(defthm cr0bits->nw$inline-of-cr0bits-fix-x
  (equal (cr0bits->nw$inline (cr0bits-fix x))
         (cr0bits->nw$inline x)))

Theorem: cr0bits->nw$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->nw-of-cr0bits

(defthm cr0bits->nw-of-cr0bits
 (equal
      (cr0bits->nw (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix nw)))

Theorem: cr0bits->nw-of-write-with-mask

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

Function: cr0bits->cd$inline

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

Theorem: bitp-of-cr0bits->cd

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

Theorem: cr0bits->cd$inline-of-cr0bits-fix-x

(defthm cr0bits->cd$inline-of-cr0bits-fix-x
  (equal (cr0bits->cd$inline (cr0bits-fix x))
         (cr0bits->cd$inline x)))

Theorem: cr0bits->cd$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->cd-of-cr0bits

(defthm cr0bits->cd-of-cr0bits
 (equal
      (cr0bits->cd (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix cd)))

Theorem: cr0bits->cd-of-write-with-mask

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

Function: cr0bits->pg$inline

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

Theorem: bitp-of-cr0bits->pg

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

Theorem: cr0bits->pg$inline-of-cr0bits-fix-x

(defthm cr0bits->pg$inline-of-cr0bits-fix-x
  (equal (cr0bits->pg$inline (cr0bits-fix x))
         (cr0bits->pg$inline x)))

Theorem: cr0bits->pg$inline-cr0bits-equiv-congruence-on-x

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

Theorem: cr0bits->pg-of-cr0bits

(defthm cr0bits->pg-of-cr0bits
 (equal
      (cr0bits->pg (cr0bits pe mp em
                            ts et ne res1 wp res2 am res3 nw cd pg))
      (bfix pg)))

Theorem: cr0bits->pg-of-write-with-mask

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

Theorem: cr0bits-fix-in-terms-of-cr0bits

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

Function: !cr0bits->pe$inline

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

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

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

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

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

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

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

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

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

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

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

Theorem: !cr0bits->pe-is-cr0bits

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

Theorem: cr0bits->pe-of-!cr0bits->pe

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

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

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

Function: !cr0bits->mp$inline

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

Theorem: cr0bits-p-of-!cr0bits->mp

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

Theorem: !cr0bits->mp$inline-of-bfix-mp

(defthm !cr0bits->mp$inline-of-bfix-mp
  (equal (!cr0bits->mp$inline (bfix mp) x)
         (!cr0bits->mp$inline mp x)))

Theorem: !cr0bits->mp$inline-bit-equiv-congruence-on-mp

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

Theorem: !cr0bits->mp$inline-of-cr0bits-fix-x

(defthm !cr0bits->mp$inline-of-cr0bits-fix-x
  (equal (!cr0bits->mp$inline mp (cr0bits-fix x))
         (!cr0bits->mp$inline mp x)))

Theorem: !cr0bits->mp$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->mp-is-cr0bits

(defthm !cr0bits->mp-is-cr0bits
  (equal (!cr0bits->mp mp x)
         (change-cr0bits x :mp mp)))

Theorem: cr0bits->mp-of-!cr0bits->mp

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

Theorem: !cr0bits->mp-equiv-under-mask

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

Function: !cr0bits->em$inline

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

Theorem: cr0bits-p-of-!cr0bits->em

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

Theorem: !cr0bits->em$inline-of-bfix-em

(defthm !cr0bits->em$inline-of-bfix-em
  (equal (!cr0bits->em$inline (bfix em) x)
         (!cr0bits->em$inline em x)))

Theorem: !cr0bits->em$inline-bit-equiv-congruence-on-em

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

Theorem: !cr0bits->em$inline-of-cr0bits-fix-x

(defthm !cr0bits->em$inline-of-cr0bits-fix-x
  (equal (!cr0bits->em$inline em (cr0bits-fix x))
         (!cr0bits->em$inline em x)))

Theorem: !cr0bits->em$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->em-is-cr0bits

(defthm !cr0bits->em-is-cr0bits
  (equal (!cr0bits->em em x)
         (change-cr0bits x :em em)))

Theorem: cr0bits->em-of-!cr0bits->em

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

Theorem: !cr0bits->em-equiv-under-mask

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

Function: !cr0bits->ts$inline

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

Theorem: cr0bits-p-of-!cr0bits->ts

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

Theorem: !cr0bits->ts$inline-of-bfix-ts

(defthm !cr0bits->ts$inline-of-bfix-ts
  (equal (!cr0bits->ts$inline (bfix ts) x)
         (!cr0bits->ts$inline ts x)))

Theorem: !cr0bits->ts$inline-bit-equiv-congruence-on-ts

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

Theorem: !cr0bits->ts$inline-of-cr0bits-fix-x

(defthm !cr0bits->ts$inline-of-cr0bits-fix-x
  (equal (!cr0bits->ts$inline ts (cr0bits-fix x))
         (!cr0bits->ts$inline ts x)))

Theorem: !cr0bits->ts$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->ts-is-cr0bits

(defthm !cr0bits->ts-is-cr0bits
  (equal (!cr0bits->ts ts x)
         (change-cr0bits x :ts ts)))

Theorem: cr0bits->ts-of-!cr0bits->ts

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

Theorem: !cr0bits->ts-equiv-under-mask

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

Function: !cr0bits->et$inline

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

Theorem: cr0bits-p-of-!cr0bits->et

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

Theorem: !cr0bits->et$inline-of-bfix-et

(defthm !cr0bits->et$inline-of-bfix-et
  (equal (!cr0bits->et$inline (bfix et) x)
         (!cr0bits->et$inline et x)))

Theorem: !cr0bits->et$inline-bit-equiv-congruence-on-et

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

Theorem: !cr0bits->et$inline-of-cr0bits-fix-x

(defthm !cr0bits->et$inline-of-cr0bits-fix-x
  (equal (!cr0bits->et$inline et (cr0bits-fix x))
         (!cr0bits->et$inline et x)))

Theorem: !cr0bits->et$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->et-is-cr0bits

(defthm !cr0bits->et-is-cr0bits
  (equal (!cr0bits->et et x)
         (change-cr0bits x :et et)))

Theorem: cr0bits->et-of-!cr0bits->et

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

Theorem: !cr0bits->et-equiv-under-mask

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

Function: !cr0bits->ne$inline

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

Theorem: cr0bits-p-of-!cr0bits->ne

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

Theorem: !cr0bits->ne$inline-of-bfix-ne

(defthm !cr0bits->ne$inline-of-bfix-ne
  (equal (!cr0bits->ne$inline (bfix ne) x)
         (!cr0bits->ne$inline ne x)))

Theorem: !cr0bits->ne$inline-bit-equiv-congruence-on-ne

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

Theorem: !cr0bits->ne$inline-of-cr0bits-fix-x

(defthm !cr0bits->ne$inline-of-cr0bits-fix-x
  (equal (!cr0bits->ne$inline ne (cr0bits-fix x))
         (!cr0bits->ne$inline ne x)))

Theorem: !cr0bits->ne$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->ne-is-cr0bits

(defthm !cr0bits->ne-is-cr0bits
  (equal (!cr0bits->ne ne x)
         (change-cr0bits x :ne ne)))

Theorem: cr0bits->ne-of-!cr0bits->ne

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

Theorem: !cr0bits->ne-equiv-under-mask

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

Function: !cr0bits->res1$inline

(defun !cr0bits->res1$inline (res1 x)
 (declare (xargs :guard (and (10bits-p res1) (cr0bits-p x))))
 (mbe
     :logic
     (b* ((res1 (mbe :logic (10bits-fix res1)
                     :exec res1))
          (x (cr0bits-fix x)))
       (part-install res1 x :width 10 :low 6))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 17) -65473)))
                        (the (unsigned-byte 16)
                             (ash (the (unsigned-byte 10) res1)
                                  6))))))

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

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

Theorem: !cr0bits->res1$inline-of-10bits-fix-res1

(defthm !cr0bits->res1$inline-of-10bits-fix-res1
  (equal (!cr0bits->res1$inline (10bits-fix res1)
                                x)
         (!cr0bits->res1$inline res1 x)))

Theorem: !cr0bits->res1$inline-10bits-equiv-congruence-on-res1

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

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

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

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

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

Theorem: !cr0bits->res1-is-cr0bits

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

Theorem: cr0bits->res1-of-!cr0bits->res1

(defthm cr0bits->res1-of-!cr0bits->res1
  (b* ((?new-x (!cr0bits->res1$inline res1 x)))
    (equal (cr0bits->res1 new-x)
           (10bits-fix res1))))

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

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

Function: !cr0bits->wp$inline

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

Theorem: cr0bits-p-of-!cr0bits->wp

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

Theorem: !cr0bits->wp$inline-of-bfix-wp

(defthm !cr0bits->wp$inline-of-bfix-wp
  (equal (!cr0bits->wp$inline (bfix wp) x)
         (!cr0bits->wp$inline wp x)))

Theorem: !cr0bits->wp$inline-bit-equiv-congruence-on-wp

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

Theorem: !cr0bits->wp$inline-of-cr0bits-fix-x

(defthm !cr0bits->wp$inline-of-cr0bits-fix-x
  (equal (!cr0bits->wp$inline wp (cr0bits-fix x))
         (!cr0bits->wp$inline wp x)))

Theorem: !cr0bits->wp$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->wp-is-cr0bits

(defthm !cr0bits->wp-is-cr0bits
  (equal (!cr0bits->wp wp x)
         (change-cr0bits x :wp wp)))

Theorem: cr0bits->wp-of-!cr0bits->wp

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

Theorem: !cr0bits->wp-equiv-under-mask

(defthm !cr0bits->wp-equiv-under-mask
  (b* ((?new-x (!cr0bits->wp$inline wp x)))
    (cr0bits-equiv-under-mask new-x x -65537)))

Function: !cr0bits->res2$inline

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

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

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

Theorem: !cr0bits->res2$inline-of-bfix-res2

(defthm !cr0bits->res2$inline-of-bfix-res2
  (equal (!cr0bits->res2$inline (bfix res2) x)
         (!cr0bits->res2$inline res2 x)))

Theorem: !cr0bits->res2$inline-bit-equiv-congruence-on-res2

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

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

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

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

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

Theorem: !cr0bits->res2-is-cr0bits

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

Theorem: cr0bits->res2-of-!cr0bits->res2

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

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

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

Function: !cr0bits->am$inline

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

Theorem: cr0bits-p-of-!cr0bits->am

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

Theorem: !cr0bits->am$inline-of-bfix-am

(defthm !cr0bits->am$inline-of-bfix-am
  (equal (!cr0bits->am$inline (bfix am) x)
         (!cr0bits->am$inline am x)))

Theorem: !cr0bits->am$inline-bit-equiv-congruence-on-am

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

Theorem: !cr0bits->am$inline-of-cr0bits-fix-x

(defthm !cr0bits->am$inline-of-cr0bits-fix-x
  (equal (!cr0bits->am$inline am (cr0bits-fix x))
         (!cr0bits->am$inline am x)))

Theorem: !cr0bits->am$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->am-is-cr0bits

(defthm !cr0bits->am-is-cr0bits
  (equal (!cr0bits->am am x)
         (change-cr0bits x :am am)))

Theorem: cr0bits->am-of-!cr0bits->am

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

Theorem: !cr0bits->am-equiv-under-mask

(defthm !cr0bits->am-equiv-under-mask
  (b* ((?new-x (!cr0bits->am$inline am x)))
    (cr0bits-equiv-under-mask new-x x -262145)))

Function: !cr0bits->res3$inline

(defun !cr0bits->res3$inline (res3 x)
  (declare (xargs :guard (and (10bits-p res3) (cr0bits-p x))))
  (mbe :logic
       (b* ((res3 (mbe :logic (10bits-fix res3)
                       :exec res3))
            (x (cr0bits-fix x)))
         (part-install res3 x :width 10 :low 19))
       :exec
       (the (unsigned-byte 32)
            (logior (the (unsigned-byte 32)
                         (logand (the (unsigned-byte 32) x)
                                 (the (signed-byte 30) -536346625)))
                    (the (unsigned-byte 29)
                         (ash (the (unsigned-byte 10) res3)
                              19))))))

Theorem: cr0bits-p-of-!cr0bits->res3

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

Theorem: !cr0bits->res3$inline-of-10bits-fix-res3

(defthm !cr0bits->res3$inline-of-10bits-fix-res3
  (equal (!cr0bits->res3$inline (10bits-fix res3)
                                x)
         (!cr0bits->res3$inline res3 x)))

Theorem: !cr0bits->res3$inline-10bits-equiv-congruence-on-res3

(defthm !cr0bits->res3$inline-10bits-equiv-congruence-on-res3
  (implies (10bits-equiv res3 res3-equiv)
           (equal (!cr0bits->res3$inline res3 x)
                  (!cr0bits->res3$inline res3-equiv x)))
  :rule-classes :congruence)

Theorem: !cr0bits->res3$inline-of-cr0bits-fix-x

(defthm !cr0bits->res3$inline-of-cr0bits-fix-x
  (equal (!cr0bits->res3$inline res3 (cr0bits-fix x))
         (!cr0bits->res3$inline res3 x)))

Theorem: !cr0bits->res3$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->res3-is-cr0bits

(defthm !cr0bits->res3-is-cr0bits
  (equal (!cr0bits->res3 res3 x)
         (change-cr0bits x :res3 res3)))

Theorem: cr0bits->res3-of-!cr0bits->res3

(defthm cr0bits->res3-of-!cr0bits->res3
  (b* ((?new-x (!cr0bits->res3$inline res3 x)))
    (equal (cr0bits->res3 new-x)
           (10bits-fix res3))))

Theorem: !cr0bits->res3-equiv-under-mask

(defthm !cr0bits->res3-equiv-under-mask
  (b* ((?new-x (!cr0bits->res3$inline res3 x)))
    (cr0bits-equiv-under-mask new-x x -536346625)))

Function: !cr0bits->nw$inline

(defun !cr0bits->nw$inline (nw x)
  (declare (xargs :guard (and (bitp nw) (cr0bits-p x))))
  (mbe :logic
       (b* ((nw (mbe :logic (bfix nw) :exec nw))
            (x (cr0bits-fix x)))
         (part-install nw x :width 1 :low 29))
       :exec
       (the (unsigned-byte 32)
            (logior (the (unsigned-byte 32)
                         (logand (the (unsigned-byte 32) x)
                                 (the (signed-byte 31) -536870913)))
                    (the (unsigned-byte 30)
                         (ash (the (unsigned-byte 1) nw) 29))))))

Theorem: cr0bits-p-of-!cr0bits->nw

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

Theorem: !cr0bits->nw$inline-of-bfix-nw

(defthm !cr0bits->nw$inline-of-bfix-nw
  (equal (!cr0bits->nw$inline (bfix nw) x)
         (!cr0bits->nw$inline nw x)))

Theorem: !cr0bits->nw$inline-bit-equiv-congruence-on-nw

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

Theorem: !cr0bits->nw$inline-of-cr0bits-fix-x

(defthm !cr0bits->nw$inline-of-cr0bits-fix-x
  (equal (!cr0bits->nw$inline nw (cr0bits-fix x))
         (!cr0bits->nw$inline nw x)))

Theorem: !cr0bits->nw$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->nw-is-cr0bits

(defthm !cr0bits->nw-is-cr0bits
  (equal (!cr0bits->nw nw x)
         (change-cr0bits x :nw nw)))

Theorem: cr0bits->nw-of-!cr0bits->nw

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

Theorem: !cr0bits->nw-equiv-under-mask

(defthm !cr0bits->nw-equiv-under-mask
  (b* ((?new-x (!cr0bits->nw$inline nw x)))
    (cr0bits-equiv-under-mask new-x x -536870913)))

Function: !cr0bits->cd$inline

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

Theorem: cr0bits-p-of-!cr0bits->cd

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

Theorem: !cr0bits->cd$inline-of-bfix-cd

(defthm !cr0bits->cd$inline-of-bfix-cd
  (equal (!cr0bits->cd$inline (bfix cd) x)
         (!cr0bits->cd$inline cd x)))

Theorem: !cr0bits->cd$inline-bit-equiv-congruence-on-cd

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

Theorem: !cr0bits->cd$inline-of-cr0bits-fix-x

(defthm !cr0bits->cd$inline-of-cr0bits-fix-x
  (equal (!cr0bits->cd$inline cd (cr0bits-fix x))
         (!cr0bits->cd$inline cd x)))

Theorem: !cr0bits->cd$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->cd-is-cr0bits

(defthm !cr0bits->cd-is-cr0bits
  (equal (!cr0bits->cd cd x)
         (change-cr0bits x :cd cd)))

Theorem: cr0bits->cd-of-!cr0bits->cd

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

Theorem: !cr0bits->cd-equiv-under-mask

(defthm !cr0bits->cd-equiv-under-mask
  (b* ((?new-x (!cr0bits->cd$inline cd x)))
    (cr0bits-equiv-under-mask new-x x -1073741825)))

Function: !cr0bits->pg$inline

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

Theorem: cr0bits-p-of-!cr0bits->pg

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

Theorem: !cr0bits->pg$inline-of-bfix-pg

(defthm !cr0bits->pg$inline-of-bfix-pg
  (equal (!cr0bits->pg$inline (bfix pg) x)
         (!cr0bits->pg$inline pg x)))

Theorem: !cr0bits->pg$inline-bit-equiv-congruence-on-pg

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

Theorem: !cr0bits->pg$inline-of-cr0bits-fix-x

(defthm !cr0bits->pg$inline-of-cr0bits-fix-x
  (equal (!cr0bits->pg$inline pg (cr0bits-fix x))
         (!cr0bits->pg$inline pg x)))

Theorem: !cr0bits->pg$inline-cr0bits-equiv-congruence-on-x

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

Theorem: !cr0bits->pg-is-cr0bits

(defthm !cr0bits->pg-is-cr0bits
  (equal (!cr0bits->pg pg x)
         (change-cr0bits x :pg pg)))

Theorem: cr0bits->pg-of-!cr0bits->pg

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

Theorem: !cr0bits->pg-equiv-under-mask

(defthm !cr0bits->pg-equiv-under-mask
  (b* ((?new-x (!cr0bits->pg$inline pg x)))
    (cr0bits-equiv-under-mask new-x x 2147483647)))

Function: cr0bits-debug$inline

(defun cr0bits-debug$inline (x)
 (declare (xargs :guard (cr0bits-p x)))
 (b* (((cr0bits x)))
  (cons
   (cons 'pe x.pe)
   (cons
    (cons 'mp x.mp)
    (cons
     (cons 'em x.em)
     (cons
      (cons 'ts x.ts)
      (cons
       (cons 'et x.et)
       (cons
        (cons 'ne x.ne)
        (cons
         (cons 'res1 x.res1)
         (cons
             (cons 'wp x.wp)
             (cons (cons 'res2 x.res2)
                   (cons (cons 'am x.am)
                         (cons (cons 'res3 x.res3)
                               (cons (cons 'nw x.nw)
                                     (cons (cons 'cd x.cd)
                                           (cons (cons 'pg x.pg)
                                                 nil))))))))))))))))

Subtopics

Cr0bits-p: Recognizer for cr0bits bit structures.
!cr0bits->res3: Update the |X86ISA|::|RES3| field of a cr0bits bit structure.
!cr0bits->res1: Update the |X86ISA|::|RES1| field of a cr0bits bit structure.
!cr0bits->res2: Update the |X86ISA|::|RES2| field of a cr0bits bit structure.
!cr0bits->nw: Update the |X86ISA|::|NW| field of a cr0bits bit structure.
!cr0bits->wp: Update the |X86ISA|::|WP| field of a cr0bits bit structure.
!cr0bits->ts: Update the |X86ISA|::|TS| field of a cr0bits bit structure.
!cr0bits->pg: Update the |X86ISA|::|PG| field of a cr0bits bit structure.
!cr0bits->pe: Update the |ACL2|::|PE| field of a cr0bits bit structure.
!cr0bits->ne: Update the |X86ISA|::|NE| field of a cr0bits bit structure.
!cr0bits->mp: Update the |X86ISA|::|MP| field of a cr0bits bit structure.
!cr0bits->et: Update the |X86ISA|::|ET| field of a cr0bits bit structure.
!cr0bits->em: Update the |X86ISA|::|EM| field of a cr0bits bit structure.
!cr0bits->cd: Update the |X86ISA|::|CD| field of a cr0bits bit structure.
!cr0bits->am: Update the |X86ISA|::|AM| field of a cr0bits bit structure.
Cr0bits->res3: Access the |X86ISA|::|RES3| field of a cr0bits bit structure.
Cr0bits->res2: Access the |X86ISA|::|RES2| field of a cr0bits bit structure.
Cr0bits->res1: Access the |X86ISA|::|RES1| field of a cr0bits bit structure.
Cr0bits-fix: Fixing function for cr0bits bit structures.
Cr0bits->wp: Access the |X86ISA|::|WP| field of a cr0bits bit structure.
Cr0bits->ts: Access the |X86ISA|::|TS| field of a cr0bits bit structure.
Cr0bits->pg: Access the |X86ISA|::|PG| field of a cr0bits bit structure.
Cr0bits->nw: Access the |X86ISA|::|NW| field of a cr0bits bit structure.
Cr0bits->ne: Access the |X86ISA|::|NE| field of a cr0bits bit structure.
Cr0bits->mp: Access the |X86ISA|::|MP| field of a cr0bits bit structure.
Cr0bits->et: Access the |X86ISA|::|ET| field of a cr0bits bit structure.
Cr0bits->em: Access the |X86ISA|::|EM| field of a cr0bits bit structure.
Cr0bits->cd: Access the |X86ISA|::|CD| field of a cr0bits bit structure.
Cr0bits->am: Access the |X86ISA|::|AM| field of a cr0bits bit structure.
Cr0bits->pe: Access the |ACL2|::|PE| field of a cr0bits bit structure.