		Search-engine friendly clone of the ACL2 documentation.

Structures

Rflagsbits

An 32-bit unsigned bitstruct type.

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

Fields

cf — bit
res1 — bit
pf — bit
res2 — bit
af — bit
res3 — bit
zf — bit
sf — bit
tf — bit
intf — bit
df — bit
of — bit
iopl — 2bits
nt — bit
res4 — bit
rf — bit
vm — bit
ac — bit
vif — bit
vip — bit
id — bit
res5 — 10bits

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

Definitions and Theorems

Function: rflagsbits-p$inline

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

Theorem: rflagsbits-p-when-unsigned-byte-p

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

Theorem: unsigned-byte-p-when-rflagsbits-p

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

Theorem: rflagsbits-p-compound-recognizer

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

Function: rflagsbits-fix$inline

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

Theorem: rflagsbits-p-of-rflagsbits-fix

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

Theorem: rflagsbits-fix-when-rflagsbits-p

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

Function: rflagsbits-equiv$inline

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

Theorem: rflagsbits-equiv-is-an-equivalence

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

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

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

Theorem: rflagsbits-fix-under-rflagsbits-equiv

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

Function: rflagsbits$inline

(defun rflagsbits$inline
       (cf res1 pf res2 af res3 zf sf tf intf df of
           iopl nt res4 rf vm ac vif vip id res5)
 (declare (xargs :guard (and (bitp cf)
                             (bitp res1)
                             (bitp pf)
                             (bitp res2)
                             (bitp af)
                             (bitp res3)
                             (bitp zf)
                             (bitp sf)
                             (bitp tf)
                             (bitp intf)
                             (bitp df)
                             (bitp of)
                             (2bits-p iopl)
                             (bitp nt)
                             (bitp res4)
                             (bitp rf)
                             (bitp vm)
                             (bitp ac)
                             (bitp vif)
                             (bitp vip)
                             (bitp id)
                             (10bits-p res5))))
 (b* ((cf (mbe :logic (bfix cf) :exec cf))
      (res1 (mbe :logic (bfix res1) :exec res1))
      (pf (mbe :logic (bfix pf) :exec pf))
      (res2 (mbe :logic (bfix res2) :exec res2))
      (af (mbe :logic (bfix af) :exec af))
      (res3 (mbe :logic (bfix res3) :exec res3))
      (zf (mbe :logic (bfix zf) :exec zf))
      (sf (mbe :logic (bfix sf) :exec sf))
      (tf (mbe :logic (bfix tf) :exec tf))
      (intf (mbe :logic (bfix intf) :exec intf))
      (df (mbe :logic (bfix df) :exec df))
      (of (mbe :logic (bfix of) :exec of))
      (iopl (mbe :logic (2bits-fix iopl)
                 :exec iopl))
      (nt (mbe :logic (bfix nt) :exec nt))
      (res4 (mbe :logic (bfix res4) :exec res4))
      (rf (mbe :logic (bfix rf) :exec rf))
      (vm (mbe :logic (bfix vm) :exec vm))
      (ac (mbe :logic (bfix ac) :exec ac))
      (vif (mbe :logic (bfix vif) :exec vif))
      (vip (mbe :logic (bfix vip) :exec vip))
      (id (mbe :logic (bfix id) :exec id))
      (res5 (mbe :logic (10bits-fix res5)
                 :exec res5)))
  (logapp
   1 cf
   (logapp
    1 res1
    (logapp
     1 pf
     (logapp
      1 res2
      (logapp
       1 af
       (logapp
        1 res3
        (logapp
         1 zf
         (logapp
          1 sf
          (logapp
           1 tf
           (logapp
            1 intf
            (logapp
             1 df
             (logapp
              1 of
              (logapp
               2 iopl
               (logapp
                1 nt
                (logapp
                 1 res4
                 (logapp
                  1 rf
                  (logapp
                   1 vm
                   (logapp
                    1 ac
                    (logapp
                       1 vif
                       (logapp
                            1 vip
                            (logapp 1 id res5)))))))))))))))))))))))

Theorem: rflagsbits-p-of-rflagsbits

(defthm rflagsbits-p-of-rflagsbits
  (b*
   ((rflagsbits
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
   (rflagsbits-p rflagsbits))
  :rule-classes :rewrite)

Theorem: rflagsbits$inline-of-bfix-cf

(defthm rflagsbits$inline-of-bfix-cf
  (equal (rflagsbits$inline (bfix cf)
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-cf

(defthm rflagsbits$inline-bit-equiv-congruence-on-cf
 (implies
  (bit-equiv cf cf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf-equiv
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-res1

(defthm rflagsbits$inline-of-bfix-res1
  (equal (rflagsbits$inline cf (bfix res1)
                            pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

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

(defthm rflagsbits$inline-bit-equiv-congruence-on-res1
 (implies
  (bit-equiv res1 res1-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1-equiv
                            pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-pf

(defthm rflagsbits$inline-of-bfix-pf
  (equal (rflagsbits$inline cf res1 (bfix pf)
                            res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-pf

(defthm rflagsbits$inline-bit-equiv-congruence-on-pf
 (implies
  (bit-equiv pf pf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf-equiv
                            res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-res2

(defthm rflagsbits$inline-of-bfix-res2
  (equal (rflagsbits$inline cf res1 pf (bfix res2)
                            af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

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

(defthm rflagsbits$inline-bit-equiv-congruence-on-res2
 (implies
  (bit-equiv res2 res2-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2-equiv af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-af

(defthm rflagsbits$inline-of-bfix-af
  (equal (rflagsbits$inline cf res1 pf res2 (bfix af)
                            res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-af

(defthm rflagsbits$inline-bit-equiv-congruence-on-af
 (implies
  (bit-equiv af af-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af-equiv res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-res3

(defthm rflagsbits$inline-of-bfix-res3
  (equal (rflagsbits$inline cf res1 pf res2 af (bfix res3)
                            zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-res3

(defthm rflagsbits$inline-bit-equiv-congruence-on-res3
 (implies
  (bit-equiv res3 res3-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3-equiv zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-zf

(defthm rflagsbits$inline-of-bfix-zf
  (equal (rflagsbits$inline cf res1 pf res2 af res3 (bfix zf)
                            sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-zf

(defthm rflagsbits$inline-bit-equiv-congruence-on-zf
 (implies
  (bit-equiv zf zf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf-equiv sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-sf

(defthm rflagsbits$inline-of-bfix-sf
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf (bfix sf)
                            tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-sf

(defthm rflagsbits$inline-bit-equiv-congruence-on-sf
 (implies
  (bit-equiv sf sf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf-equiv tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-tf

(defthm rflagsbits$inline-of-bfix-tf
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf sf (bfix tf)
                            intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-tf

(defthm rflagsbits$inline-bit-equiv-congruence-on-tf
 (implies
  (bit-equiv tf tf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf-equiv intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-intf

(defthm rflagsbits$inline-of-bfix-intf
  (equal (rflagsbits$inline cf res1
                            pf res2 af res3 zf sf tf (bfix intf)
                            df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-intf

(defthm rflagsbits$inline-bit-equiv-congruence-on-intf
 (implies
  (bit-equiv intf intf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf-equiv df of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-df

(defthm rflagsbits$inline-of-bfix-df
  (equal (rflagsbits$inline cf res1
                            pf res2 af res3 zf sf tf intf (bfix df)
                            of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-df

(defthm rflagsbits$inline-bit-equiv-congruence-on-df
 (implies
  (bit-equiv df df-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df-equiv of
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-of

(defthm rflagsbits$inline-of-bfix-of
  (equal (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df (bfix of)
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-of

(defthm rflagsbits$inline-bit-equiv-congruence-on-of
 (implies
  (bit-equiv of of-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of-equiv
                            iopl nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-2bits-fix-iopl

(defthm rflagsbits$inline-of-2bits-fix-iopl
  (equal (rflagsbits$inline cf res1 pf res2 af res3
                            zf sf tf intf df of (2bits-fix iopl)
                            nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-2bits-equiv-congruence-on-iopl

(defthm rflagsbits$inline-2bits-equiv-congruence-on-iopl
 (implies
  (2bits-equiv iopl iopl-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf res2
                            af res3 zf sf tf intf df of iopl-equiv
                            nt res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-nt

(defthm rflagsbits$inline-of-bfix-nt
  (equal (rflagsbits$inline cf res1 pf res2 af
                            res3 zf sf tf intf df of iopl (bfix nt)
                            res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-nt

(defthm rflagsbits$inline-bit-equiv-congruence-on-nt
 (implies
  (bit-equiv nt nt-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf res2 af
                            res3 zf sf tf intf df of iopl nt-equiv
                            res4 rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-res4

(defthm rflagsbits$inline-of-bfix-res4
  (equal (rflagsbits$inline cf res1 pf res2 af res3
                            zf sf tf intf df of iopl nt (bfix res4)
                            rf vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-res4

(defthm rflagsbits$inline-bit-equiv-congruence-on-res4
 (implies
  (bit-equiv res4 res4-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4-equiv rf vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-rf

(defthm rflagsbits$inline-of-bfix-rf
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf
                            sf tf intf df of iopl nt res4 (bfix rf)
                            vm ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-rf

(defthm rflagsbits$inline-bit-equiv-congruence-on-rf
 (implies
  (bit-equiv rf rf-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf-equiv vm ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-vm

(defthm rflagsbits$inline-of-bfix-vm
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf sf
                            tf intf df of iopl nt res4 rf (bfix vm)
                            ac vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-vm

(defthm rflagsbits$inline-bit-equiv-congruence-on-vm
 (implies
  (bit-equiv vm vm-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf vm-equiv ac vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-ac

(defthm rflagsbits$inline-of-bfix-ac
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf sf tf
                            intf df of iopl nt res4 rf vm (bfix ac)
                            vif vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-ac

(defthm rflagsbits$inline-bit-equiv-congruence-on-ac
 (implies
  (bit-equiv ac ac-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf vm ac-equiv vif vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-vif

(defthm rflagsbits$inline-of-bfix-vif
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf sf tf intf
                            df of iopl nt res4 rf vm ac (bfix vif)
                            vip id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-vif

(defthm rflagsbits$inline-bit-equiv-congruence-on-vif
 (implies
  (bit-equiv vif vif-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf vm ac vif-equiv vip id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-vip

(defthm rflagsbits$inline-of-bfix-vip
  (equal (rflagsbits$inline cf res1 pf res2 af res3 zf sf tf intf df
                            of iopl nt res4 rf vm ac vif (bfix vip)
                            id res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-vip

(defthm rflagsbits$inline-bit-equiv-congruence-on-vip
 (implies
  (bit-equiv vip vip-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf vm ac vif vip-equiv id res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-bfix-id

(defthm rflagsbits$inline-of-bfix-id
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip (bfix id)
                            res5)
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-bit-equiv-congruence-on-id

(defthm rflagsbits$inline-bit-equiv-congruence-on-id
 (implies
  (bit-equiv id id-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf vm ac vif vip id-equiv res5)))
 :rule-classes :congruence)

Theorem: rflagsbits$inline-of-10bits-fix-res5

(defthm rflagsbits$inline-of-10bits-fix-res5
  (equal (rflagsbits$inline cf res1 pf res2
                            af res3 zf sf tf intf df of iopl nt res4
                            rf vm ac vif vip id (10bits-fix res5))
         (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)))

Theorem: rflagsbits$inline-10bits-equiv-congruence-on-res5

(defthm rflagsbits$inline-10bits-equiv-congruence-on-res5
 (implies
  (10bits-equiv res5 res5-equiv)
  (equal (rflagsbits$inline cf
                            res1 pf res2 af res3 zf sf tf intf df of
                            iopl nt res4 rf vm ac vif vip id res5)
         (rflagsbits$inline cf res1 pf
                            res2 af res3 zf sf tf intf df of iopl nt
                            res4 rf vm ac vif vip id res5-equiv)))
 :rule-classes :congruence)

Function: rflagsbits-equiv-under-mask$inline

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

Function: rflagsbits->cf$inline

(defun rflagsbits->cf$inline (x)
  (declare (xargs :guard (rflagsbits-p x)))
  (mbe :logic
       (let ((x (rflagsbits-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-rflagsbits->cf

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

Theorem: rflagsbits->cf$inline-of-rflagsbits-fix-x

(defthm rflagsbits->cf$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->cf$inline (rflagsbits-fix x))
         (rflagsbits->cf$inline x)))

Theorem: rflagsbits->cf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->cf-of-rflagsbits

(defthm rflagsbits->cf-of-rflagsbits
  (equal (rflagsbits->cf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix cf)))

Theorem: rflagsbits->cf-of-write-with-mask

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

Function: rflagsbits->res1$inline

(defun rflagsbits->res1$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (mbe
    :logic
    (let ((x (rflagsbits-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-rflagsbits->res1

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

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

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

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

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

Theorem: rflagsbits->res1-of-rflagsbits

(defthm rflagsbits->res1-of-rflagsbits
  (equal (rflagsbits->res1
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix res1)))

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

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

Function: rflagsbits->pf$inline

(defun rflagsbits->pf$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (mbe
    :logic
    (let ((x (rflagsbits-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-rflagsbits->pf

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

Theorem: rflagsbits->pf$inline-of-rflagsbits-fix-x

(defthm rflagsbits->pf$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->pf$inline (rflagsbits-fix x))
         (rflagsbits->pf$inline x)))

Theorem: rflagsbits->pf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->pf-of-rflagsbits

(defthm rflagsbits->pf-of-rflagsbits
  (equal (rflagsbits->pf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix pf)))

Theorem: rflagsbits->pf-of-write-with-mask

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

Function: rflagsbits->res2$inline

(defun rflagsbits->res2$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (mbe
    :logic
    (let ((x (rflagsbits-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-rflagsbits->res2

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

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

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

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

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

Theorem: rflagsbits->res2-of-rflagsbits

(defthm rflagsbits->res2-of-rflagsbits
  (equal (rflagsbits->res2
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix res2)))

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

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

Function: rflagsbits->af$inline

(defun rflagsbits->af$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (mbe
    :logic
    (let ((x (rflagsbits-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-rflagsbits->af

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

Theorem: rflagsbits->af$inline-of-rflagsbits-fix-x

(defthm rflagsbits->af$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->af$inline (rflagsbits-fix x))
         (rflagsbits->af$inline x)))

Theorem: rflagsbits->af$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->af-of-rflagsbits

(defthm rflagsbits->af-of-rflagsbits
  (equal (rflagsbits->af
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix af)))

Theorem: rflagsbits->af-of-write-with-mask

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

Function: rflagsbits->res3$inline

(defun rflagsbits->res3$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (mbe
    :logic
    (let ((x (rflagsbits-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-rflagsbits->res3

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

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

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

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

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

Theorem: rflagsbits->res3-of-rflagsbits

(defthm rflagsbits->res3-of-rflagsbits
  (equal (rflagsbits->res3
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix res3)))

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

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

Function: rflagsbits->zf$inline

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

Theorem: bitp-of-rflagsbits->zf

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

Theorem: rflagsbits->zf$inline-of-rflagsbits-fix-x

(defthm rflagsbits->zf$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->zf$inline (rflagsbits-fix x))
         (rflagsbits->zf$inline x)))

Theorem: rflagsbits->zf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->zf-of-rflagsbits

(defthm rflagsbits->zf-of-rflagsbits
  (equal (rflagsbits->zf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix zf)))

Theorem: rflagsbits->zf-of-write-with-mask

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

Function: rflagsbits->sf$inline

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

Theorem: bitp-of-rflagsbits->sf

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

Theorem: rflagsbits->sf$inline-of-rflagsbits-fix-x

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

Theorem: rflagsbits->sf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->sf-of-rflagsbits

(defthm rflagsbits->sf-of-rflagsbits
  (equal (rflagsbits->sf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix sf)))

Theorem: rflagsbits->sf-of-write-with-mask

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

Function: rflagsbits->tf$inline

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

Theorem: bitp-of-rflagsbits->tf

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

Theorem: rflagsbits->tf$inline-of-rflagsbits-fix-x

(defthm rflagsbits->tf$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->tf$inline (rflagsbits-fix x))
         (rflagsbits->tf$inline x)))

Theorem: rflagsbits->tf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->tf-of-rflagsbits

(defthm rflagsbits->tf-of-rflagsbits
  (equal (rflagsbits->tf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix tf)))

Theorem: rflagsbits->tf-of-write-with-mask

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

Function: rflagsbits->intf$inline

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

Theorem: bitp-of-rflagsbits->intf

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

Theorem: rflagsbits->intf$inline-of-rflagsbits-fix-x

(defthm rflagsbits->intf$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->intf$inline (rflagsbits-fix x))
         (rflagsbits->intf$inline x)))

Theorem: rflagsbits->intf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->intf-of-rflagsbits

(defthm rflagsbits->intf-of-rflagsbits
  (equal (rflagsbits->intf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix intf)))

Theorem: rflagsbits->intf-of-write-with-mask

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

Function: rflagsbits->df$inline

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

Theorem: bitp-of-rflagsbits->df

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

Theorem: rflagsbits->df$inline-of-rflagsbits-fix-x

(defthm rflagsbits->df$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->df$inline (rflagsbits-fix x))
         (rflagsbits->df$inline x)))

Theorem: rflagsbits->df$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->df-of-rflagsbits

(defthm rflagsbits->df-of-rflagsbits
  (equal (rflagsbits->df
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix df)))

Theorem: rflagsbits->df-of-write-with-mask

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

Function: rflagsbits->of$inline

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

Theorem: bitp-of-rflagsbits->of

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

Theorem: rflagsbits->of$inline-of-rflagsbits-fix-x

(defthm rflagsbits->of$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->of$inline (rflagsbits-fix x))
         (rflagsbits->of$inline x)))

Theorem: rflagsbits->of$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->of-of-rflagsbits

(defthm rflagsbits->of-of-rflagsbits
  (equal (rflagsbits->of
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix of)))

Theorem: rflagsbits->of-of-write-with-mask

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

Function: rflagsbits->iopl$inline

(defun rflagsbits->iopl$inline (x)
  (declare (xargs :guard (rflagsbits-p x)))
  (mbe :logic
       (let ((x (rflagsbits-fix x)))
         (part-select x :low 12 :width 2))
       :exec (the (unsigned-byte 2)
                  (logand (the (unsigned-byte 2) 3)
                          (the (unsigned-byte 20)
                               (ash (the (unsigned-byte 32) x)
                                    -12))))))

Theorem: 2bits-p-of-rflagsbits->iopl

(defthm 2bits-p-of-rflagsbits->iopl
  (b* ((iopl (rflagsbits->iopl$inline x)))
    (2bits-p iopl))
  :rule-classes :rewrite)

Theorem: rflagsbits->iopl$inline-of-rflagsbits-fix-x

(defthm rflagsbits->iopl$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->iopl$inline (rflagsbits-fix x))
         (rflagsbits->iopl$inline x)))

Theorem: rflagsbits->iopl$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->iopl-of-rflagsbits

(defthm rflagsbits->iopl-of-rflagsbits
  (equal (rflagsbits->iopl
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (2bits-fix iopl)))

Theorem: rflagsbits->iopl-of-write-with-mask

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

Function: rflagsbits->nt$inline

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

Theorem: bitp-of-rflagsbits->nt

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

Theorem: rflagsbits->nt$inline-of-rflagsbits-fix-x

(defthm rflagsbits->nt$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->nt$inline (rflagsbits-fix x))
         (rflagsbits->nt$inline x)))

Theorem: rflagsbits->nt$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->nt-of-rflagsbits

(defthm rflagsbits->nt-of-rflagsbits
  (equal (rflagsbits->nt
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix nt)))

Theorem: rflagsbits->nt-of-write-with-mask

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

Function: rflagsbits->res4$inline

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

Theorem: bitp-of-rflagsbits->res4

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

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

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

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

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

Theorem: rflagsbits->res4-of-rflagsbits

(defthm rflagsbits->res4-of-rflagsbits
  (equal (rflagsbits->res4
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix res4)))

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

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

Function: rflagsbits->rf$inline

(defun rflagsbits->rf$inline (x)
  (declare (xargs :guard (rflagsbits-p x)))
  (mbe :logic
       (let ((x (rflagsbits-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-rflagsbits->rf

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

Theorem: rflagsbits->rf$inline-of-rflagsbits-fix-x

(defthm rflagsbits->rf$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->rf$inline (rflagsbits-fix x))
         (rflagsbits->rf$inline x)))

Theorem: rflagsbits->rf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->rf-of-rflagsbits

(defthm rflagsbits->rf-of-rflagsbits
  (equal (rflagsbits->rf
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix rf)))

Theorem: rflagsbits->rf-of-write-with-mask

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

Function: rflagsbits->vm$inline

(defun rflagsbits->vm$inline (x)
  (declare (xargs :guard (rflagsbits-p x)))
  (mbe :logic
       (let ((x (rflagsbits-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-rflagsbits->vm

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

Theorem: rflagsbits->vm$inline-of-rflagsbits-fix-x

(defthm rflagsbits->vm$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->vm$inline (rflagsbits-fix x))
         (rflagsbits->vm$inline x)))

Theorem: rflagsbits->vm$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->vm-of-rflagsbits

(defthm rflagsbits->vm-of-rflagsbits
  (equal (rflagsbits->vm
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix vm)))

Theorem: rflagsbits->vm-of-write-with-mask

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

Function: rflagsbits->ac$inline

(defun rflagsbits->ac$inline (x)
  (declare (xargs :guard (rflagsbits-p x)))
  (mbe :logic
       (let ((x (rflagsbits-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-rflagsbits->ac

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

Theorem: rflagsbits->ac$inline-of-rflagsbits-fix-x

(defthm rflagsbits->ac$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->ac$inline (rflagsbits-fix x))
         (rflagsbits->ac$inline x)))

Theorem: rflagsbits->ac$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->ac-of-rflagsbits

(defthm rflagsbits->ac-of-rflagsbits
  (equal (rflagsbits->ac
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix ac)))

Theorem: rflagsbits->ac-of-write-with-mask

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

Function: rflagsbits->vif$inline

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

Theorem: bitp-of-rflagsbits->vif

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

Theorem: rflagsbits->vif$inline-of-rflagsbits-fix-x

(defthm rflagsbits->vif$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->vif$inline (rflagsbits-fix x))
         (rflagsbits->vif$inline x)))

Theorem: rflagsbits->vif$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->vif-of-rflagsbits

(defthm rflagsbits->vif-of-rflagsbits
  (equal (rflagsbits->vif
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix vif)))

Theorem: rflagsbits->vif-of-write-with-mask

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

Function: rflagsbits->vip$inline

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

Theorem: bitp-of-rflagsbits->vip

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

Theorem: rflagsbits->vip$inline-of-rflagsbits-fix-x

(defthm rflagsbits->vip$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->vip$inline (rflagsbits-fix x))
         (rflagsbits->vip$inline x)))

Theorem: rflagsbits->vip$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->vip-of-rflagsbits

(defthm rflagsbits->vip-of-rflagsbits
  (equal (rflagsbits->vip
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix vip)))

Theorem: rflagsbits->vip-of-write-with-mask

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

Function: rflagsbits->id$inline

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

Theorem: bitp-of-rflagsbits->id

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

Theorem: rflagsbits->id$inline-of-rflagsbits-fix-x

(defthm rflagsbits->id$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->id$inline (rflagsbits-fix x))
         (rflagsbits->id$inline x)))

Theorem: rflagsbits->id$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->id-of-rflagsbits

(defthm rflagsbits->id-of-rflagsbits
  (equal (rflagsbits->id
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (bfix id)))

Theorem: rflagsbits->id-of-write-with-mask

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

Function: rflagsbits->res5$inline

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

Theorem: 10bits-p-of-rflagsbits->res5

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

Theorem: rflagsbits->res5$inline-of-rflagsbits-fix-x

(defthm rflagsbits->res5$inline-of-rflagsbits-fix-x
  (equal (rflagsbits->res5$inline (rflagsbits-fix x))
         (rflagsbits->res5$inline x)))

Theorem: rflagsbits->res5$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: rflagsbits->res5-of-rflagsbits

(defthm rflagsbits->res5-of-rflagsbits
  (equal (rflagsbits->res5
              (rflagsbits cf
                          res1 pf res2 af res3 zf sf tf intf df of
                          iopl nt res4 rf vm ac vif vip id res5))
         (10bits-fix res5)))

Theorem: rflagsbits->res5-of-write-with-mask

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

Theorem: rflagsbits-fix-in-terms-of-rflagsbits

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

Function: !rflagsbits->cf$inline

(defun !rflagsbits->cf$inline (cf x)
  (declare (xargs :guard (and (bitp cf) (rflagsbits-p x))))
  (mbe :logic
       (b* ((cf (mbe :logic (bfix cf) :exec cf))
            (x (rflagsbits-fix x)))
         (part-install cf 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) cf)))))

Theorem: rflagsbits-p-of-!rflagsbits->cf

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

Theorem: !rflagsbits->cf$inline-of-bfix-cf

(defthm !rflagsbits->cf$inline-of-bfix-cf
  (equal (!rflagsbits->cf$inline (bfix cf) x)
         (!rflagsbits->cf$inline cf x)))

Theorem: !rflagsbits->cf$inline-bit-equiv-congruence-on-cf

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

Theorem: !rflagsbits->cf$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->cf$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->cf$inline cf (rflagsbits-fix x))
         (!rflagsbits->cf$inline cf x)))

Theorem: !rflagsbits->cf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->cf-is-rflagsbits

(defthm !rflagsbits->cf-is-rflagsbits
  (equal (!rflagsbits->cf cf x)
         (change-rflagsbits x :cf cf)))

Theorem: rflagsbits->cf-of-!rflagsbits->cf

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

Theorem: !rflagsbits->cf-equiv-under-mask

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

Function: !rflagsbits->res1$inline

(defun !rflagsbits->res1$inline (res1 x)
  (declare (xargs :guard (and (bitp res1) (rflagsbits-p x))))
  (mbe :logic
       (b* ((res1 (mbe :logic (bfix res1) :exec res1))
            (x (rflagsbits-fix x)))
         (part-install res1 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) res1)
                                    1))))))

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

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

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

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

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

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

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

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

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

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

Theorem: !rflagsbits->res1-is-rflagsbits

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

Theorem: rflagsbits->res1-of-!rflagsbits->res1

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

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

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

Function: !rflagsbits->pf$inline

(defun !rflagsbits->pf$inline (pf x)
 (declare (xargs :guard (and (bitp pf) (rflagsbits-p x))))
 (mbe
     :logic
     (b* ((pf (mbe :logic (bfix pf) :exec pf))
          (x (rflagsbits-fix x)))
       (part-install pf 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) pf) 2))))))

Theorem: rflagsbits-p-of-!rflagsbits->pf

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

Theorem: !rflagsbits->pf$inline-of-bfix-pf

(defthm !rflagsbits->pf$inline-of-bfix-pf
  (equal (!rflagsbits->pf$inline (bfix pf) x)
         (!rflagsbits->pf$inline pf x)))

Theorem: !rflagsbits->pf$inline-bit-equiv-congruence-on-pf

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

Theorem: !rflagsbits->pf$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->pf$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->pf$inline pf (rflagsbits-fix x))
         (!rflagsbits->pf$inline pf x)))

Theorem: !rflagsbits->pf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->pf-is-rflagsbits

(defthm !rflagsbits->pf-is-rflagsbits
  (equal (!rflagsbits->pf pf x)
         (change-rflagsbits x :pf pf)))

Theorem: rflagsbits->pf-of-!rflagsbits->pf

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

Theorem: !rflagsbits->pf-equiv-under-mask

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

Function: !rflagsbits->res2$inline

(defun !rflagsbits->res2$inline (res2 x)
  (declare (xargs :guard (and (bitp res2) (rflagsbits-p x))))
  (mbe :logic
       (b* ((res2 (mbe :logic (bfix res2) :exec res2))
            (x (rflagsbits-fix x)))
         (part-install res2 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) res2)
                                    3))))))

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

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

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

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

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

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

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

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

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

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

Theorem: !rflagsbits->res2-is-rflagsbits

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

Theorem: rflagsbits->res2-of-!rflagsbits->res2

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

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

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

Function: !rflagsbits->af$inline

(defun !rflagsbits->af$inline (af x)
 (declare (xargs :guard (and (bitp af) (rflagsbits-p x))))
 (mbe
     :logic
     (b* ((af (mbe :logic (bfix af) :exec af))
          (x (rflagsbits-fix x)))
       (part-install af 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) af) 4))))))

Theorem: rflagsbits-p-of-!rflagsbits->af

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

Theorem: !rflagsbits->af$inline-of-bfix-af

(defthm !rflagsbits->af$inline-of-bfix-af
  (equal (!rflagsbits->af$inline (bfix af) x)
         (!rflagsbits->af$inline af x)))

Theorem: !rflagsbits->af$inline-bit-equiv-congruence-on-af

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

Theorem: !rflagsbits->af$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->af$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->af$inline af (rflagsbits-fix x))
         (!rflagsbits->af$inline af x)))

Theorem: !rflagsbits->af$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->af-is-rflagsbits

(defthm !rflagsbits->af-is-rflagsbits
  (equal (!rflagsbits->af af x)
         (change-rflagsbits x :af af)))

Theorem: rflagsbits->af-of-!rflagsbits->af

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

Theorem: !rflagsbits->af-equiv-under-mask

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

Function: !rflagsbits->res3$inline

(defun !rflagsbits->res3$inline (res3 x)
  (declare (xargs :guard (and (bitp res3) (rflagsbits-p x))))
  (mbe :logic
       (b* ((res3 (mbe :logic (bfix res3) :exec res3))
            (x (rflagsbits-fix x)))
         (part-install res3 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) res3)
                                    5))))))

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

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

Theorem: !rflagsbits->res3$inline-of-bfix-res3

(defthm !rflagsbits->res3$inline-of-bfix-res3
  (equal (!rflagsbits->res3$inline (bfix res3) x)
         (!rflagsbits->res3$inline res3 x)))

Theorem: !rflagsbits->res3$inline-bit-equiv-congruence-on-res3

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

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

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

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

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

Theorem: !rflagsbits->res3-is-rflagsbits

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

Theorem: rflagsbits->res3-of-!rflagsbits->res3

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

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

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

Function: !rflagsbits->zf$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->zf

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

Theorem: !rflagsbits->zf$inline-of-bfix-zf

(defthm !rflagsbits->zf$inline-of-bfix-zf
  (equal (!rflagsbits->zf$inline (bfix zf) x)
         (!rflagsbits->zf$inline zf x)))

Theorem: !rflagsbits->zf$inline-bit-equiv-congruence-on-zf

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

Theorem: !rflagsbits->zf$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->zf$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->zf$inline zf (rflagsbits-fix x))
         (!rflagsbits->zf$inline zf x)))

Theorem: !rflagsbits->zf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->zf-is-rflagsbits

(defthm !rflagsbits->zf-is-rflagsbits
  (equal (!rflagsbits->zf zf x)
         (change-rflagsbits x :zf zf)))

Theorem: rflagsbits->zf-of-!rflagsbits->zf

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

Theorem: !rflagsbits->zf-equiv-under-mask

(defthm !rflagsbits->zf-equiv-under-mask
  (b* ((?new-x (!rflagsbits->zf$inline zf x)))
    (rflagsbits-equiv-under-mask new-x x -65)))

Function: !rflagsbits->sf$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->sf

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

Theorem: !rflagsbits->sf$inline-of-bfix-sf

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

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

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

Theorem: !rflagsbits->sf$inline-of-rflagsbits-fix-x

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

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

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

Theorem: !rflagsbits->sf-is-rflagsbits

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

Theorem: rflagsbits->sf-of-!rflagsbits->sf

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

Theorem: !rflagsbits->sf-equiv-under-mask

(defthm !rflagsbits->sf-equiv-under-mask
  (b* ((?new-x (!rflagsbits->sf$inline sf x)))
    (rflagsbits-equiv-under-mask new-x x -129)))

Function: !rflagsbits->tf$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->tf

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

Theorem: !rflagsbits->tf$inline-of-bfix-tf

(defthm !rflagsbits->tf$inline-of-bfix-tf
  (equal (!rflagsbits->tf$inline (bfix tf) x)
         (!rflagsbits->tf$inline tf x)))

Theorem: !rflagsbits->tf$inline-bit-equiv-congruence-on-tf

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

Theorem: !rflagsbits->tf$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->tf$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->tf$inline tf (rflagsbits-fix x))
         (!rflagsbits->tf$inline tf x)))

Theorem: !rflagsbits->tf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->tf-is-rflagsbits

(defthm !rflagsbits->tf-is-rflagsbits
  (equal (!rflagsbits->tf tf x)
         (change-rflagsbits x :tf tf)))

Theorem: rflagsbits->tf-of-!rflagsbits->tf

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

Theorem: !rflagsbits->tf-equiv-under-mask

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

Function: !rflagsbits->intf$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->intf

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

Theorem: !rflagsbits->intf$inline-of-bfix-intf

(defthm !rflagsbits->intf$inline-of-bfix-intf
  (equal (!rflagsbits->intf$inline (bfix intf) x)
         (!rflagsbits->intf$inline intf x)))

Theorem: !rflagsbits->intf$inline-bit-equiv-congruence-on-intf

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

Theorem: !rflagsbits->intf$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->intf$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->intf$inline intf (rflagsbits-fix x))
         (!rflagsbits->intf$inline intf x)))

Theorem: !rflagsbits->intf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->intf-is-rflagsbits

(defthm !rflagsbits->intf-is-rflagsbits
  (equal (!rflagsbits->intf intf x)
         (change-rflagsbits x :intf intf)))

Theorem: rflagsbits->intf-of-!rflagsbits->intf

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

Theorem: !rflagsbits->intf-equiv-under-mask

(defthm !rflagsbits->intf-equiv-under-mask
  (b* ((?new-x (!rflagsbits->intf$inline intf x)))
    (rflagsbits-equiv-under-mask new-x x -513)))

Function: !rflagsbits->df$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->df

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

Theorem: !rflagsbits->df$inline-of-bfix-df

(defthm !rflagsbits->df$inline-of-bfix-df
  (equal (!rflagsbits->df$inline (bfix df) x)
         (!rflagsbits->df$inline df x)))

Theorem: !rflagsbits->df$inline-bit-equiv-congruence-on-df

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

Theorem: !rflagsbits->df$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->df$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->df$inline df (rflagsbits-fix x))
         (!rflagsbits->df$inline df x)))

Theorem: !rflagsbits->df$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->df-is-rflagsbits

(defthm !rflagsbits->df-is-rflagsbits
  (equal (!rflagsbits->df df x)
         (change-rflagsbits x :df df)))

Theorem: rflagsbits->df-of-!rflagsbits->df

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

Theorem: !rflagsbits->df-equiv-under-mask

(defthm !rflagsbits->df-equiv-under-mask
  (b* ((?new-x (!rflagsbits->df$inline df x)))
    (rflagsbits-equiv-under-mask new-x x -1025)))

Function: !rflagsbits->of$inline

(defun !rflagsbits->of$inline (of x)
 (declare (xargs :guard (and (bitp of) (rflagsbits-p x))))
 (mbe
    :logic
    (b* ((of (mbe :logic (bfix of) :exec of))
         (x (rflagsbits-fix x)))
      (part-install of x :width 1 :low 11))
    :exec (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32)
                            (logand (the (unsigned-byte 32) x)
                                    (the (signed-byte 13) -2049)))
                       (the (unsigned-byte 12)
                            (ash (the (unsigned-byte 1) of) 11))))))

Theorem: rflagsbits-p-of-!rflagsbits->of

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

Theorem: !rflagsbits->of$inline-of-bfix-of

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

Theorem: !rflagsbits->of$inline-bit-equiv-congruence-on-of

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

Theorem: !rflagsbits->of$inline-of-rflagsbits-fix-x

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

Theorem: !rflagsbits->of$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->of-is-rflagsbits

(defthm !rflagsbits->of-is-rflagsbits
  (equal (!rflagsbits->of of x)
         (change-rflagsbits x :of of)))

Theorem: rflagsbits->of-of-!rflagsbits->of

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

Theorem: !rflagsbits->of-equiv-under-mask

(defthm !rflagsbits->of-equiv-under-mask
  (b* ((?new-x (!rflagsbits->of$inline of x)))
    (rflagsbits-equiv-under-mask new-x x -2049)))

Function: !rflagsbits->iopl$inline

(defun !rflagsbits->iopl$inline (iopl x)
 (declare (xargs :guard (and (2bits-p iopl) (rflagsbits-p x))))
 (mbe
     :logic
     (b* ((iopl (mbe :logic (2bits-fix iopl)
                     :exec iopl))
          (x (rflagsbits-fix x)))
       (part-install iopl x :width 2 :low 12))
     :exec (the (unsigned-byte 32)
                (logior (the (unsigned-byte 32)
                             (logand (the (unsigned-byte 32) x)
                                     (the (signed-byte 15) -12289)))
                        (the (unsigned-byte 14)
                             (ash (the (unsigned-byte 2) iopl)
                                  12))))))

Theorem: rflagsbits-p-of-!rflagsbits->iopl

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

Theorem: !rflagsbits->iopl$inline-of-2bits-fix-iopl

(defthm !rflagsbits->iopl$inline-of-2bits-fix-iopl
  (equal (!rflagsbits->iopl$inline (2bits-fix iopl)
                                   x)
         (!rflagsbits->iopl$inline iopl x)))

Theorem: !rflagsbits->iopl$inline-2bits-equiv-congruence-on-iopl

(defthm !rflagsbits->iopl$inline-2bits-equiv-congruence-on-iopl
  (implies (2bits-equiv iopl iopl-equiv)
           (equal (!rflagsbits->iopl$inline iopl x)
                  (!rflagsbits->iopl$inline iopl-equiv x)))
  :rule-classes :congruence)

Theorem: !rflagsbits->iopl$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->iopl$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->iopl$inline iopl (rflagsbits-fix x))
         (!rflagsbits->iopl$inline iopl x)))

Theorem: !rflagsbits->iopl$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->iopl-is-rflagsbits

(defthm !rflagsbits->iopl-is-rflagsbits
  (equal (!rflagsbits->iopl iopl x)
         (change-rflagsbits x :iopl iopl)))

Theorem: rflagsbits->iopl-of-!rflagsbits->iopl

(defthm rflagsbits->iopl-of-!rflagsbits->iopl
  (b* ((?new-x (!rflagsbits->iopl$inline iopl x)))
    (equal (rflagsbits->iopl new-x)
           (2bits-fix iopl))))

Theorem: !rflagsbits->iopl-equiv-under-mask

(defthm !rflagsbits->iopl-equiv-under-mask
  (b* ((?new-x (!rflagsbits->iopl$inline iopl x)))
    (rflagsbits-equiv-under-mask new-x x -12289)))

Function: !rflagsbits->nt$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->nt

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

Theorem: !rflagsbits->nt$inline-of-bfix-nt

(defthm !rflagsbits->nt$inline-of-bfix-nt
  (equal (!rflagsbits->nt$inline (bfix nt) x)
         (!rflagsbits->nt$inline nt x)))

Theorem: !rflagsbits->nt$inline-bit-equiv-congruence-on-nt

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

Theorem: !rflagsbits->nt$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->nt$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->nt$inline nt (rflagsbits-fix x))
         (!rflagsbits->nt$inline nt x)))

Theorem: !rflagsbits->nt$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->nt-is-rflagsbits

(defthm !rflagsbits->nt-is-rflagsbits
  (equal (!rflagsbits->nt nt x)
         (change-rflagsbits x :nt nt)))

Theorem: rflagsbits->nt-of-!rflagsbits->nt

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

Theorem: !rflagsbits->nt-equiv-under-mask

(defthm !rflagsbits->nt-equiv-under-mask
  (b* ((?new-x (!rflagsbits->nt$inline nt x)))
    (rflagsbits-equiv-under-mask new-x x -16385)))

Function: !rflagsbits->res4$inline

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

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

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

Theorem: !rflagsbits->res4$inline-of-bfix-res4

(defthm !rflagsbits->res4$inline-of-bfix-res4
  (equal (!rflagsbits->res4$inline (bfix res4) x)
         (!rflagsbits->res4$inline res4 x)))

Theorem: !rflagsbits->res4$inline-bit-equiv-congruence-on-res4

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

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

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

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

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

Theorem: !rflagsbits->res4-is-rflagsbits

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

Theorem: rflagsbits->res4-of-!rflagsbits->res4

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

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

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

Function: !rflagsbits->rf$inline

(defun !rflagsbits->rf$inline (rf x)
 (declare (xargs :guard (and (bitp rf) (rflagsbits-p x))))
 (mbe
    :logic
    (b* ((rf (mbe :logic (bfix rf) :exec rf))
         (x (rflagsbits-fix x)))
      (part-install rf 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) rf) 16))))))

Theorem: rflagsbits-p-of-!rflagsbits->rf

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

Theorem: !rflagsbits->rf$inline-of-bfix-rf

(defthm !rflagsbits->rf$inline-of-bfix-rf
  (equal (!rflagsbits->rf$inline (bfix rf) x)
         (!rflagsbits->rf$inline rf x)))

Theorem: !rflagsbits->rf$inline-bit-equiv-congruence-on-rf

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

Theorem: !rflagsbits->rf$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->rf$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->rf$inline rf (rflagsbits-fix x))
         (!rflagsbits->rf$inline rf x)))

Theorem: !rflagsbits->rf$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->rf-is-rflagsbits

(defthm !rflagsbits->rf-is-rflagsbits
  (equal (!rflagsbits->rf rf x)
         (change-rflagsbits x :rf rf)))

Theorem: rflagsbits->rf-of-!rflagsbits->rf

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

Theorem: !rflagsbits->rf-equiv-under-mask

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

Function: !rflagsbits->vm$inline

(defun !rflagsbits->vm$inline (vm x)
 (declare (xargs :guard (and (bitp vm) (rflagsbits-p x))))
 (mbe
    :logic
    (b* ((vm (mbe :logic (bfix vm) :exec vm))
         (x (rflagsbits-fix x)))
      (part-install vm 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) vm) 17))))))

Theorem: rflagsbits-p-of-!rflagsbits->vm

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

Theorem: !rflagsbits->vm$inline-of-bfix-vm

(defthm !rflagsbits->vm$inline-of-bfix-vm
  (equal (!rflagsbits->vm$inline (bfix vm) x)
         (!rflagsbits->vm$inline vm x)))

Theorem: !rflagsbits->vm$inline-bit-equiv-congruence-on-vm

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

Theorem: !rflagsbits->vm$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->vm$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->vm$inline vm (rflagsbits-fix x))
         (!rflagsbits->vm$inline vm x)))

Theorem: !rflagsbits->vm$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->vm-is-rflagsbits

(defthm !rflagsbits->vm-is-rflagsbits
  (equal (!rflagsbits->vm vm x)
         (change-rflagsbits x :vm vm)))

Theorem: rflagsbits->vm-of-!rflagsbits->vm

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

Theorem: !rflagsbits->vm-equiv-under-mask

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

Function: !rflagsbits->ac$inline

(defun !rflagsbits->ac$inline (ac x)
 (declare (xargs :guard (and (bitp ac) (rflagsbits-p x))))
 (mbe
    :logic
    (b* ((ac (mbe :logic (bfix ac) :exec ac))
         (x (rflagsbits-fix x)))
      (part-install ac 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) ac) 18))))))

Theorem: rflagsbits-p-of-!rflagsbits->ac

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

Theorem: !rflagsbits->ac$inline-of-bfix-ac

(defthm !rflagsbits->ac$inline-of-bfix-ac
  (equal (!rflagsbits->ac$inline (bfix ac) x)
         (!rflagsbits->ac$inline ac x)))

Theorem: !rflagsbits->ac$inline-bit-equiv-congruence-on-ac

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

Theorem: !rflagsbits->ac$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->ac$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->ac$inline ac (rflagsbits-fix x))
         (!rflagsbits->ac$inline ac x)))

Theorem: !rflagsbits->ac$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->ac-is-rflagsbits

(defthm !rflagsbits->ac-is-rflagsbits
  (equal (!rflagsbits->ac ac x)
         (change-rflagsbits x :ac ac)))

Theorem: rflagsbits->ac-of-!rflagsbits->ac

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

Theorem: !rflagsbits->ac-equiv-under-mask

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

Function: !rflagsbits->vif$inline

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

Theorem: rflagsbits-p-of-!rflagsbits->vif

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

Theorem: !rflagsbits->vif$inline-of-bfix-vif

(defthm !rflagsbits->vif$inline-of-bfix-vif
  (equal (!rflagsbits->vif$inline (bfix vif) x)
         (!rflagsbits->vif$inline vif x)))

Theorem: !rflagsbits->vif$inline-bit-equiv-congruence-on-vif

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

Theorem: !rflagsbits->vif$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->vif$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->vif$inline vif (rflagsbits-fix x))
         (!rflagsbits->vif$inline vif x)))

Theorem: !rflagsbits->vif$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->vif-is-rflagsbits

(defthm !rflagsbits->vif-is-rflagsbits
  (equal (!rflagsbits->vif vif x)
         (change-rflagsbits x :vif vif)))

Theorem: rflagsbits->vif-of-!rflagsbits->vif

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

Theorem: !rflagsbits->vif-equiv-under-mask

(defthm !rflagsbits->vif-equiv-under-mask
  (b* ((?new-x (!rflagsbits->vif$inline vif x)))
    (rflagsbits-equiv-under-mask new-x x -524289)))

Function: !rflagsbits->vip$inline

(defun !rflagsbits->vip$inline (vip x)
 (declare (xargs :guard (and (bitp vip) (rflagsbits-p x))))
 (mbe
   :logic
   (b* ((vip (mbe :logic (bfix vip) :exec vip))
        (x (rflagsbits-fix x)))
     (part-install vip x :width 1 :low 20))
   :exec (the (unsigned-byte 32)
              (logior (the (unsigned-byte 32)
                           (logand (the (unsigned-byte 32) x)
                                   (the (signed-byte 22) -1048577)))
                      (the (unsigned-byte 21)
                           (ash (the (unsigned-byte 1) vip)
                                20))))))

Theorem: rflagsbits-p-of-!rflagsbits->vip

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

Theorem: !rflagsbits->vip$inline-of-bfix-vip

(defthm !rflagsbits->vip$inline-of-bfix-vip
  (equal (!rflagsbits->vip$inline (bfix vip) x)
         (!rflagsbits->vip$inline vip x)))

Theorem: !rflagsbits->vip$inline-bit-equiv-congruence-on-vip

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

Theorem: !rflagsbits->vip$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->vip$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->vip$inline vip (rflagsbits-fix x))
         (!rflagsbits->vip$inline vip x)))

Theorem: !rflagsbits->vip$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->vip-is-rflagsbits

(defthm !rflagsbits->vip-is-rflagsbits
  (equal (!rflagsbits->vip vip x)
         (change-rflagsbits x :vip vip)))

Theorem: rflagsbits->vip-of-!rflagsbits->vip

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

Theorem: !rflagsbits->vip-equiv-under-mask

(defthm !rflagsbits->vip-equiv-under-mask
  (b* ((?new-x (!rflagsbits->vip$inline vip x)))
    (rflagsbits-equiv-under-mask new-x x -1048577)))

Function: !rflagsbits->id$inline

(defun !rflagsbits->id$inline (id x)
 (declare (xargs :guard (and (bitp id) (rflagsbits-p x))))
 (mbe
   :logic
   (b* ((id (mbe :logic (bfix id) :exec id))
        (x (rflagsbits-fix x)))
     (part-install id x :width 1 :low 21))
   :exec (the (unsigned-byte 32)
              (logior (the (unsigned-byte 32)
                           (logand (the (unsigned-byte 32) x)
                                   (the (signed-byte 23) -2097153)))
                      (the (unsigned-byte 22)
                           (ash (the (unsigned-byte 1) id) 21))))))

Theorem: rflagsbits-p-of-!rflagsbits->id

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

Theorem: !rflagsbits->id$inline-of-bfix-id

(defthm !rflagsbits->id$inline-of-bfix-id
  (equal (!rflagsbits->id$inline (bfix id) x)
         (!rflagsbits->id$inline id x)))

Theorem: !rflagsbits->id$inline-bit-equiv-congruence-on-id

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

Theorem: !rflagsbits->id$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->id$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->id$inline id (rflagsbits-fix x))
         (!rflagsbits->id$inline id x)))

Theorem: !rflagsbits->id$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->id-is-rflagsbits

(defthm !rflagsbits->id-is-rflagsbits
  (equal (!rflagsbits->id id x)
         (change-rflagsbits x :id id)))

Theorem: rflagsbits->id-of-!rflagsbits->id

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

Theorem: !rflagsbits->id-equiv-under-mask

(defthm !rflagsbits->id-equiv-under-mask
  (b* ((?new-x (!rflagsbits->id$inline id x)))
    (rflagsbits-equiv-under-mask new-x x -2097153)))

Function: !rflagsbits->res5$inline

(defun !rflagsbits->res5$inline (res5 x)
 (declare (xargs :guard (and (10bits-p res5) (rflagsbits-p x))))
 (mbe :logic
      (b* ((res5 (mbe :logic (10bits-fix res5)
                      :exec res5))
           (x (rflagsbits-fix x)))
        (part-install res5 x :width 10 :low 22))
      :exec
      (the (unsigned-byte 32)
           (logior (the (unsigned-byte 32)
                        (logand (the (unsigned-byte 32) x)
                                (the (signed-byte 33) -4290772993)))
                   (the (unsigned-byte 32)
                        (ash (the (unsigned-byte 10) res5)
                             22))))))

Theorem: rflagsbits-p-of-!rflagsbits->res5

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

Theorem: !rflagsbits->res5$inline-of-10bits-fix-res5

(defthm !rflagsbits->res5$inline-of-10bits-fix-res5
  (equal (!rflagsbits->res5$inline (10bits-fix res5)
                                   x)
         (!rflagsbits->res5$inline res5 x)))

Theorem: !rflagsbits->res5$inline-10bits-equiv-congruence-on-res5

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

Theorem: !rflagsbits->res5$inline-of-rflagsbits-fix-x

(defthm !rflagsbits->res5$inline-of-rflagsbits-fix-x
  (equal (!rflagsbits->res5$inline res5 (rflagsbits-fix x))
         (!rflagsbits->res5$inline res5 x)))

Theorem: !rflagsbits->res5$inline-rflagsbits-equiv-congruence-on-x

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

Theorem: !rflagsbits->res5-is-rflagsbits

(defthm !rflagsbits->res5-is-rflagsbits
  (equal (!rflagsbits->res5 res5 x)
         (change-rflagsbits x :res5 res5)))

Theorem: rflagsbits->res5-of-!rflagsbits->res5

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

Theorem: !rflagsbits->res5-equiv-under-mask

(defthm !rflagsbits->res5-equiv-under-mask
  (b* ((?new-x (!rflagsbits->res5$inline res5 x)))
    (rflagsbits-equiv-under-mask new-x x 4194303)))

Function: rflagsbits-debug$inline

(defun rflagsbits-debug$inline (x)
 (declare (xargs :guard (rflagsbits-p x)))
 (b* (((rflagsbits x)))
  (cons
   (cons 'cf x.cf)
   (cons
    (cons 'res1 x.res1)
    (cons
     (cons 'pf x.pf)
     (cons
      (cons 'res2 x.res2)
      (cons
       (cons 'af x.af)
       (cons
        (cons 'res3 x.res3)
        (cons
         (cons 'zf x.zf)
         (cons
          (cons 'sf x.sf)
          (cons
           (cons 'tf x.tf)
           (cons
            (cons 'intf x.intf)
            (cons
             (cons 'df x.df)
             (cons
              (cons 'of x.of)
              (cons
               (cons 'iopl x.iopl)
               (cons
                (cons 'nt x.nt)
                (cons
                 (cons 'res4 x.res4)
                 (cons
                  (cons 'rf x.rf)
                  (cons
                   (cons 'vm x.vm)
                   (cons
                    (cons 'ac x.ac)
                    (cons
                       (cons 'vif x.vif)
                       (cons (cons 'vip x.vip)
                             (cons (cons 'id x.id)
                                   (cons (cons 'res5 x.res5)
                                         nil))))))))))))))))))))))))

Subtopics

Rflagsbits-p: Recognizer for rflagsbits bit structures.
!rflagsbits->res5: Update the |X86ISA|::|RES5| field of a rflagsbits bit structure.
!rflagsbits->res4: Update the |X86ISA|::|RES4| field of a rflagsbits bit structure.
!rflagsbits->res3: Update the |X86ISA|::|RES3| field of a rflagsbits bit structure.
!rflagsbits->res2: Update the |X86ISA|::|RES2| field of a rflagsbits bit structure.
!rflagsbits->res1: Update the |X86ISA|::|RES1| field of a rflagsbits bit structure.
!rflagsbits->iopl: Update the |X86ISA|::|IOPL| field of a rflagsbits bit structure.
!rflagsbits->intf: Update the |X86ISA|::|INTF| field of a rflagsbits bit structure.
!rflagsbits->vip: Update the |X86ISA|::|VIP| field of a rflagsbits bit structure.
!rflagsbits->vif: Update the |X86ISA|::|VIF| field of a rflagsbits bit structure.
!rflagsbits->zf: Update the |X86ISA|::|ZF| field of a rflagsbits bit structure.
!rflagsbits->vm: Update the |X86ISA|::|VM| field of a rflagsbits bit structure.
!rflagsbits->tf: Update the |X86ISA|::|TF| field of a rflagsbits bit structure.
!rflagsbits->sf: Update the |X86ISA|::|SF| field of a rflagsbits bit structure.
!rflagsbits->rf: Update the |X86ISA|::|RF| field of a rflagsbits bit structure.
!rflagsbits->pf: Update the |ACL2|::|PF| field of a rflagsbits bit structure.
!rflagsbits->of: Update the |X86ISA|::|OF| field of a rflagsbits bit structure.
!rflagsbits->nt: Update the |X86ISA|::|NT| field of a rflagsbits bit structure.
!rflagsbits->id: Update the |ACL2|::|ID| field of a rflagsbits bit structure.
!rflagsbits->df: Update the |X86ISA|::|DF| field of a rflagsbits bit structure.
!rflagsbits->cf: Update the |X86ISA|::|CF| field of a rflagsbits bit structure.
!rflagsbits->af: Update the |X86ISA|::|AF| field of a rflagsbits bit structure.
!rflagsbits->ac: Update the |X86ISA|::|AC| field of a rflagsbits bit structure.
Rflagsbits->res5: Access the |X86ISA|::|RES5| field of a rflagsbits bit structure.
Rflagsbits->res4: Access the |X86ISA|::|RES4| field of a rflagsbits bit structure.
Rflagsbits->iopl: Access the |X86ISA|::|IOPL| field of a rflagsbits bit structure.
Rflagsbits->zf: Access the |X86ISA|::|ZF| field of a rflagsbits bit structure.
Rflagsbits->vm: Access the |X86ISA|::|VM| field of a rflagsbits bit structure.
Rflagsbits->vip: Access the |X86ISA|::|VIP| field of a rflagsbits bit structure.
Rflagsbits->vif: Access the |X86ISA|::|VIF| field of a rflagsbits bit structure.
Rflagsbits->tf: Access the |X86ISA|::|TF| field of a rflagsbits bit structure.
Rflagsbits->sf: Access the |X86ISA|::|SF| field of a rflagsbits bit structure.
Rflagsbits->rf: Access the |X86ISA|::|RF| field of a rflagsbits bit structure.
Rflagsbits->res3: Access the |X86ISA|::|RES3| field of a rflagsbits bit structure.
Rflagsbits->res2: Access the |X86ISA|::|RES2| field of a rflagsbits bit structure.
Rflagsbits->res1: Access the |X86ISA|::|RES1| field of a rflagsbits bit structure.
Rflagsbits->pf: Access the |ACL2|::|PF| field of a rflagsbits bit structure.
Rflagsbits->of: Access the |X86ISA|::|OF| field of a rflagsbits bit structure.
Rflagsbits->nt: Access the |X86ISA|::|NT| field of a rflagsbits bit structure.
Rflagsbits->intf: Access the |X86ISA|::|INTF| field of a rflagsbits bit structure.
Rflagsbits->id: Access the |ACL2|::|ID| field of a rflagsbits bit structure.
Rflagsbits->df: Access the |X86ISA|::|DF| field of a rflagsbits bit structure.
Rflagsbits->af: Access the |X86ISA|::|AF| field of a rflagsbits bit structure.
Rflagsbits->ac: Access the |X86ISA|::|AC| field of a rflagsbits bit structure.
Rflagsbits-fix: Fixing function for rflagsbits bit structures.
Rflagsbits->cf: Access the |X86ISA|::|CF| field of a rflagsbits bit structure.