		Search-engine friendly clone of the ACL2 documentation.

Paging-bitstructs

Ia32e-pml4ebits

An 64-bit unsigned bitstruct type.

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

Fields

p — bit
r/w — bit
u/s — bit
pwt — bit
pcd — bit
a — bit
res1 — bit
ps — bit
res2 — 4bits
pdpt — 40bits
res3 — 11bits
xd — bit

Definitions and Theorems

Function: ia32e-pml4ebits-p

(defun ia32e-pml4ebits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'ia32e-pml4ebits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 64 x)
         :exec (and (natp x)
                    (< x 18446744073709551616)))))

Theorem: ia32e-pml4ebits-p-when-unsigned-byte-p

(defthm ia32e-pml4ebits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (ia32e-pml4ebits-p x)))

Theorem: unsigned-byte-p-when-ia32e-pml4ebits-p

(defthm unsigned-byte-p-when-ia32e-pml4ebits-p
  (implies (ia32e-pml4ebits-p x)
           (unsigned-byte-p 64 x)))

Theorem: ia32e-pml4ebits-p-compound-recognizer

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

Function: ia32e-pml4ebits-fix

(defun ia32e-pml4ebits-fix (x)
  (declare (xargs :guard (ia32e-pml4ebits-p x)))
  (let ((__function__ 'ia32e-pml4ebits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 64 x) :exec x)))

Theorem: ia32e-pml4ebits-p-of-ia32e-pml4ebits-fix

(defthm ia32e-pml4ebits-p-of-ia32e-pml4ebits-fix
  (b* ((fty::fixed (ia32e-pml4ebits-fix x)))
    (ia32e-pml4ebits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits-fix-when-ia32e-pml4ebits-p

(defthm ia32e-pml4ebits-fix-when-ia32e-pml4ebits-p
  (implies (ia32e-pml4ebits-p x)
           (equal (ia32e-pml4ebits-fix x) x)))

Function: ia32e-pml4ebits-equiv$inline

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

Theorem: ia32e-pml4ebits-equiv-is-an-equivalence

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

Theorem: ia32e-pml4ebits-equiv-implies-equal-ia32e-pml4ebits-fix-1

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

Theorem: ia32e-pml4ebits-fix-under-ia32e-pml4ebits-equiv

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

Function: ia32e-pml4ebits

(defun ia32e-pml4ebits (p r/w
                          u/s pwt pcd a res1 ps res2 pdpt res3 xd)
 (declare (xargs :guard (and (bitp p)
                             (bitp r/w)
                             (bitp u/s)
                             (bitp pwt)
                             (bitp pcd)
                             (bitp a)
                             (bitp res1)
                             (bitp ps)
                             (4bits-p res2)
                             (40bits-p pdpt)
                             (11bits-p res3)
                             (bitp xd))))
 (let ((__function__ 'ia32e-pml4ebits))
  (declare (ignorable __function__))
  (b* ((p (mbe :logic (bfix p) :exec p))
       (r/w (mbe :logic (bfix r/w) :exec r/w))
       (u/s (mbe :logic (bfix u/s) :exec u/s))
       (pwt (mbe :logic (bfix pwt) :exec pwt))
       (pcd (mbe :logic (bfix pcd) :exec pcd))
       (a (mbe :logic (bfix a) :exec a))
       (res1 (mbe :logic (bfix res1) :exec res1))
       (ps (mbe :logic (bfix ps) :exec ps))
       (res2 (mbe :logic (4bits-fix res2)
                  :exec res2))
       (pdpt (mbe :logic (40bits-fix pdpt)
                  :exec pdpt))
       (res3 (mbe :logic (11bits-fix res3)
                  :exec res3))
       (xd (mbe :logic (bfix xd) :exec xd)))
   (logapp
    1 p
    (logapp
     1 r/w
     (logapp
      1 u/s
      (logapp
       1 pwt
       (logapp
        1 pcd
        (logapp
         1 a
         (logapp
          1 res1
          (logapp
            1 ps
            (logapp 4 res2
                    (logapp 40 pdpt (logapp 11 res3 xd))))))))))))))

Theorem: ia32e-pml4ebits-p-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits-p-of-ia32e-pml4ebits
  (b* ((ia32e-pml4ebits
            (ia32e-pml4ebits p r/w u/s
                             pwt pcd a res1 ps res2 pdpt res3 xd)))
    (ia32e-pml4ebits-p ia32e-pml4ebits))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits-of-bfix-p

(defthm ia32e-pml4ebits-of-bfix-p
  (equal (ia32e-pml4ebits (bfix p)
                          r/w
                          u/s pwt pcd a res1 ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-p

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-p
 (implies
    (bit-equiv p p-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p-equiv r/w u/s
                            pwt pcd a res1 ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-r/w

(defthm ia32e-pml4ebits-of-bfix-r/w
  (equal (ia32e-pml4ebits p (bfix r/w)
                          u/s pwt pcd a res1 ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-r/w

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-r/w
 (implies
    (bit-equiv r/w r/w-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w-equiv u/s
                            pwt pcd a res1 ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-u/s

(defthm ia32e-pml4ebits-of-bfix-u/s
  (equal (ia32e-pml4ebits p r/w (bfix u/s)
                          pwt pcd a res1 ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-u/s

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-u/s
 (implies
    (bit-equiv u/s u/s-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s-equiv
                            pwt pcd a res1 ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-pwt

(defthm ia32e-pml4ebits-of-bfix-pwt
  (equal (ia32e-pml4ebits p r/w u/s (bfix pwt)
                          pcd a res1 ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-pwt

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-pwt
 (implies
    (bit-equiv pwt pwt-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt-equiv
                            pcd a res1 ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-pcd

(defthm ia32e-pml4ebits-of-bfix-pcd
  (equal (ia32e-pml4ebits p r/w u/s pwt (bfix pcd)
                          a res1 ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-pcd

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-pcd
 (implies
    (bit-equiv pcd pcd-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd-equiv a res1 ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-a

(defthm ia32e-pml4ebits-of-bfix-a
  (equal (ia32e-pml4ebits p r/w u/s pwt pcd (bfix a)
                          res1 ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-a

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-a
 (implies
    (bit-equiv a a-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a-equiv res1 ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-res1

(defthm ia32e-pml4ebits-of-bfix-res1
  (equal (ia32e-pml4ebits p r/w u/s pwt pcd a (bfix res1)
                          ps res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-res1

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-res1
 (implies
    (bit-equiv res1 res1-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a res1-equiv ps res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-ps

(defthm ia32e-pml4ebits-of-bfix-ps
  (equal (ia32e-pml4ebits p r/w u/s pwt pcd a res1 (bfix ps)
                          res2 pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-ps

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-ps
 (implies
    (bit-equiv ps ps-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a res1 ps-equiv res2 pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-4bits-fix-res2

(defthm ia32e-pml4ebits-of-4bits-fix-res2
  (equal (ia32e-pml4ebits p r/w
                          u/s pwt pcd a res1 ps (4bits-fix res2)
                          pdpt res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-4bits-equiv-congruence-on-res2

(defthm ia32e-pml4ebits-4bits-equiv-congruence-on-res2
 (implies
    (4bits-equiv res2 res2-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a res1 ps res2-equiv pdpt res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-40bits-fix-pdpt

(defthm ia32e-pml4ebits-of-40bits-fix-pdpt
  (equal (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 (40bits-fix pdpt)
                          res3 xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-40bits-equiv-congruence-on-pdpt

(defthm ia32e-pml4ebits-40bits-equiv-congruence-on-pdpt
 (implies
    (40bits-equiv pdpt pdpt-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a res1 ps res2 pdpt-equiv res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-11bits-fix-res3

(defthm ia32e-pml4ebits-of-11bits-fix-res3
  (equal (ia32e-pml4ebits p r/w u/s pwt pcd
                          a res1 ps res2 pdpt (11bits-fix res3)
                          xd)
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-11bits-equiv-congruence-on-res3

(defthm ia32e-pml4ebits-11bits-equiv-congruence-on-res3
 (implies
    (11bits-equiv res3 res3-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a res1 ps res2 pdpt res3-equiv xd)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits-of-bfix-xd

(defthm ia32e-pml4ebits-of-bfix-xd
  (equal (ia32e-pml4ebits p r/w u/s pwt
                          pcd a res1 ps res2 pdpt res3 (bfix xd))
         (ia32e-pml4ebits p r/w u/s
                          pwt pcd a res1 ps res2 pdpt res3 xd)))

Theorem: ia32e-pml4ebits-bit-equiv-congruence-on-xd

(defthm ia32e-pml4ebits-bit-equiv-congruence-on-xd
 (implies
    (bit-equiv xd xd-equiv)
    (equal (ia32e-pml4ebits p r/w
                            u/s pwt pcd a res1 ps res2 pdpt res3 xd)
           (ia32e-pml4ebits p r/w u/s pwt
                            pcd a res1 ps res2 pdpt res3 xd-equiv)))
 :rule-classes :congruence)

Function: ia32e-pml4ebits-equiv-under-mask

(defun ia32e-pml4ebits-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (ia32e-pml4ebits-p x)
                              (ia32e-pml4ebits-p x1)
                              (integerp mask))))
  (let ((__function__ 'ia32e-pml4ebits-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (ia32e-pml4ebits-fix x)
                               (ia32e-pml4ebits-fix x1)
                               mask)))

Function: ia32e-pml4ebits->p$inline

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

Theorem: bitp-of-ia32e-pml4ebits->p

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

Theorem: ia32e-pml4ebits->p$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->p$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->p$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->p$inline x)))

Theorem: ia32e-pml4ebits->p$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
    ia32e-pml4ebits->p$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->p$inline x)
                  (ia32e-pml4ebits->p$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->p-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->p-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->p
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix p)))

Theorem: ia32e-pml4ebits->p-of-write-with-mask

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

Function: ia32e-pml4ebits->r/w$inline

(defun ia32e-pml4ebits->r/w$inline (x)
 (declare (xargs :guard (ia32e-pml4ebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pml4ebits-fix x)))
      (part-select x :low 1 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 63)
                            (ash (the (unsigned-byte 64) x) -1))))))

Theorem: bitp-of-ia32e-pml4ebits->r/w

(defthm bitp-of-ia32e-pml4ebits->r/w
  (b* ((r/w (ia32e-pml4ebits->r/w$inline x)))
    (bitp r/w))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits->r/w$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->r/w$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->r/w$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->r/w$inline x)))

Theorem: ia32e-pml4ebits->r/w$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
  ia32e-pml4ebits->r/w$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->r/w$inline x)
                  (ia32e-pml4ebits->r/w$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->r/w-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->r/w-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->r/w
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix r/w)))

Theorem: ia32e-pml4ebits->r/w-of-write-with-mask

(defthm ia32e-pml4ebits->r/w-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x ia32e-pml4ebits-equiv-under-mask)
                (ia32e-pml4ebits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 2) 0))
           (equal (ia32e-pml4ebits->r/w x)
                  (ia32e-pml4ebits->r/w y))))

Function: ia32e-pml4ebits->u/s$inline

(defun ia32e-pml4ebits->u/s$inline (x)
 (declare (xargs :guard (ia32e-pml4ebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pml4ebits-fix x)))
      (part-select x :low 2 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 62)
                            (ash (the (unsigned-byte 64) x) -2))))))

Theorem: bitp-of-ia32e-pml4ebits->u/s

(defthm bitp-of-ia32e-pml4ebits->u/s
  (b* ((u/s (ia32e-pml4ebits->u/s$inline x)))
    (bitp u/s))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits->u/s$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->u/s$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->u/s$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->u/s$inline x)))

Theorem: ia32e-pml4ebits->u/s$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
  ia32e-pml4ebits->u/s$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->u/s$inline x)
                  (ia32e-pml4ebits->u/s$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->u/s-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->u/s-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->u/s
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix u/s)))

Theorem: ia32e-pml4ebits->u/s-of-write-with-mask

(defthm ia32e-pml4ebits->u/s-of-write-with-mask
  (implies (and (fty::bitstruct-read-over-write-hyps
                     x ia32e-pml4ebits-equiv-under-mask)
                (ia32e-pml4ebits-equiv-under-mask x y fty::mask)
                (equal (logand (lognot fty::mask) 4) 0))
           (equal (ia32e-pml4ebits->u/s x)
                  (ia32e-pml4ebits->u/s y))))

Function: ia32e-pml4ebits->pwt$inline

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

Theorem: bitp-of-ia32e-pml4ebits->pwt

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

Theorem: ia32e-pml4ebits->pwt$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->pwt$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->pwt$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->pwt$inline x)))

Theorem: ia32e-pml4ebits->pwt$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
  ia32e-pml4ebits->pwt$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->pwt$inline x)
                  (ia32e-pml4ebits->pwt$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->pwt-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->pwt-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->pwt
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix pwt)))

Theorem: ia32e-pml4ebits->pwt-of-write-with-mask

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

Function: ia32e-pml4ebits->pcd$inline

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

Theorem: bitp-of-ia32e-pml4ebits->pcd

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

Theorem: ia32e-pml4ebits->pcd$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->pcd$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->pcd$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->pcd$inline x)))

Theorem: ia32e-pml4ebits->pcd$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
  ia32e-pml4ebits->pcd$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->pcd$inline x)
                  (ia32e-pml4ebits->pcd$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->pcd-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->pcd-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->pcd
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix pcd)))

Theorem: ia32e-pml4ebits->pcd-of-write-with-mask

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

Function: ia32e-pml4ebits->a$inline

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

Theorem: bitp-of-ia32e-pml4ebits->a

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

Theorem: ia32e-pml4ebits->a$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->a$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->a$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->a$inline x)))

Theorem: ia32e-pml4ebits->a$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
    ia32e-pml4ebits->a$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->a$inline x)
                  (ia32e-pml4ebits->a$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->a-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->a-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->a
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix a)))

Theorem: ia32e-pml4ebits->a-of-write-with-mask

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

Function: ia32e-pml4ebits->res1$inline

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

Theorem: bitp-of-ia32e-pml4ebits->res1

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

Theorem: ia32e-pml4ebits->res1$inline-of-ia32e-pml4ebits-fix-x

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

Theorem: ia32e-pml4ebits->res1$inline-ia32e-pml4ebits-equiv-congruence-on-x

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

Theorem: ia32e-pml4ebits->res1-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->res1-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->res1
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix res1)))

Theorem: ia32e-pml4ebits->res1-of-write-with-mask

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

Function: ia32e-pml4ebits->ps$inline

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

Theorem: bitp-of-ia32e-pml4ebits->ps

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

Theorem: ia32e-pml4ebits->ps$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->ps$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->ps$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->ps$inline x)))

Theorem: ia32e-pml4ebits->ps$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
   ia32e-pml4ebits->ps$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->ps$inline x)
                  (ia32e-pml4ebits->ps$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->ps-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->ps-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->ps
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix ps)))

Theorem: ia32e-pml4ebits->ps-of-write-with-mask

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

Function: ia32e-pml4ebits->res2$inline

(defun ia32e-pml4ebits->res2$inline (x)
 (declare (xargs :guard (ia32e-pml4ebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pml4ebits-fix x)))
      (part-select x :low 8 :width 4))
    :exec (the (unsigned-byte 4)
               (logand (the (unsigned-byte 4) 15)
                       (the (unsigned-byte 56)
                            (ash (the (unsigned-byte 64) x) -8))))))

Theorem: 4bits-p-of-ia32e-pml4ebits->res2

(defthm 4bits-p-of-ia32e-pml4ebits->res2
  (b* ((res2 (ia32e-pml4ebits->res2$inline x)))
    (4bits-p res2))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits->res2$inline-of-ia32e-pml4ebits-fix-x

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

Theorem: ia32e-pml4ebits->res2$inline-ia32e-pml4ebits-equiv-congruence-on-x

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

Theorem: ia32e-pml4ebits->res2-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->res2-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->res2
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (4bits-fix res2)))

Theorem: ia32e-pml4ebits->res2-of-write-with-mask

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

Function: ia32e-pml4ebits->pdpt$inline

(defun ia32e-pml4ebits->pdpt$inline (x)
  (declare (xargs :guard (ia32e-pml4ebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pml4ebits-fix x)))
         (part-select x :low 12 :width 40))
       :exec (the (unsigned-byte 40)
                  (logand (the (unsigned-byte 40) 1099511627775)
                          (the (unsigned-byte 52)
                               (ash (the (unsigned-byte 64) x)
                                    -12))))))

Theorem: 40bits-p-of-ia32e-pml4ebits->pdpt

(defthm 40bits-p-of-ia32e-pml4ebits->pdpt
  (b* ((pdpt (ia32e-pml4ebits->pdpt$inline x)))
    (40bits-p pdpt))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits->pdpt$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->pdpt$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->pdpt$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->pdpt$inline x)))

Theorem: ia32e-pml4ebits->pdpt$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
 ia32e-pml4ebits->pdpt$inline-ia32e-pml4ebits-equiv-congruence-on-x
 (implies (ia32e-pml4ebits-equiv x x-equiv)
          (equal (ia32e-pml4ebits->pdpt$inline x)
                 (ia32e-pml4ebits->pdpt$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pml4ebits->pdpt-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->pdpt-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->pdpt
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (40bits-fix pdpt)))

Theorem: ia32e-pml4ebits->pdpt-of-write-with-mask

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

Function: ia32e-pml4ebits->res3$inline

(defun ia32e-pml4ebits->res3$inline (x)
  (declare (xargs :guard (ia32e-pml4ebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pml4ebits-fix x)))
         (part-select x :low 52 :width 11))
       :exec (the (unsigned-byte 11)
                  (logand (the (unsigned-byte 11) 2047)
                          (the (unsigned-byte 12)
                               (ash (the (unsigned-byte 64) x)
                                    -52))))))

Theorem: 11bits-p-of-ia32e-pml4ebits->res3

(defthm 11bits-p-of-ia32e-pml4ebits->res3
  (b* ((res3 (ia32e-pml4ebits->res3$inline x)))
    (11bits-p res3))
  :rule-classes :rewrite)

Theorem: ia32e-pml4ebits->res3$inline-of-ia32e-pml4ebits-fix-x

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

Theorem: ia32e-pml4ebits->res3$inline-ia32e-pml4ebits-equiv-congruence-on-x

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

Theorem: ia32e-pml4ebits->res3-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->res3-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->res3
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (11bits-fix res3)))

Theorem: ia32e-pml4ebits->res3-of-write-with-mask

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

Function: ia32e-pml4ebits->xd$inline

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

Theorem: bitp-of-ia32e-pml4ebits->xd

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

Theorem: ia32e-pml4ebits->xd$inline-of-ia32e-pml4ebits-fix-x

(defthm ia32e-pml4ebits->xd$inline-of-ia32e-pml4ebits-fix-x
  (equal (ia32e-pml4ebits->xd$inline (ia32e-pml4ebits-fix x))
         (ia32e-pml4ebits->xd$inline x)))

Theorem: ia32e-pml4ebits->xd$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
   ia32e-pml4ebits->xd$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (ia32e-pml4ebits->xd$inline x)
                  (ia32e-pml4ebits->xd$inline x-equiv)))
  :rule-classes :congruence)

Theorem: ia32e-pml4ebits->xd-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits->xd-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits->xd
              (ia32e-pml4ebits p r/w u/s
                               pwt pcd a res1 ps res2 pdpt res3 xd))
         (bfix xd)))

Theorem: ia32e-pml4ebits->xd-of-write-with-mask

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

Theorem: ia32e-pml4ebits-fix-in-terms-of-ia32e-pml4ebits

(defthm ia32e-pml4ebits-fix-in-terms-of-ia32e-pml4ebits
  (equal (ia32e-pml4ebits-fix x)
         (change-ia32e-pml4ebits x)))

Function: !ia32e-pml4ebits->p$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->p

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

Theorem: !ia32e-pml4ebits->p$inline-of-bfix-p

(defthm !ia32e-pml4ebits->p$inline-of-bfix-p
  (equal (!ia32e-pml4ebits->p$inline (bfix p) x)
         (!ia32e-pml4ebits->p$inline p x)))

Theorem: !ia32e-pml4ebits->p$inline-bit-equiv-congruence-on-p

(defthm !ia32e-pml4ebits->p$inline-bit-equiv-congruence-on-p
  (implies (bit-equiv p p-equiv)
           (equal (!ia32e-pml4ebits->p$inline p x)
                  (!ia32e-pml4ebits->p$inline p-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->p$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->p$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->p$inline p (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->p$inline p x)))

Theorem: !ia32e-pml4ebits->p$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
   !ia32e-pml4ebits->p$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (!ia32e-pml4ebits->p$inline p x)
                  (!ia32e-pml4ebits->p$inline p x-equiv)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->p-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->p-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->p p x)
         (change-ia32e-pml4ebits x :p p)))

Theorem: ia32e-pml4ebits->p-of-!ia32e-pml4ebits->p

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

Theorem: !ia32e-pml4ebits->p-equiv-under-mask

(defthm !ia32e-pml4ebits->p-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->p$inline p x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -2)))

Function: !ia32e-pml4ebits->r/w$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->r/w

(defthm ia32e-pml4ebits-p-of-!ia32e-pml4ebits->r/w
  (b* ((new-x (!ia32e-pml4ebits->r/w$inline r/w x)))
    (ia32e-pml4ebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pml4ebits->r/w$inline-of-bfix-r/w

(defthm !ia32e-pml4ebits->r/w$inline-of-bfix-r/w
  (equal (!ia32e-pml4ebits->r/w$inline (bfix r/w)
                                       x)
         (!ia32e-pml4ebits->r/w$inline r/w x)))

Theorem: !ia32e-pml4ebits->r/w$inline-bit-equiv-congruence-on-r/w

(defthm !ia32e-pml4ebits->r/w$inline-bit-equiv-congruence-on-r/w
  (implies (bit-equiv r/w r/w-equiv)
           (equal (!ia32e-pml4ebits->r/w$inline r/w x)
                  (!ia32e-pml4ebits->r/w$inline r/w-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->r/w$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->r/w$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->r/w$inline r/w (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->r/w$inline r/w x)))

Theorem: !ia32e-pml4ebits->r/w$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
 !ia32e-pml4ebits->r/w$inline-ia32e-pml4ebits-equiv-congruence-on-x
 (implies (ia32e-pml4ebits-equiv x x-equiv)
          (equal (!ia32e-pml4ebits->r/w$inline r/w x)
                 (!ia32e-pml4ebits->r/w$inline r/w x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->r/w-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->r/w-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->r/w r/w x)
         (change-ia32e-pml4ebits x :r/w r/w)))

Theorem: ia32e-pml4ebits->r/w-of-!ia32e-pml4ebits->r/w

(defthm ia32e-pml4ebits->r/w-of-!ia32e-pml4ebits->r/w
  (b* ((?new-x (!ia32e-pml4ebits->r/w$inline r/w x)))
    (equal (ia32e-pml4ebits->r/w new-x)
           (bfix r/w))))

Theorem: !ia32e-pml4ebits->r/w-equiv-under-mask

(defthm !ia32e-pml4ebits->r/w-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->r/w$inline r/w x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -3)))

Function: !ia32e-pml4ebits->u/s$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->u/s

(defthm ia32e-pml4ebits-p-of-!ia32e-pml4ebits->u/s
  (b* ((new-x (!ia32e-pml4ebits->u/s$inline u/s x)))
    (ia32e-pml4ebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pml4ebits->u/s$inline-of-bfix-u/s

(defthm !ia32e-pml4ebits->u/s$inline-of-bfix-u/s
  (equal (!ia32e-pml4ebits->u/s$inline (bfix u/s)
                                       x)
         (!ia32e-pml4ebits->u/s$inline u/s x)))

Theorem: !ia32e-pml4ebits->u/s$inline-bit-equiv-congruence-on-u/s

(defthm !ia32e-pml4ebits->u/s$inline-bit-equiv-congruence-on-u/s
  (implies (bit-equiv u/s u/s-equiv)
           (equal (!ia32e-pml4ebits->u/s$inline u/s x)
                  (!ia32e-pml4ebits->u/s$inline u/s-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->u/s$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->u/s$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->u/s$inline u/s (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->u/s$inline u/s x)))

Theorem: !ia32e-pml4ebits->u/s$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
 !ia32e-pml4ebits->u/s$inline-ia32e-pml4ebits-equiv-congruence-on-x
 (implies (ia32e-pml4ebits-equiv x x-equiv)
          (equal (!ia32e-pml4ebits->u/s$inline u/s x)
                 (!ia32e-pml4ebits->u/s$inline u/s x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->u/s-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->u/s-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->u/s u/s x)
         (change-ia32e-pml4ebits x :u/s u/s)))

Theorem: ia32e-pml4ebits->u/s-of-!ia32e-pml4ebits->u/s

(defthm ia32e-pml4ebits->u/s-of-!ia32e-pml4ebits->u/s
  (b* ((?new-x (!ia32e-pml4ebits->u/s$inline u/s x)))
    (equal (ia32e-pml4ebits->u/s new-x)
           (bfix u/s))))

Theorem: !ia32e-pml4ebits->u/s-equiv-under-mask

(defthm !ia32e-pml4ebits->u/s-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->u/s$inline u/s x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -5)))

Function: !ia32e-pml4ebits->pwt$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->pwt

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

Theorem: !ia32e-pml4ebits->pwt$inline-of-bfix-pwt

(defthm !ia32e-pml4ebits->pwt$inline-of-bfix-pwt
  (equal (!ia32e-pml4ebits->pwt$inline (bfix pwt)
                                       x)
         (!ia32e-pml4ebits->pwt$inline pwt x)))

Theorem: !ia32e-pml4ebits->pwt$inline-bit-equiv-congruence-on-pwt

(defthm !ia32e-pml4ebits->pwt$inline-bit-equiv-congruence-on-pwt
  (implies (bit-equiv pwt pwt-equiv)
           (equal (!ia32e-pml4ebits->pwt$inline pwt x)
                  (!ia32e-pml4ebits->pwt$inline pwt-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->pwt$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->pwt$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->pwt$inline pwt (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->pwt$inline pwt x)))

Theorem: !ia32e-pml4ebits->pwt$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
 !ia32e-pml4ebits->pwt$inline-ia32e-pml4ebits-equiv-congruence-on-x
 (implies (ia32e-pml4ebits-equiv x x-equiv)
          (equal (!ia32e-pml4ebits->pwt$inline pwt x)
                 (!ia32e-pml4ebits->pwt$inline pwt x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->pwt-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->pwt-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->pwt pwt x)
         (change-ia32e-pml4ebits x :pwt pwt)))

Theorem: ia32e-pml4ebits->pwt-of-!ia32e-pml4ebits->pwt

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

Theorem: !ia32e-pml4ebits->pwt-equiv-under-mask

(defthm !ia32e-pml4ebits->pwt-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->pwt$inline pwt x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -9)))

Function: !ia32e-pml4ebits->pcd$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->pcd

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

Theorem: !ia32e-pml4ebits->pcd$inline-of-bfix-pcd

(defthm !ia32e-pml4ebits->pcd$inline-of-bfix-pcd
  (equal (!ia32e-pml4ebits->pcd$inline (bfix pcd)
                                       x)
         (!ia32e-pml4ebits->pcd$inline pcd x)))

Theorem: !ia32e-pml4ebits->pcd$inline-bit-equiv-congruence-on-pcd

(defthm !ia32e-pml4ebits->pcd$inline-bit-equiv-congruence-on-pcd
  (implies (bit-equiv pcd pcd-equiv)
           (equal (!ia32e-pml4ebits->pcd$inline pcd x)
                  (!ia32e-pml4ebits->pcd$inline pcd-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->pcd$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->pcd$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->pcd$inline pcd (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->pcd$inline pcd x)))

Theorem: !ia32e-pml4ebits->pcd$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
 !ia32e-pml4ebits->pcd$inline-ia32e-pml4ebits-equiv-congruence-on-x
 (implies (ia32e-pml4ebits-equiv x x-equiv)
          (equal (!ia32e-pml4ebits->pcd$inline pcd x)
                 (!ia32e-pml4ebits->pcd$inline pcd x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->pcd-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->pcd-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->pcd pcd x)
         (change-ia32e-pml4ebits x :pcd pcd)))

Theorem: ia32e-pml4ebits->pcd-of-!ia32e-pml4ebits->pcd

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

Theorem: !ia32e-pml4ebits->pcd-equiv-under-mask

(defthm !ia32e-pml4ebits->pcd-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->pcd$inline pcd x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -17)))

Function: !ia32e-pml4ebits->a$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->a

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

Theorem: !ia32e-pml4ebits->a$inline-of-bfix-a

(defthm !ia32e-pml4ebits->a$inline-of-bfix-a
  (equal (!ia32e-pml4ebits->a$inline (bfix a) x)
         (!ia32e-pml4ebits->a$inline a x)))

Theorem: !ia32e-pml4ebits->a$inline-bit-equiv-congruence-on-a

(defthm !ia32e-pml4ebits->a$inline-bit-equiv-congruence-on-a
  (implies (bit-equiv a a-equiv)
           (equal (!ia32e-pml4ebits->a$inline a x)
                  (!ia32e-pml4ebits->a$inline a-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->a$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->a$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->a$inline a (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->a$inline a x)))

Theorem: !ia32e-pml4ebits->a$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
   !ia32e-pml4ebits->a$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (!ia32e-pml4ebits->a$inline a x)
                  (!ia32e-pml4ebits->a$inline a x-equiv)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->a-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->a-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->a a x)
         (change-ia32e-pml4ebits x :a a)))

Theorem: ia32e-pml4ebits->a-of-!ia32e-pml4ebits->a

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

Theorem: !ia32e-pml4ebits->a-equiv-under-mask

(defthm !ia32e-pml4ebits->a-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->a$inline a x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -33)))

Function: !ia32e-pml4ebits->res1$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->res1

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

Theorem: !ia32e-pml4ebits->res1$inline-of-bfix-res1

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

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

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

Theorem: !ia32e-pml4ebits->res1$inline-of-ia32e-pml4ebits-fix-x

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

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

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

Theorem: !ia32e-pml4ebits->res1-is-ia32e-pml4ebits

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

Theorem: ia32e-pml4ebits->res1-of-!ia32e-pml4ebits->res1

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

Theorem: !ia32e-pml4ebits->res1-equiv-under-mask

(defthm !ia32e-pml4ebits->res1-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->res1$inline res1 x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -65)))

Function: !ia32e-pml4ebits->ps$inline

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

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->ps

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

Theorem: !ia32e-pml4ebits->ps$inline-of-bfix-ps

(defthm !ia32e-pml4ebits->ps$inline-of-bfix-ps
  (equal (!ia32e-pml4ebits->ps$inline (bfix ps)
                                      x)
         (!ia32e-pml4ebits->ps$inline ps x)))

Theorem: !ia32e-pml4ebits->ps$inline-bit-equiv-congruence-on-ps

(defthm !ia32e-pml4ebits->ps$inline-bit-equiv-congruence-on-ps
  (implies (bit-equiv ps ps-equiv)
           (equal (!ia32e-pml4ebits->ps$inline ps x)
                  (!ia32e-pml4ebits->ps$inline ps-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->ps$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->ps$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->ps$inline ps (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->ps$inline ps x)))

Theorem: !ia32e-pml4ebits->ps$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
  !ia32e-pml4ebits->ps$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (!ia32e-pml4ebits->ps$inline ps x)
                  (!ia32e-pml4ebits->ps$inline ps x-equiv)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->ps-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->ps-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->ps ps x)
         (change-ia32e-pml4ebits x :ps ps)))

Theorem: ia32e-pml4ebits->ps-of-!ia32e-pml4ebits->ps

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

Theorem: !ia32e-pml4ebits->ps-equiv-under-mask

(defthm !ia32e-pml4ebits->ps-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->ps$inline ps x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -129)))

Function: !ia32e-pml4ebits->res2$inline

(defun !ia32e-pml4ebits->res2$inline (res2 x)
 (declare (xargs :guard (and (4bits-p res2)
                             (ia32e-pml4ebits-p x))))
 (mbe :logic
      (b* ((res2 (mbe :logic (4bits-fix res2)
                      :exec res2))
           (x (ia32e-pml4ebits-fix x)))
        (part-install res2 x :width 4 :low 8))
      :exec (the (unsigned-byte 64)
                 (logior (the (unsigned-byte 64)
                              (logand (the (unsigned-byte 64) x)
                                      (the (signed-byte 13) -3841)))
                         (the (unsigned-byte 12)
                              (ash (the (unsigned-byte 4) res2)
                                   8))))))

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->res2

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

Theorem: !ia32e-pml4ebits->res2$inline-of-4bits-fix-res2

(defthm !ia32e-pml4ebits->res2$inline-of-4bits-fix-res2
  (equal (!ia32e-pml4ebits->res2$inline (4bits-fix res2)
                                        x)
         (!ia32e-pml4ebits->res2$inline res2 x)))

Theorem: !ia32e-pml4ebits->res2$inline-4bits-equiv-congruence-on-res2

(defthm !ia32e-pml4ebits->res2$inline-4bits-equiv-congruence-on-res2
  (implies (4bits-equiv res2 res2-equiv)
           (equal (!ia32e-pml4ebits->res2$inline res2 x)
                  (!ia32e-pml4ebits->res2$inline res2-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->res2$inline-of-ia32e-pml4ebits-fix-x

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

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

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

Theorem: !ia32e-pml4ebits->res2-is-ia32e-pml4ebits

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

Theorem: ia32e-pml4ebits->res2-of-!ia32e-pml4ebits->res2

(defthm ia32e-pml4ebits->res2-of-!ia32e-pml4ebits->res2
  (b* ((?new-x (!ia32e-pml4ebits->res2$inline res2 x)))
    (equal (ia32e-pml4ebits->res2 new-x)
           (4bits-fix res2))))

Theorem: !ia32e-pml4ebits->res2-equiv-under-mask

(defthm !ia32e-pml4ebits->res2-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->res2$inline res2 x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -3841)))

Function: !ia32e-pml4ebits->pdpt$inline

(defun !ia32e-pml4ebits->pdpt$inline (pdpt x)
  (declare (xargs :guard (and (40bits-p pdpt)
                              (ia32e-pml4ebits-p x))))
  (mbe :logic
       (b* ((pdpt (mbe :logic (40bits-fix pdpt)
                       :exec pdpt))
            (x (ia32e-pml4ebits-fix x)))
         (part-install pdpt x :width 40 :low 12))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 53)
                                            -4503599627366401)))
                          (the (unsigned-byte 52)
                               (ash (the (unsigned-byte 40) pdpt)
                                    12))))))

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->pdpt

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

Theorem: !ia32e-pml4ebits->pdpt$inline-of-40bits-fix-pdpt

(defthm !ia32e-pml4ebits->pdpt$inline-of-40bits-fix-pdpt
  (equal (!ia32e-pml4ebits->pdpt$inline (40bits-fix pdpt)
                                        x)
         (!ia32e-pml4ebits->pdpt$inline pdpt x)))

Theorem: !ia32e-pml4ebits->pdpt$inline-40bits-equiv-congruence-on-pdpt

(defthm
      !ia32e-pml4ebits->pdpt$inline-40bits-equiv-congruence-on-pdpt
  (implies (40bits-equiv pdpt pdpt-equiv)
           (equal (!ia32e-pml4ebits->pdpt$inline pdpt x)
                  (!ia32e-pml4ebits->pdpt$inline pdpt-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->pdpt$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->pdpt$inline-of-ia32e-pml4ebits-fix-x
 (equal (!ia32e-pml4ebits->pdpt$inline pdpt (ia32e-pml4ebits-fix x))
        (!ia32e-pml4ebits->pdpt$inline pdpt x)))

Theorem: !ia32e-pml4ebits->pdpt$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
 !ia32e-pml4ebits->pdpt$inline-ia32e-pml4ebits-equiv-congruence-on-x
 (implies (ia32e-pml4ebits-equiv x x-equiv)
          (equal (!ia32e-pml4ebits->pdpt$inline pdpt x)
                 (!ia32e-pml4ebits->pdpt$inline pdpt x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->pdpt-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->pdpt-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->pdpt pdpt x)
         (change-ia32e-pml4ebits x :pdpt pdpt)))

Theorem: ia32e-pml4ebits->pdpt-of-!ia32e-pml4ebits->pdpt

(defthm ia32e-pml4ebits->pdpt-of-!ia32e-pml4ebits->pdpt
  (b* ((?new-x (!ia32e-pml4ebits->pdpt$inline pdpt x)))
    (equal (ia32e-pml4ebits->pdpt new-x)
           (40bits-fix pdpt))))

Theorem: !ia32e-pml4ebits->pdpt-equiv-under-mask

(defthm !ia32e-pml4ebits->pdpt-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->pdpt$inline pdpt x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x -4503599627366401)))

Function: !ia32e-pml4ebits->res3$inline

(defun !ia32e-pml4ebits->res3$inline (res3 x)
  (declare (xargs :guard (and (11bits-p res3)
                              (ia32e-pml4ebits-p x))))
  (mbe :logic
       (b* ((res3 (mbe :logic (11bits-fix res3)
                       :exec res3))
            (x (ia32e-pml4ebits-fix x)))
         (part-install res3 x :width 11 :low 52))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 64)
                                            -9218868437227405313)))
                          (the (unsigned-byte 63)
                               (ash (the (unsigned-byte 11) res3)
                                    52))))))

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->res3

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

Theorem: !ia32e-pml4ebits->res3$inline-of-11bits-fix-res3

(defthm !ia32e-pml4ebits->res3$inline-of-11bits-fix-res3
  (equal (!ia32e-pml4ebits->res3$inline (11bits-fix res3)
                                        x)
         (!ia32e-pml4ebits->res3$inline res3 x)))

Theorem: !ia32e-pml4ebits->res3$inline-11bits-equiv-congruence-on-res3

(defthm
      !ia32e-pml4ebits->res3$inline-11bits-equiv-congruence-on-res3
  (implies (11bits-equiv res3 res3-equiv)
           (equal (!ia32e-pml4ebits->res3$inline res3 x)
                  (!ia32e-pml4ebits->res3$inline res3-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->res3$inline-of-ia32e-pml4ebits-fix-x

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

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

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

Theorem: !ia32e-pml4ebits->res3-is-ia32e-pml4ebits

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

Theorem: ia32e-pml4ebits->res3-of-!ia32e-pml4ebits->res3

(defthm ia32e-pml4ebits->res3-of-!ia32e-pml4ebits->res3
  (b* ((?new-x (!ia32e-pml4ebits->res3$inline res3 x)))
    (equal (ia32e-pml4ebits->res3 new-x)
           (11bits-fix res3))))

Theorem: !ia32e-pml4ebits->res3-equiv-under-mask

(defthm !ia32e-pml4ebits->res3-equiv-under-mask
 (b* ((?new-x (!ia32e-pml4ebits->res3$inline res3 x)))
   (ia32e-pml4ebits-equiv-under-mask new-x x -9218868437227405313)))

Function: !ia32e-pml4ebits->xd$inline

(defun !ia32e-pml4ebits->xd$inline (xd x)
 (declare (xargs :guard (and (bitp xd) (ia32e-pml4ebits-p x))))
 (mbe
    :logic
    (b* ((xd (mbe :logic (bfix xd) :exec xd))
         (x (ia32e-pml4ebits-fix x)))
      (part-install xd x :width 1 :low 63))
    :exec (the (unsigned-byte 64)
               (logior (the (unsigned-byte 64)
                            (logand (the (unsigned-byte 64) x)
                                    (the (signed-byte 65)
                                         -9223372036854775809)))
                       (the (unsigned-byte 64)
                            (ash (the (unsigned-byte 1) xd) 63))))))

Theorem: ia32e-pml4ebits-p-of-!ia32e-pml4ebits->xd

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

Theorem: !ia32e-pml4ebits->xd$inline-of-bfix-xd

(defthm !ia32e-pml4ebits->xd$inline-of-bfix-xd
  (equal (!ia32e-pml4ebits->xd$inline (bfix xd)
                                      x)
         (!ia32e-pml4ebits->xd$inline xd x)))

Theorem: !ia32e-pml4ebits->xd$inline-bit-equiv-congruence-on-xd

(defthm !ia32e-pml4ebits->xd$inline-bit-equiv-congruence-on-xd
  (implies (bit-equiv xd xd-equiv)
           (equal (!ia32e-pml4ebits->xd$inline xd x)
                  (!ia32e-pml4ebits->xd$inline xd-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->xd$inline-of-ia32e-pml4ebits-fix-x

(defthm !ia32e-pml4ebits->xd$inline-of-ia32e-pml4ebits-fix-x
  (equal (!ia32e-pml4ebits->xd$inline xd (ia32e-pml4ebits-fix x))
         (!ia32e-pml4ebits->xd$inline xd x)))

Theorem: !ia32e-pml4ebits->xd$inline-ia32e-pml4ebits-equiv-congruence-on-x

(defthm
  !ia32e-pml4ebits->xd$inline-ia32e-pml4ebits-equiv-congruence-on-x
  (implies (ia32e-pml4ebits-equiv x x-equiv)
           (equal (!ia32e-pml4ebits->xd$inline xd x)
                  (!ia32e-pml4ebits->xd$inline xd x-equiv)))
  :rule-classes :congruence)

Theorem: !ia32e-pml4ebits->xd-is-ia32e-pml4ebits

(defthm !ia32e-pml4ebits->xd-is-ia32e-pml4ebits
  (equal (!ia32e-pml4ebits->xd xd x)
         (change-ia32e-pml4ebits x :xd xd)))

Theorem: ia32e-pml4ebits->xd-of-!ia32e-pml4ebits->xd

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

Theorem: !ia32e-pml4ebits->xd-equiv-under-mask

(defthm !ia32e-pml4ebits->xd-equiv-under-mask
  (b* ((?new-x (!ia32e-pml4ebits->xd$inline xd x)))
    (ia32e-pml4ebits-equiv-under-mask new-x x 9223372036854775807)))

Function: ia32e-pml4ebits-debug

(defun ia32e-pml4ebits-debug (x)
 (declare (xargs :guard (ia32e-pml4ebits-p x)))
 (let ((__function__ 'ia32e-pml4ebits-debug))
  (declare (ignorable __function__))
  (b* (((ia32e-pml4ebits x)))
   (cons
    (cons 'p x.p)
    (cons
     (cons 'r/w x.r/w)
     (cons
      (cons 'u/s x.u/s)
      (cons
       (cons 'pwt x.pwt)
       (cons
        (cons 'pcd x.pcd)
        (cons
         (cons 'a x.a)
         (cons
          (cons 'res1 x.res1)
          (cons
           (cons 'ps x.ps)
           (cons
                (cons 'res2 x.res2)
                (cons (cons 'pdpt x.pdpt)
                      (cons (cons 'res3 x.res3)
                            (cons (cons 'xd x.xd) nil)))))))))))))))

Subtopics

Ia32e-pml4ebits-p: Recognizer for ia32e-pml4ebits bit structures.
!ia32e-pml4ebits->res3: Update the |X86ISA|::|RES3| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->pdpt: Update the |X86ISA|::|PDPT| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->res2: Update the |X86ISA|::|RES2| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->res1: Update the |X86ISA|::|RES1| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->xd: Update the |X86ISA|::|XD| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->u/s: Update the |X86ISA|::|U/S| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->r/w: Update the |X86ISA|::|R/W| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->pwt: Update the |X86ISA|::|PWT| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->pcd: Update the |X86ISA|::|PCD| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->ps: Update the |X86ISA|::|PS| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->a: Update the |ACL2|::|A| field of a ia32e-pml4ebits bit structure.
!ia32e-pml4ebits->p: Update the |ACL2|::|P| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->res3: Access the |X86ISA|::|RES3| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->pdpt: Access the |X86ISA|::|PDPT| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits-fix: Fixing function for ia32e-pml4ebits bit structures.
Ia32e-pml4ebits->xd: Access the |X86ISA|::|XD| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->u/s: Access the |X86ISA|::|U/S| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->r/w: Access the |X86ISA|::|R/W| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->res2: Access the |X86ISA|::|RES2| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->res1: Access the |X86ISA|::|RES1| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->pwt: Access the |X86ISA|::|PWT| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->ps: Access the |X86ISA|::|PS| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->pcd: Access the |X86ISA|::|PCD| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->p: Access the |ACL2|::|P| field of a ia32e-pml4ebits bit structure.
Ia32e-pml4ebits->a: Access the |ACL2|::|A| field of a ia32e-pml4ebits bit structure.