		Search-engine friendly clone of the ACL2 documentation.

Paging-bitstructs

Ia32e-pde-2mb-pagebits

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
d — bit
ps — bit
g — bit
res1 — 3bits
pat — bit
res2 — 8bits
page — 31bits
res3 — 11bits
xd — bit

Definitions and Theorems

Function: ia32e-pde-2mb-pagebits-p

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

Theorem: ia32e-pde-2mb-pagebits-p-when-unsigned-byte-p

(defthm ia32e-pde-2mb-pagebits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (ia32e-pde-2mb-pagebits-p x)))

Theorem: unsigned-byte-p-when-ia32e-pde-2mb-pagebits-p

(defthm unsigned-byte-p-when-ia32e-pde-2mb-pagebits-p
  (implies (ia32e-pde-2mb-pagebits-p x)
           (unsigned-byte-p 64 x)))

Theorem: ia32e-pde-2mb-pagebits-p-compound-recognizer

(defthm ia32e-pde-2mb-pagebits-p-compound-recognizer
  (implies (ia32e-pde-2mb-pagebits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: ia32e-pde-2mb-pagebits-fix

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

Theorem: ia32e-pde-2mb-pagebits-p-of-ia32e-pde-2mb-pagebits-fix

(defthm ia32e-pde-2mb-pagebits-p-of-ia32e-pde-2mb-pagebits-fix
  (b* ((fty::fixed (ia32e-pde-2mb-pagebits-fix x)))
    (ia32e-pde-2mb-pagebits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits-fix-when-ia32e-pde-2mb-pagebits-p

(defthm ia32e-pde-2mb-pagebits-fix-when-ia32e-pde-2mb-pagebits-p
  (implies (ia32e-pde-2mb-pagebits-p x)
           (equal (ia32e-pde-2mb-pagebits-fix x)
                  x)))

Function: ia32e-pde-2mb-pagebits-equiv$inline

(defun ia32e-pde-2mb-pagebits-equiv$inline (x y)
  (declare (xargs :guard (and (ia32e-pde-2mb-pagebits-p x)
                              (ia32e-pde-2mb-pagebits-p y))))
  (equal (ia32e-pde-2mb-pagebits-fix x)
         (ia32e-pde-2mb-pagebits-fix y)))

Theorem: ia32e-pde-2mb-pagebits-equiv-is-an-equivalence

(defthm ia32e-pde-2mb-pagebits-equiv-is-an-equivalence
  (and (booleanp (ia32e-pde-2mb-pagebits-equiv x y))
       (ia32e-pde-2mb-pagebits-equiv x x)
       (implies (ia32e-pde-2mb-pagebits-equiv x y)
                (ia32e-pde-2mb-pagebits-equiv y x))
       (implies (and (ia32e-pde-2mb-pagebits-equiv x y)
                     (ia32e-pde-2mb-pagebits-equiv y z))
                (ia32e-pde-2mb-pagebits-equiv x z)))
  :rule-classes (:equivalence))

Theorem: ia32e-pde-2mb-pagebits-equiv-implies-equal-ia32e-pde-2mb-pagebits-fix-1

(defthm
 ia32e-pde-2mb-pagebits-equiv-implies-equal-ia32e-pde-2mb-pagebits-fix-1
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits-fix x)
                 (ia32e-pde-2mb-pagebits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: ia32e-pde-2mb-pagebits-fix-under-ia32e-pde-2mb-pagebits-equiv

(defthm
      ia32e-pde-2mb-pagebits-fix-under-ia32e-pde-2mb-pagebits-equiv
  (ia32e-pde-2mb-pagebits-equiv (ia32e-pde-2mb-pagebits-fix x)
                                x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: ia32e-pde-2mb-pagebits

(defun ia32e-pde-2mb-pagebits
       (p r/w u/s pwt
          pcd a d ps g res1 pat res2 page res3 xd)
 (declare (xargs :guard (and (bitp p)
                             (bitp r/w)
                             (bitp u/s)
                             (bitp pwt)
                             (bitp pcd)
                             (bitp a)
                             (bitp d)
                             (bitp ps)
                             (bitp g)
                             (3bits-p res1)
                             (bitp pat)
                             (8bits-p res2)
                             (31bits-p page)
                             (11bits-p res3)
                             (bitp xd))))
 (let ((__function__ 'ia32e-pde-2mb-pagebits))
  (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))
       (d (mbe :logic (bfix d) :exec d))
       (ps (mbe :logic (bfix ps) :exec ps))
       (g (mbe :logic (bfix g) :exec g))
       (res1 (mbe :logic (3bits-fix res1)
                  :exec res1))
       (pat (mbe :logic (bfix pat) :exec pat))
       (res2 (mbe :logic (8bits-fix res2)
                  :exec res2))
       (page (mbe :logic (31bits-fix page)
                  :exec page))
       (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 d
          (logapp
           1 ps
           (logapp
            1 g
            (logapp
             3 res1
             (logapp
               1 pat
               (logapp
                    8 res2
                    (logapp 31
                            page (logapp 11 res3 xd)))))))))))))))))

Theorem: ia32e-pde-2mb-pagebits-p-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits-p-of-ia32e-pde-2mb-pagebits
 (b*
  ((ia32e-pde-2mb-pagebits
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))
  (ia32e-pde-2mb-pagebits-p ia32e-pde-2mb-pagebits))
 :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-p

(defthm ia32e-pde-2mb-pagebits-of-bfix-p
 (equal
    (ia32e-pde-2mb-pagebits (bfix p)
                            r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-p

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-p
 (implies
  (bit-equiv p p-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p-equiv r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-r/w

(defthm ia32e-pde-2mb-pagebits-of-bfix-r/w
 (equal
    (ia32e-pde-2mb-pagebits p (bfix r/w)
                            u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-r/w

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-r/w
 (implies
  (bit-equiv r/w r/w-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w-equiv u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-u/s

(defthm ia32e-pde-2mb-pagebits-of-bfix-u/s
 (equal
    (ia32e-pde-2mb-pagebits p r/w (bfix u/s)
                            pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-u/s

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-u/s
 (implies
  (bit-equiv u/s u/s-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s-equiv pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-pwt

(defthm ia32e-pde-2mb-pagebits-of-bfix-pwt
 (equal
    (ia32e-pde-2mb-pagebits p r/w u/s (bfix pwt)
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-pwt

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-pwt
 (implies
  (bit-equiv pwt pwt-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt-equiv pcd
                            a d ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-pcd

(defthm ia32e-pde-2mb-pagebits-of-bfix-pcd
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt (bfix pcd)
                              a d ps g res1 pat res2 page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-pcd

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-pcd
 (implies
  (bit-equiv pcd pcd-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd-equiv
                            a d ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-a

(defthm ia32e-pde-2mb-pagebits-of-bfix-a
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd (bfix a)
                              d ps g res1 pat res2 page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-a

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-a
 (implies
  (bit-equiv a a-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a-equiv
                            d ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-d

(defthm ia32e-pde-2mb-pagebits-of-bfix-d
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a (bfix d)
                              ps g res1 pat res2 page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-d

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-d
 (implies
  (bit-equiv d d-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d-equiv
                            ps g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-ps

(defthm ia32e-pde-2mb-pagebits-of-bfix-ps
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d (bfix ps)
                              g res1 pat res2 page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-ps

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-ps
 (implies
  (bit-equiv ps ps-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps-equiv g res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-g

(defthm ia32e-pde-2mb-pagebits-of-bfix-g
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d ps (bfix g)
                              res1 pat res2 page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-g

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-g
 (implies
  (bit-equiv g g-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g-equiv res1 pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-3bits-fix-res1

(defthm ia32e-pde-2mb-pagebits-of-3bits-fix-res1
 (equal
      (ia32e-pde-2mb-pagebits p r/w
                              u/s pwt pcd a d ps g (3bits-fix res1)
                              pat res2 page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-3bits-equiv-congruence-on-res1

(defthm ia32e-pde-2mb-pagebits-3bits-equiv-congruence-on-res1
 (implies
  (3bits-equiv res1 res1-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g res1-equiv pat res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-pat

(defthm ia32e-pde-2mb-pagebits-of-bfix-pat
 (equal
    (ia32e-pde-2mb-pagebits p
                            r/w u/s pwt pcd a d ps g res1 (bfix pat)
                            res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-pat

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-pat
 (implies
  (bit-equiv pat pat-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g res1 pat-equiv res2 page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-8bits-fix-res2

(defthm ia32e-pde-2mb-pagebits-of-8bits-fix-res2
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt
                              pcd a d ps g res1 pat (8bits-fix res2)
                              page res3 xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-8bits-equiv-congruence-on-res2

(defthm ia32e-pde-2mb-pagebits-8bits-equiv-congruence-on-res2
 (implies
  (8bits-equiv res2 res2-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g res1 pat res2-equiv page res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-31bits-fix-page

(defthm ia32e-pde-2mb-pagebits-of-31bits-fix-page
 (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 (31bits-fix page)
                            res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                            a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-31bits-equiv-congruence-on-page

(defthm ia32e-pde-2mb-pagebits-31bits-equiv-congruence-on-page
 (implies
  (31bits-equiv page page-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g res1 pat res2 page-equiv res3 xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-11bits-fix-res3

(defthm ia32e-pde-2mb-pagebits-of-11bits-fix-res3
 (equal
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d ps
                              g res1 pat res2 page (11bits-fix res3)
                              xd)
      (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                              a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-11bits-equiv-congruence-on-res3

(defthm ia32e-pde-2mb-pagebits-11bits-equiv-congruence-on-res3
 (implies
  (11bits-equiv res3 res3-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g res1 pat res2 page res3-equiv xd)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits-of-bfix-xd

(defthm ia32e-pde-2mb-pagebits-of-bfix-xd
 (equal
     (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                             ps g res1 pat res2 page res3 (bfix xd))
     (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                             a d ps g res1 pat res2 page res3 xd)))

Theorem: ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-xd

(defthm ia32e-pde-2mb-pagebits-bit-equiv-congruence-on-xd
 (implies
  (bit-equiv xd xd-equiv)
  (equal
    (ia32e-pde-2mb-pagebits p r/w u/s pwt
                            pcd a d ps g res1 pat res2 page res3 xd)
    (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd a d
                            ps g res1 pat res2 page res3 xd-equiv)))
 :rule-classes :congruence)

Function: ia32e-pde-2mb-pagebits-equiv-under-mask

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

Function: ia32e-pde-2mb-pagebits->p$inline

(defun ia32e-pde-2mb-pagebits->p$inline (x)
  (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->p

(defthm bitp-of-ia32e-pde-2mb-pagebits->p
  (b* ((p (ia32e-pde-2mb-pagebits->p$inline x)))
    (bitp p))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->p$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
   ia32e-pde-2mb-pagebits->p$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal
   (ia32e-pde-2mb-pagebits->p$inline (ia32e-pde-2mb-pagebits-fix x))
   (ia32e-pde-2mb-pagebits->p$inline x)))

Theorem: ia32e-pde-2mb-pagebits->p$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->p$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->p$inline x)
                 (ia32e-pde-2mb-pagebits->p$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->p-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->p-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->p
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix p)))

Theorem: ia32e-pde-2mb-pagebits->p-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->r/w$inline

(defun ia32e-pde-2mb-pagebits->r/w$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->r/w

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

Theorem: ia32e-pde-2mb-pagebits->r/w$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->r/w$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->r/w$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->r/w$inline x)))

Theorem: ia32e-pde-2mb-pagebits->r/w$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-2mb-pagebits->r/w-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->r/w-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->r/w
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix r/w)))

Theorem: ia32e-pde-2mb-pagebits->r/w-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->u/s$inline

(defun ia32e-pde-2mb-pagebits->u/s$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->u/s

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

Theorem: ia32e-pde-2mb-pagebits->u/s$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->u/s$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->u/s$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->u/s$inline x)))

Theorem: ia32e-pde-2mb-pagebits->u/s$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-2mb-pagebits->u/s-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->u/s-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->u/s
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix u/s)))

Theorem: ia32e-pde-2mb-pagebits->u/s-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->pwt$inline

(defun ia32e-pde-2mb-pagebits->pwt$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->pwt

(defthm bitp-of-ia32e-pde-2mb-pagebits->pwt
  (b* ((pwt (ia32e-pde-2mb-pagebits->pwt$inline x)))
    (bitp pwt))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->pwt$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->pwt$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->pwt$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->pwt$inline x)))

Theorem: ia32e-pde-2mb-pagebits->pwt$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->pwt$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->pwt$inline x)
                 (ia32e-pde-2mb-pagebits->pwt$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->pwt-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->pwt-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->pwt
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix pwt)))

Theorem: ia32e-pde-2mb-pagebits->pwt-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->pcd$inline

(defun ia32e-pde-2mb-pagebits->pcd$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->pcd

(defthm bitp-of-ia32e-pde-2mb-pagebits->pcd
  (b* ((pcd (ia32e-pde-2mb-pagebits->pcd$inline x)))
    (bitp pcd))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->pcd$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->pcd$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->pcd$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->pcd$inline x)))

Theorem: ia32e-pde-2mb-pagebits->pcd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->pcd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->pcd$inline x)
                 (ia32e-pde-2mb-pagebits->pcd$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->pcd-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->pcd-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->pcd
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix pcd)))

Theorem: ia32e-pde-2mb-pagebits->pcd-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->a$inline

(defun ia32e-pde-2mb-pagebits->a$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->a

(defthm bitp-of-ia32e-pde-2mb-pagebits->a
  (b* ((a (ia32e-pde-2mb-pagebits->a$inline x)))
    (bitp a))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->a$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
   ia32e-pde-2mb-pagebits->a$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal
   (ia32e-pde-2mb-pagebits->a$inline (ia32e-pde-2mb-pagebits-fix x))
   (ia32e-pde-2mb-pagebits->a$inline x)))

Theorem: ia32e-pde-2mb-pagebits->a$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->a$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->a$inline x)
                 (ia32e-pde-2mb-pagebits->a$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->a-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->a-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->a
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix a)))

Theorem: ia32e-pde-2mb-pagebits->a-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->d$inline

(defun ia32e-pde-2mb-pagebits->d$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->d

(defthm bitp-of-ia32e-pde-2mb-pagebits->d
  (b* ((d (ia32e-pde-2mb-pagebits->d$inline x)))
    (bitp d))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->d$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
   ia32e-pde-2mb-pagebits->d$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal
   (ia32e-pde-2mb-pagebits->d$inline (ia32e-pde-2mb-pagebits-fix x))
   (ia32e-pde-2mb-pagebits->d$inline x)))

Theorem: ia32e-pde-2mb-pagebits->d$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->d$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->d$inline x)
                 (ia32e-pde-2mb-pagebits->d$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->d-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->d-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->d
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix d)))

Theorem: ia32e-pde-2mb-pagebits->d-of-write-with-mask

(defthm ia32e-pde-2mb-pagebits->d-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pde-2mb-pagebits-equiv-under-mask)
            (ia32e-pde-2mb-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 64)
                   0))
       (equal (ia32e-pde-2mb-pagebits->d x)
              (ia32e-pde-2mb-pagebits->d y))))

Function: ia32e-pde-2mb-pagebits->ps$inline

(defun ia32e-pde-2mb-pagebits->ps$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->ps

(defthm bitp-of-ia32e-pde-2mb-pagebits->ps
  (b* ((ps (ia32e-pde-2mb-pagebits->ps$inline x)))
    (bitp ps))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->ps$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
  ia32e-pde-2mb-pagebits->ps$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal
  (ia32e-pde-2mb-pagebits->ps$inline (ia32e-pde-2mb-pagebits-fix x))
  (ia32e-pde-2mb-pagebits->ps$inline x)))

Theorem: ia32e-pde-2mb-pagebits->ps$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->ps$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->ps$inline x)
                 (ia32e-pde-2mb-pagebits->ps$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->ps-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->ps-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->ps
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix ps)))

Theorem: ia32e-pde-2mb-pagebits->ps-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->g$inline

(defun ia32e-pde-2mb-pagebits->g$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-fix x)))
      (part-select x :low 8 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 56)
                            (ash (the (unsigned-byte 64) x) -8))))))

Theorem: bitp-of-ia32e-pde-2mb-pagebits->g

(defthm bitp-of-ia32e-pde-2mb-pagebits->g
  (b* ((g (ia32e-pde-2mb-pagebits->g$inline x)))
    (bitp g))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->g$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
   ia32e-pde-2mb-pagebits->g$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal
   (ia32e-pde-2mb-pagebits->g$inline (ia32e-pde-2mb-pagebits-fix x))
   (ia32e-pde-2mb-pagebits->g$inline x)))

Theorem: ia32e-pde-2mb-pagebits->g$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->g$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->g$inline x)
                 (ia32e-pde-2mb-pagebits->g$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->g-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->g-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->g
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix g)))

Theorem: ia32e-pde-2mb-pagebits->g-of-write-with-mask

(defthm ia32e-pde-2mb-pagebits->g-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pde-2mb-pagebits-equiv-under-mask)
            (ia32e-pde-2mb-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 256)
                   0))
       (equal (ia32e-pde-2mb-pagebits->g x)
              (ia32e-pde-2mb-pagebits->g y))))

Function: ia32e-pde-2mb-pagebits->res1$inline

(defun ia32e-pde-2mb-pagebits->res1$inline (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (mbe
    :logic
    (let ((x (ia32e-pde-2mb-pagebits-fix x)))
      (part-select x :low 9 :width 3))
    :exec (the (unsigned-byte 3)
               (logand (the (unsigned-byte 3) 7)
                       (the (unsigned-byte 55)
                            (ash (the (unsigned-byte 64) x) -9))))))

Theorem: 3bits-p-of-ia32e-pde-2mb-pagebits->res1

(defthm 3bits-p-of-ia32e-pde-2mb-pagebits->res1
  (b* ((res1 (ia32e-pde-2mb-pagebits->res1$inline x)))
    (3bits-p res1))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->res1$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->res1$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->res1$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->res1$inline x)))

Theorem: ia32e-pde-2mb-pagebits->res1$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->res1$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->res1$inline x)
                 (ia32e-pde-2mb-pagebits->res1$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->res1-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->res1-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->res1
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (3bits-fix res1)))

Theorem: ia32e-pde-2mb-pagebits->res1-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->pat$inline

(defun ia32e-pde-2mb-pagebits->pat$inline (x)
  (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pde-2mb-pagebits-fix x)))
         (part-select x :low 12 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 52)
                               (ash (the (unsigned-byte 64) x)
                                    -12))))))

Theorem: bitp-of-ia32e-pde-2mb-pagebits->pat

(defthm bitp-of-ia32e-pde-2mb-pagebits->pat
  (b* ((pat (ia32e-pde-2mb-pagebits->pat$inline x)))
    (bitp pat))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->pat$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->pat$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->pat$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->pat$inline x)))

Theorem: ia32e-pde-2mb-pagebits->pat$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->pat$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->pat$inline x)
                 (ia32e-pde-2mb-pagebits->pat$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->pat-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->pat-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->pat
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix pat)))

Theorem: ia32e-pde-2mb-pagebits->pat-of-write-with-mask

(defthm ia32e-pde-2mb-pagebits->pat-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pde-2mb-pagebits-equiv-under-mask)
            (ia32e-pde-2mb-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 4096)
                   0))
       (equal (ia32e-pde-2mb-pagebits->pat x)
              (ia32e-pde-2mb-pagebits->pat y))))

Function: ia32e-pde-2mb-pagebits->res2$inline

(defun ia32e-pde-2mb-pagebits->res2$inline (x)
  (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pde-2mb-pagebits-fix x)))
         (part-select x :low 13 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 51)
                               (ash (the (unsigned-byte 64) x)
                                    -13))))))

Theorem: 8bits-p-of-ia32e-pde-2mb-pagebits->res2

(defthm 8bits-p-of-ia32e-pde-2mb-pagebits->res2
  (b* ((res2 (ia32e-pde-2mb-pagebits->res2$inline x)))
    (8bits-p res2))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->res2$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->res2$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->res2$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->res2$inline x)))

Theorem: ia32e-pde-2mb-pagebits->res2$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->res2$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->res2$inline x)
                 (ia32e-pde-2mb-pagebits->res2$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->res2-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->res2-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->res2
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (8bits-fix res2)))

Theorem: ia32e-pde-2mb-pagebits->res2-of-write-with-mask

(defthm ia32e-pde-2mb-pagebits->res2-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pde-2mb-pagebits-equiv-under-mask)
            (ia32e-pde-2mb-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 2088960)
                   0))
       (equal (ia32e-pde-2mb-pagebits->res2 x)
              (ia32e-pde-2mb-pagebits->res2 y))))

Function: ia32e-pde-2mb-pagebits->page$inline

(defun ia32e-pde-2mb-pagebits->page$inline (x)
  (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pde-2mb-pagebits-fix x)))
         (part-select x :low 21 :width 31))
       :exec (the (unsigned-byte 31)
                  (logand (the (unsigned-byte 31) 2147483647)
                          (the (unsigned-byte 43)
                               (ash (the (unsigned-byte 64) x)
                                    -21))))))

Theorem: 31bits-p-of-ia32e-pde-2mb-pagebits->page

(defthm 31bits-p-of-ia32e-pde-2mb-pagebits->page
  (b* ((page (ia32e-pde-2mb-pagebits->page$inline x)))
    (31bits-p page))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->page$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->page$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->page$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->page$inline x)))

Theorem: ia32e-pde-2mb-pagebits->page$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->page$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->page$inline x)
                 (ia32e-pde-2mb-pagebits->page$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->page-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->page-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->page
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (31bits-fix page)))

Theorem: ia32e-pde-2mb-pagebits->page-of-write-with-mask

(defthm ia32e-pde-2mb-pagebits->page-of-write-with-mask
  (implies
       (and (fty::bitstruct-read-over-write-hyps
                 x
                 ia32e-pde-2mb-pagebits-equiv-under-mask)
            (ia32e-pde-2mb-pagebits-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask)
                           4503599625273344)
                   0))
       (equal (ia32e-pde-2mb-pagebits->page x)
              (ia32e-pde-2mb-pagebits->page y))))

Function: ia32e-pde-2mb-pagebits->res3$inline

(defun ia32e-pde-2mb-pagebits->res3$inline (x)
  (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->res3

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

Theorem: ia32e-pde-2mb-pagebits->res3$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 ia32e-pde-2mb-pagebits->res3$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (ia32e-pde-2mb-pagebits->res3$inline
             (ia32e-pde-2mb-pagebits-fix x))
        (ia32e-pde-2mb-pagebits->res3$inline x)))

Theorem: ia32e-pde-2mb-pagebits->res3$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->res3$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->res3$inline x)
                 (ia32e-pde-2mb-pagebits->res3$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->res3-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->res3-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->res3
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (11bits-fix res3)))

Theorem: ia32e-pde-2mb-pagebits->res3-of-write-with-mask

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

Function: ia32e-pde-2mb-pagebits->xd$inline

(defun ia32e-pde-2mb-pagebits->xd$inline (x)
  (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
  (mbe :logic
       (let ((x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits->xd

(defthm bitp-of-ia32e-pde-2mb-pagebits->xd
  (b* ((xd (ia32e-pde-2mb-pagebits->xd$inline x)))
    (bitp xd))
  :rule-classes :rewrite)

Theorem: ia32e-pde-2mb-pagebits->xd$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
  ia32e-pde-2mb-pagebits->xd$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal
  (ia32e-pde-2mb-pagebits->xd$inline (ia32e-pde-2mb-pagebits-fix x))
  (ia32e-pde-2mb-pagebits->xd$inline x)))

Theorem: ia32e-pde-2mb-pagebits->xd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 ia32e-pde-2mb-pagebits->xd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (ia32e-pde-2mb-pagebits->xd$inline x)
                 (ia32e-pde-2mb-pagebits->xd$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-2mb-pagebits->xd-of-ia32e-pde-2mb-pagebits

(defthm ia32e-pde-2mb-pagebits->xd-of-ia32e-pde-2mb-pagebits
 (equal
  (ia32e-pde-2mb-pagebits->xd
       (ia32e-pde-2mb-pagebits p r/w u/s pwt pcd
                               a d ps g res1 pat res2 page res3 xd))
  (bfix xd)))

Theorem: ia32e-pde-2mb-pagebits->xd-of-write-with-mask

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

Theorem: ia32e-pde-2mb-pagebits-fix-in-terms-of-ia32e-pde-2mb-pagebits

(defthm
      ia32e-pde-2mb-pagebits-fix-in-terms-of-ia32e-pde-2mb-pagebits
  (equal (ia32e-pde-2mb-pagebits-fix x)
         (change-ia32e-pde-2mb-pagebits x)))

Function: !ia32e-pde-2mb-pagebits->p$inline

(defun !ia32e-pde-2mb-pagebits->p$inline (p x)
  (declare (xargs :guard (and (bitp p)
                              (ia32e-pde-2mb-pagebits-p x))))
  (mbe :logic
       (b* ((p (mbe :logic (bfix p) :exec p))
            (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->p

(defthm ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->p
  (b* ((new-x (!ia32e-pde-2mb-pagebits->p$inline p x)))
    (ia32e-pde-2mb-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pde-2mb-pagebits->p$inline-of-bfix-p

(defthm !ia32e-pde-2mb-pagebits->p$inline-of-bfix-p
  (equal (!ia32e-pde-2mb-pagebits->p$inline (bfix p)
                                            x)
         (!ia32e-pde-2mb-pagebits->p$inline p x)))

Theorem: !ia32e-pde-2mb-pagebits->p$inline-bit-equiv-congruence-on-p

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

Theorem: !ia32e-pde-2mb-pagebits->p$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
  !ia32e-pde-2mb-pagebits->p$inline-of-ia32e-pde-2mb-pagebits-fix-x
  (equal (!ia32e-pde-2mb-pagebits->p$inline
              p (ia32e-pde-2mb-pagebits-fix x))
         (!ia32e-pde-2mb-pagebits->p$inline p x)))

Theorem: !ia32e-pde-2mb-pagebits->p$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->p$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->p$inline p x)
                 (!ia32e-pde-2mb-pagebits->p$inline p x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->p-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->p-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->p p x)
         (change-ia32e-pde-2mb-pagebits x :p p)))

Theorem: ia32e-pde-2mb-pagebits->p-of-!ia32e-pde-2mb-pagebits->p

(defthm ia32e-pde-2mb-pagebits->p-of-!ia32e-pde-2mb-pagebits->p
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->p$inline p x)))
    (equal (ia32e-pde-2mb-pagebits->p new-x)
           (bfix p))))

Theorem: !ia32e-pde-2mb-pagebits->p-equiv-under-mask

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

Function: !ia32e-pde-2mb-pagebits->r/w$inline

(defun !ia32e-pde-2mb-pagebits->r/w$inline (r/w x)
 (declare (xargs :guard (and (bitp r/w)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
    :logic
    (b* ((r/w (mbe :logic (bfix r/w) :exec r/w))
         (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->r/w

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

Theorem: !ia32e-pde-2mb-pagebits->r/w$inline-of-bfix-r/w

(defthm !ia32e-pde-2mb-pagebits->r/w$inline-of-bfix-r/w
  (equal (!ia32e-pde-2mb-pagebits->r/w$inline (bfix r/w)
                                              x)
         (!ia32e-pde-2mb-pagebits->r/w$inline r/w x)))

Theorem: !ia32e-pde-2mb-pagebits->r/w$inline-bit-equiv-congruence-on-r/w

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

Theorem: !ia32e-pde-2mb-pagebits->r/w$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->r/w$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->r/w$inline
             r/w (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->r/w$inline r/w x)))

Theorem: !ia32e-pde-2mb-pagebits->r/w$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-2mb-pagebits->r/w-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->r/w-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->r/w r/w x)
         (change-ia32e-pde-2mb-pagebits x
                                        :r/w r/w)))

Theorem: ia32e-pde-2mb-pagebits->r/w-of-!ia32e-pde-2mb-pagebits->r/w

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

Theorem: !ia32e-pde-2mb-pagebits->r/w-equiv-under-mask

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

Function: !ia32e-pde-2mb-pagebits->u/s$inline

(defun !ia32e-pde-2mb-pagebits->u/s$inline (u/s x)
 (declare (xargs :guard (and (bitp u/s)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
    :logic
    (b* ((u/s (mbe :logic (bfix u/s) :exec u/s))
         (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->u/s

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

Theorem: !ia32e-pde-2mb-pagebits->u/s$inline-of-bfix-u/s

(defthm !ia32e-pde-2mb-pagebits->u/s$inline-of-bfix-u/s
  (equal (!ia32e-pde-2mb-pagebits->u/s$inline (bfix u/s)
                                              x)
         (!ia32e-pde-2mb-pagebits->u/s$inline u/s x)))

Theorem: !ia32e-pde-2mb-pagebits->u/s$inline-bit-equiv-congruence-on-u/s

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

Theorem: !ia32e-pde-2mb-pagebits->u/s$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->u/s$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->u/s$inline
             u/s (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->u/s$inline u/s x)))

Theorem: !ia32e-pde-2mb-pagebits->u/s$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-2mb-pagebits->u/s-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->u/s-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->u/s u/s x)
         (change-ia32e-pde-2mb-pagebits x
                                        :u/s u/s)))

Theorem: ia32e-pde-2mb-pagebits->u/s-of-!ia32e-pde-2mb-pagebits->u/s

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

Theorem: !ia32e-pde-2mb-pagebits->u/s-equiv-under-mask

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

Function: !ia32e-pde-2mb-pagebits->pwt$inline

(defun !ia32e-pde-2mb-pagebits->pwt$inline (pwt x)
 (declare (xargs :guard (and (bitp pwt)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
    :logic
    (b* ((pwt (mbe :logic (bfix pwt) :exec pwt))
         (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->pwt

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

Theorem: !ia32e-pde-2mb-pagebits->pwt$inline-of-bfix-pwt

(defthm !ia32e-pde-2mb-pagebits->pwt$inline-of-bfix-pwt
  (equal (!ia32e-pde-2mb-pagebits->pwt$inline (bfix pwt)
                                              x)
         (!ia32e-pde-2mb-pagebits->pwt$inline pwt x)))

Theorem: !ia32e-pde-2mb-pagebits->pwt$inline-bit-equiv-congruence-on-pwt

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

Theorem: !ia32e-pde-2mb-pagebits->pwt$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->pwt$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->pwt$inline
             pwt (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->pwt$inline pwt x)))

Theorem: !ia32e-pde-2mb-pagebits->pwt$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->pwt$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->pwt$inline pwt x)
                 (!ia32e-pde-2mb-pagebits->pwt$inline pwt x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->pwt-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->pwt-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->pwt pwt x)
         (change-ia32e-pde-2mb-pagebits x
                                        :pwt pwt)))

Theorem: ia32e-pde-2mb-pagebits->pwt-of-!ia32e-pde-2mb-pagebits->pwt

(defthm ia32e-pde-2mb-pagebits->pwt-of-!ia32e-pde-2mb-pagebits->pwt
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->pwt$inline pwt x)))
    (equal (ia32e-pde-2mb-pagebits->pwt new-x)
           (bfix pwt))))

Theorem: !ia32e-pde-2mb-pagebits->pwt-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->pwt-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->pwt$inline pwt x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -9)))

Function: !ia32e-pde-2mb-pagebits->pcd$inline

(defun !ia32e-pde-2mb-pagebits->pcd$inline (pcd x)
 (declare (xargs :guard (and (bitp pcd)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
    :logic
    (b* ((pcd (mbe :logic (bfix pcd) :exec pcd))
         (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->pcd

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

Theorem: !ia32e-pde-2mb-pagebits->pcd$inline-of-bfix-pcd

(defthm !ia32e-pde-2mb-pagebits->pcd$inline-of-bfix-pcd
  (equal (!ia32e-pde-2mb-pagebits->pcd$inline (bfix pcd)
                                              x)
         (!ia32e-pde-2mb-pagebits->pcd$inline pcd x)))

Theorem: !ia32e-pde-2mb-pagebits->pcd$inline-bit-equiv-congruence-on-pcd

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

Theorem: !ia32e-pde-2mb-pagebits->pcd$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->pcd$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->pcd$inline
             pcd (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->pcd$inline pcd x)))

Theorem: !ia32e-pde-2mb-pagebits->pcd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->pcd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->pcd$inline pcd x)
                 (!ia32e-pde-2mb-pagebits->pcd$inline pcd x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->pcd-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->pcd-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->pcd pcd x)
         (change-ia32e-pde-2mb-pagebits x
                                        :pcd pcd)))

Theorem: ia32e-pde-2mb-pagebits->pcd-of-!ia32e-pde-2mb-pagebits->pcd

(defthm ia32e-pde-2mb-pagebits->pcd-of-!ia32e-pde-2mb-pagebits->pcd
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->pcd$inline pcd x)))
    (equal (ia32e-pde-2mb-pagebits->pcd new-x)
           (bfix pcd))))

Theorem: !ia32e-pde-2mb-pagebits->pcd-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->pcd-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->pcd$inline pcd x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -17)))

Function: !ia32e-pde-2mb-pagebits->a$inline

(defun !ia32e-pde-2mb-pagebits->a$inline (a x)
 (declare (xargs :guard (and (bitp a)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe :logic
      (b* ((a (mbe :logic (bfix a) :exec a))
           (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->a

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

Theorem: !ia32e-pde-2mb-pagebits->a$inline-of-bfix-a

(defthm !ia32e-pde-2mb-pagebits->a$inline-of-bfix-a
  (equal (!ia32e-pde-2mb-pagebits->a$inline (bfix a)
                                            x)
         (!ia32e-pde-2mb-pagebits->a$inline a x)))

Theorem: !ia32e-pde-2mb-pagebits->a$inline-bit-equiv-congruence-on-a

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

Theorem: !ia32e-pde-2mb-pagebits->a$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
  !ia32e-pde-2mb-pagebits->a$inline-of-ia32e-pde-2mb-pagebits-fix-x
  (equal (!ia32e-pde-2mb-pagebits->a$inline
              a (ia32e-pde-2mb-pagebits-fix x))
         (!ia32e-pde-2mb-pagebits->a$inline a x)))

Theorem: !ia32e-pde-2mb-pagebits->a$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->a$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->a$inline a x)
                 (!ia32e-pde-2mb-pagebits->a$inline a x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->a-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->a-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->a a x)
         (change-ia32e-pde-2mb-pagebits x :a a)))

Theorem: ia32e-pde-2mb-pagebits->a-of-!ia32e-pde-2mb-pagebits->a

(defthm ia32e-pde-2mb-pagebits->a-of-!ia32e-pde-2mb-pagebits->a
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->a$inline a x)))
    (equal (ia32e-pde-2mb-pagebits->a new-x)
           (bfix a))))

Theorem: !ia32e-pde-2mb-pagebits->a-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->a-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->a$inline a x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -33)))

Function: !ia32e-pde-2mb-pagebits->d$inline

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

Theorem: ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->d

(defthm ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->d
  (b* ((new-x (!ia32e-pde-2mb-pagebits->d$inline d x)))
    (ia32e-pde-2mb-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pde-2mb-pagebits->d$inline-of-bfix-d

(defthm !ia32e-pde-2mb-pagebits->d$inline-of-bfix-d
  (equal (!ia32e-pde-2mb-pagebits->d$inline (bfix d)
                                            x)
         (!ia32e-pde-2mb-pagebits->d$inline d x)))

Theorem: !ia32e-pde-2mb-pagebits->d$inline-bit-equiv-congruence-on-d

(defthm !ia32e-pde-2mb-pagebits->d$inline-bit-equiv-congruence-on-d
  (implies (bit-equiv d d-equiv)
           (equal (!ia32e-pde-2mb-pagebits->d$inline d x)
                  (!ia32e-pde-2mb-pagebits->d$inline d-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->d$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
  !ia32e-pde-2mb-pagebits->d$inline-of-ia32e-pde-2mb-pagebits-fix-x
  (equal (!ia32e-pde-2mb-pagebits->d$inline
              d (ia32e-pde-2mb-pagebits-fix x))
         (!ia32e-pde-2mb-pagebits->d$inline d x)))

Theorem: !ia32e-pde-2mb-pagebits->d$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->d$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->d$inline d x)
                 (!ia32e-pde-2mb-pagebits->d$inline d x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->d-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->d-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->d d x)
         (change-ia32e-pde-2mb-pagebits x :d d)))

Theorem: ia32e-pde-2mb-pagebits->d-of-!ia32e-pde-2mb-pagebits->d

(defthm ia32e-pde-2mb-pagebits->d-of-!ia32e-pde-2mb-pagebits->d
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->d$inline d x)))
    (equal (ia32e-pde-2mb-pagebits->d new-x)
           (bfix d))))

Theorem: !ia32e-pde-2mb-pagebits->d-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->d-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->d$inline d x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -65)))

Function: !ia32e-pde-2mb-pagebits->ps$inline

(defun !ia32e-pde-2mb-pagebits->ps$inline (ps x)
 (declare (xargs :guard (and (bitp ps)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
     :logic
     (b* ((ps (mbe :logic (bfix ps) :exec ps))
          (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->ps

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

Theorem: !ia32e-pde-2mb-pagebits->ps$inline-of-bfix-ps

(defthm !ia32e-pde-2mb-pagebits->ps$inline-of-bfix-ps
  (equal (!ia32e-pde-2mb-pagebits->ps$inline (bfix ps)
                                             x)
         (!ia32e-pde-2mb-pagebits->ps$inline ps x)))

Theorem: !ia32e-pde-2mb-pagebits->ps$inline-bit-equiv-congruence-on-ps

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

Theorem: !ia32e-pde-2mb-pagebits->ps$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->ps$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->ps$inline
             ps (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->ps$inline ps x)))

Theorem: !ia32e-pde-2mb-pagebits->ps$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->ps$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->ps$inline ps x)
                 (!ia32e-pde-2mb-pagebits->ps$inline ps x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->ps-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->ps-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->ps ps x)
         (change-ia32e-pde-2mb-pagebits x
                                        :ps ps)))

Theorem: ia32e-pde-2mb-pagebits->ps-of-!ia32e-pde-2mb-pagebits->ps

(defthm ia32e-pde-2mb-pagebits->ps-of-!ia32e-pde-2mb-pagebits->ps
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->ps$inline ps x)))
    (equal (ia32e-pde-2mb-pagebits->ps new-x)
           (bfix ps))))

Theorem: !ia32e-pde-2mb-pagebits->ps-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->ps-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->ps$inline ps x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -129)))

Function: !ia32e-pde-2mb-pagebits->g$inline

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

Theorem: ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->g

(defthm ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->g
  (b* ((new-x (!ia32e-pde-2mb-pagebits->g$inline g x)))
    (ia32e-pde-2mb-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pde-2mb-pagebits->g$inline-of-bfix-g

(defthm !ia32e-pde-2mb-pagebits->g$inline-of-bfix-g
  (equal (!ia32e-pde-2mb-pagebits->g$inline (bfix g)
                                            x)
         (!ia32e-pde-2mb-pagebits->g$inline g x)))

Theorem: !ia32e-pde-2mb-pagebits->g$inline-bit-equiv-congruence-on-g

(defthm !ia32e-pde-2mb-pagebits->g$inline-bit-equiv-congruence-on-g
  (implies (bit-equiv g g-equiv)
           (equal (!ia32e-pde-2mb-pagebits->g$inline g x)
                  (!ia32e-pde-2mb-pagebits->g$inline g-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->g$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
  !ia32e-pde-2mb-pagebits->g$inline-of-ia32e-pde-2mb-pagebits-fix-x
  (equal (!ia32e-pde-2mb-pagebits->g$inline
              g (ia32e-pde-2mb-pagebits-fix x))
         (!ia32e-pde-2mb-pagebits->g$inline g x)))

Theorem: !ia32e-pde-2mb-pagebits->g$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->g$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->g$inline g x)
                 (!ia32e-pde-2mb-pagebits->g$inline g x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->g-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->g-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->g g x)
         (change-ia32e-pde-2mb-pagebits x :g g)))

Theorem: ia32e-pde-2mb-pagebits->g-of-!ia32e-pde-2mb-pagebits->g

(defthm ia32e-pde-2mb-pagebits->g-of-!ia32e-pde-2mb-pagebits->g
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->g$inline g x)))
    (equal (ia32e-pde-2mb-pagebits->g new-x)
           (bfix g))))

Theorem: !ia32e-pde-2mb-pagebits->g-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->g-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->g$inline g x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -257)))

Function: !ia32e-pde-2mb-pagebits->res1$inline

(defun !ia32e-pde-2mb-pagebits->res1$inline (res1 x)
 (declare (xargs :guard (and (3bits-p res1)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe :logic
      (b* ((res1 (mbe :logic (3bits-fix res1)
                      :exec res1))
           (x (ia32e-pde-2mb-pagebits-fix x)))
        (part-install res1 x :width 3 :low 9))
      :exec (the (unsigned-byte 64)
                 (logior (the (unsigned-byte 64)
                              (logand (the (unsigned-byte 64) x)
                                      (the (signed-byte 13) -3585)))
                         (the (unsigned-byte 12)
                              (ash (the (unsigned-byte 3) res1)
                                   9))))))

Theorem: ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->res1

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

Theorem: !ia32e-pde-2mb-pagebits->res1$inline-of-3bits-fix-res1

(defthm !ia32e-pde-2mb-pagebits->res1$inline-of-3bits-fix-res1
  (equal (!ia32e-pde-2mb-pagebits->res1$inline (3bits-fix res1)
                                               x)
         (!ia32e-pde-2mb-pagebits->res1$inline res1 x)))

Theorem: !ia32e-pde-2mb-pagebits->res1$inline-3bits-equiv-congruence-on-res1

(defthm
 !ia32e-pde-2mb-pagebits->res1$inline-3bits-equiv-congruence-on-res1
 (implies
      (3bits-equiv res1 res1-equiv)
      (equal (!ia32e-pde-2mb-pagebits->res1$inline res1 x)
             (!ia32e-pde-2mb-pagebits->res1$inline res1-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->res1$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->res1$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->res1$inline
             res1 (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->res1$inline res1 x)))

Theorem: !ia32e-pde-2mb-pagebits->res1$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->res1$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pde-2mb-pagebits-equiv x x-equiv)
      (equal (!ia32e-pde-2mb-pagebits->res1$inline res1 x)
             (!ia32e-pde-2mb-pagebits->res1$inline res1 x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->res1-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->res1-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->res1 res1 x)
         (change-ia32e-pde-2mb-pagebits x
                                        :res1 res1)))

Theorem: ia32e-pde-2mb-pagebits->res1-of-!ia32e-pde-2mb-pagebits->res1

(defthm
      ia32e-pde-2mb-pagebits->res1-of-!ia32e-pde-2mb-pagebits->res1
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->res1$inline res1 x)))
    (equal (ia32e-pde-2mb-pagebits->res1 new-x)
           (3bits-fix res1))))

Theorem: !ia32e-pde-2mb-pagebits->res1-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->res1-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->res1$inline res1 x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -3585)))

Function: !ia32e-pde-2mb-pagebits->pat$inline

(defun !ia32e-pde-2mb-pagebits->pat$inline (pat x)
 (declare (xargs :guard (and (bitp pat)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe :logic
      (b* ((pat (mbe :logic (bfix pat) :exec pat))
           (x (ia32e-pde-2mb-pagebits-fix x)))
        (part-install pat x :width 1 :low 12))
      :exec (the (unsigned-byte 64)
                 (logior (the (unsigned-byte 64)
                              (logand (the (unsigned-byte 64) x)
                                      (the (signed-byte 14) -4097)))
                         (the (unsigned-byte 13)
                              (ash (the (unsigned-byte 1) pat)
                                   12))))))

Theorem: ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->pat

(defthm ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->pat
  (b* ((new-x (!ia32e-pde-2mb-pagebits->pat$inline pat x)))
    (ia32e-pde-2mb-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pde-2mb-pagebits->pat$inline-of-bfix-pat

(defthm !ia32e-pde-2mb-pagebits->pat$inline-of-bfix-pat
  (equal (!ia32e-pde-2mb-pagebits->pat$inline (bfix pat)
                                              x)
         (!ia32e-pde-2mb-pagebits->pat$inline pat x)))

Theorem: !ia32e-pde-2mb-pagebits->pat$inline-bit-equiv-congruence-on-pat

(defthm
    !ia32e-pde-2mb-pagebits->pat$inline-bit-equiv-congruence-on-pat
 (implies (bit-equiv pat pat-equiv)
          (equal (!ia32e-pde-2mb-pagebits->pat$inline pat x)
                 (!ia32e-pde-2mb-pagebits->pat$inline pat-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->pat$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->pat$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->pat$inline
             pat (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->pat$inline pat x)))

Theorem: !ia32e-pde-2mb-pagebits->pat$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->pat$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->pat$inline pat x)
                 (!ia32e-pde-2mb-pagebits->pat$inline pat x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->pat-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->pat-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->pat pat x)
         (change-ia32e-pde-2mb-pagebits x
                                        :pat pat)))

Theorem: ia32e-pde-2mb-pagebits->pat-of-!ia32e-pde-2mb-pagebits->pat

(defthm ia32e-pde-2mb-pagebits->pat-of-!ia32e-pde-2mb-pagebits->pat
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->pat$inline pat x)))
    (equal (ia32e-pde-2mb-pagebits->pat new-x)
           (bfix pat))))

Theorem: !ia32e-pde-2mb-pagebits->pat-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->pat-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->pat$inline pat x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -4097)))

Function: !ia32e-pde-2mb-pagebits->res2$inline

(defun !ia32e-pde-2mb-pagebits->res2$inline (res2 x)
 (declare (xargs :guard (and (8bits-p res2)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
   :logic
   (b* ((res2 (mbe :logic (8bits-fix res2)
                   :exec res2))
        (x (ia32e-pde-2mb-pagebits-fix x)))
     (part-install res2 x :width 8 :low 13))
   :exec (the (unsigned-byte 64)
              (logior (the (unsigned-byte 64)
                           (logand (the (unsigned-byte 64) x)
                                   (the (signed-byte 22) -2088961)))
                      (the (unsigned-byte 21)
                           (ash (the (unsigned-byte 8) res2)
                                13))))))

Theorem: ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->res2

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

Theorem: !ia32e-pde-2mb-pagebits->res2$inline-of-8bits-fix-res2

(defthm !ia32e-pde-2mb-pagebits->res2$inline-of-8bits-fix-res2
  (equal (!ia32e-pde-2mb-pagebits->res2$inline (8bits-fix res2)
                                               x)
         (!ia32e-pde-2mb-pagebits->res2$inline res2 x)))

Theorem: !ia32e-pde-2mb-pagebits->res2$inline-8bits-equiv-congruence-on-res2

(defthm
 !ia32e-pde-2mb-pagebits->res2$inline-8bits-equiv-congruence-on-res2
 (implies
      (8bits-equiv res2 res2-equiv)
      (equal (!ia32e-pde-2mb-pagebits->res2$inline res2 x)
             (!ia32e-pde-2mb-pagebits->res2$inline res2-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->res2$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->res2$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->res2$inline
             res2 (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->res2$inline res2 x)))

Theorem: !ia32e-pde-2mb-pagebits->res2$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->res2$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pde-2mb-pagebits-equiv x x-equiv)
      (equal (!ia32e-pde-2mb-pagebits->res2$inline res2 x)
             (!ia32e-pde-2mb-pagebits->res2$inline res2 x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->res2-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->res2-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->res2 res2 x)
         (change-ia32e-pde-2mb-pagebits x
                                        :res2 res2)))

Theorem: ia32e-pde-2mb-pagebits->res2-of-!ia32e-pde-2mb-pagebits->res2

(defthm
      ia32e-pde-2mb-pagebits->res2-of-!ia32e-pde-2mb-pagebits->res2
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->res2$inline res2 x)))
    (equal (ia32e-pde-2mb-pagebits->res2 new-x)
           (8bits-fix res2))))

Theorem: !ia32e-pde-2mb-pagebits->res2-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->res2-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->res2$inline res2 x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask new-x x -2088961)))

Function: !ia32e-pde-2mb-pagebits->page$inline

(defun !ia32e-pde-2mb-pagebits->page$inline (page x)
  (declare (xargs :guard (and (31bits-p page)
                              (ia32e-pde-2mb-pagebits-p x))))
  (mbe :logic
       (b* ((page (mbe :logic (31bits-fix page)
                       :exec page))
            (x (ia32e-pde-2mb-pagebits-fix x)))
         (part-install page x :width 31 :low 21))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 53)
                                            -4503599625273345)))
                          (the (unsigned-byte 52)
                               (ash (the (unsigned-byte 31) page)
                                    21))))))

Theorem: ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->page

(defthm ia32e-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->page
  (b* ((new-x (!ia32e-pde-2mb-pagebits->page$inline page x)))
    (ia32e-pde-2mb-pagebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pde-2mb-pagebits->page$inline-of-31bits-fix-page

(defthm !ia32e-pde-2mb-pagebits->page$inline-of-31bits-fix-page
  (equal (!ia32e-pde-2mb-pagebits->page$inline (31bits-fix page)
                                               x)
         (!ia32e-pde-2mb-pagebits->page$inline page x)))

Theorem: !ia32e-pde-2mb-pagebits->page$inline-31bits-equiv-congruence-on-page

(defthm
 !ia32e-pde-2mb-pagebits->page$inline-31bits-equiv-congruence-on-page
 (implies
      (31bits-equiv page page-equiv)
      (equal (!ia32e-pde-2mb-pagebits->page$inline page x)
             (!ia32e-pde-2mb-pagebits->page$inline page-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->page$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->page$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->page$inline
             page (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->page$inline page x)))

Theorem: !ia32e-pde-2mb-pagebits->page$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->page$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pde-2mb-pagebits-equiv x x-equiv)
      (equal (!ia32e-pde-2mb-pagebits->page$inline page x)
             (!ia32e-pde-2mb-pagebits->page$inline page x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->page-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->page-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->page page x)
         (change-ia32e-pde-2mb-pagebits x
                                        :page page)))

Theorem: ia32e-pde-2mb-pagebits->page-of-!ia32e-pde-2mb-pagebits->page

(defthm
      ia32e-pde-2mb-pagebits->page-of-!ia32e-pde-2mb-pagebits->page
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->page$inline page x)))
    (equal (ia32e-pde-2mb-pagebits->page new-x)
           (31bits-fix page))))

Theorem: !ia32e-pde-2mb-pagebits->page-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->page-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->page$inline page x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask
         new-x x -4503599625273345)))

Function: !ia32e-pde-2mb-pagebits->res3$inline

(defun !ia32e-pde-2mb-pagebits->res3$inline (res3 x)
  (declare (xargs :guard (and (11bits-p res3)
                              (ia32e-pde-2mb-pagebits-p x))))
  (mbe :logic
       (b* ((res3 (mbe :logic (11bits-fix res3)
                       :exec res3))
            (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->res3

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

Theorem: !ia32e-pde-2mb-pagebits->res3$inline-of-11bits-fix-res3

(defthm !ia32e-pde-2mb-pagebits->res3$inline-of-11bits-fix-res3
  (equal (!ia32e-pde-2mb-pagebits->res3$inline (11bits-fix res3)
                                               x)
         (!ia32e-pde-2mb-pagebits->res3$inline res3 x)))

Theorem: !ia32e-pde-2mb-pagebits->res3$inline-11bits-equiv-congruence-on-res3

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

Theorem: !ia32e-pde-2mb-pagebits->res3$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->res3$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->res3$inline
             res3 (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->res3$inline res3 x)))

Theorem: !ia32e-pde-2mb-pagebits->res3$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->res3$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies
      (ia32e-pde-2mb-pagebits-equiv x x-equiv)
      (equal (!ia32e-pde-2mb-pagebits->res3$inline res3 x)
             (!ia32e-pde-2mb-pagebits->res3$inline res3 x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->res3-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->res3-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->res3 res3 x)
         (change-ia32e-pde-2mb-pagebits x
                                        :res3 res3)))

Theorem: ia32e-pde-2mb-pagebits->res3-of-!ia32e-pde-2mb-pagebits->res3

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

Theorem: !ia32e-pde-2mb-pagebits->res3-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->res3-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->res3$inline res3 x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask
         new-x x -9218868437227405313)))

Function: !ia32e-pde-2mb-pagebits->xd$inline

(defun !ia32e-pde-2mb-pagebits->xd$inline (xd x)
 (declare (xargs :guard (and (bitp xd)
                             (ia32e-pde-2mb-pagebits-p x))))
 (mbe
    :logic
    (b* ((xd (mbe :logic (bfix xd) :exec xd))
         (x (ia32e-pde-2mb-pagebits-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-pde-2mb-pagebits-p-of-!ia32e-pde-2mb-pagebits->xd

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

Theorem: !ia32e-pde-2mb-pagebits->xd$inline-of-bfix-xd

(defthm !ia32e-pde-2mb-pagebits->xd$inline-of-bfix-xd
  (equal (!ia32e-pde-2mb-pagebits->xd$inline (bfix xd)
                                             x)
         (!ia32e-pde-2mb-pagebits->xd$inline xd x)))

Theorem: !ia32e-pde-2mb-pagebits->xd$inline-bit-equiv-congruence-on-xd

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

Theorem: !ia32e-pde-2mb-pagebits->xd$inline-of-ia32e-pde-2mb-pagebits-fix-x

(defthm
 !ia32e-pde-2mb-pagebits->xd$inline-of-ia32e-pde-2mb-pagebits-fix-x
 (equal (!ia32e-pde-2mb-pagebits->xd$inline
             xd (ia32e-pde-2mb-pagebits-fix x))
        (!ia32e-pde-2mb-pagebits->xd$inline xd x)))

Theorem: !ia32e-pde-2mb-pagebits->xd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-2mb-pagebits->xd$inline-ia32e-pde-2mb-pagebits-equiv-congruence-on-x
 (implies (ia32e-pde-2mb-pagebits-equiv x x-equiv)
          (equal (!ia32e-pde-2mb-pagebits->xd$inline xd x)
                 (!ia32e-pde-2mb-pagebits->xd$inline xd x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-2mb-pagebits->xd-is-ia32e-pde-2mb-pagebits

(defthm !ia32e-pde-2mb-pagebits->xd-is-ia32e-pde-2mb-pagebits
  (equal (!ia32e-pde-2mb-pagebits->xd xd x)
         (change-ia32e-pde-2mb-pagebits x
                                        :xd xd)))

Theorem: ia32e-pde-2mb-pagebits->xd-of-!ia32e-pde-2mb-pagebits->xd

(defthm ia32e-pde-2mb-pagebits->xd-of-!ia32e-pde-2mb-pagebits->xd
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->xd$inline xd x)))
    (equal (ia32e-pde-2mb-pagebits->xd new-x)
           (bfix xd))))

Theorem: !ia32e-pde-2mb-pagebits->xd-equiv-under-mask

(defthm !ia32e-pde-2mb-pagebits->xd-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-2mb-pagebits->xd$inline xd x)))
    (ia32e-pde-2mb-pagebits-equiv-under-mask
         new-x x 9223372036854775807)))

Function: ia32e-pde-2mb-pagebits-debug

(defun ia32e-pde-2mb-pagebits-debug (x)
 (declare (xargs :guard (ia32e-pde-2mb-pagebits-p x)))
 (let ((__function__ 'ia32e-pde-2mb-pagebits-debug))
  (declare (ignorable __function__))
  (b* (((ia32e-pde-2mb-pagebits 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 'd x.d)
          (cons
           (cons 'ps x.ps)
           (cons
            (cons 'g x.g)
            (cons
                 (cons 'res1 x.res1)
                 (cons (cons 'pat x.pat)
                       (cons (cons 'res2 x.res2)
                             (cons (cons 'page x.page)
                                   (cons (cons 'res3 x.res3)
                                         (cons (cons 'xd x.xd)
                                               nil))))))))))))))))))

Subtopics

Ia32e-pde-2mb-pagebits-p: Recognizer for ia32e-pde-2mb-pagebits bit structures.
!ia32e-pde-2mb-pagebits->res3: Update the |X86ISA|::|RES3| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->page: Update the |X86ISA|::|PAGE| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->res2: Update the |X86ISA|::|RES2| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->res1: Update the |X86ISA|::|RES1| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->xd: Update the |X86ISA|::|XD| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->u/s: Update the |X86ISA|::|U/S| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->r/w: Update the |X86ISA|::|R/W| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->pwt: Update the |X86ISA|::|PWT| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->pcd: Update the |X86ISA|::|PCD| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->pat: Update the |X86ISA|::|PAT| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->ps: Update the |X86ISA|::|PS| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->p: Update the |ACL2|::|P| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->g: Update the |X86ISA|::|G| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->d: Update the |ACL2|::|D| field of a ia32e-pde-2mb-pagebits bit structure.
!ia32e-pde-2mb-pagebits->a: Update the |ACL2|::|A| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits-fix: Fixing function for ia32e-pde-2mb-pagebits bit structures.
Ia32e-pde-2mb-pagebits->res3: Access the |X86ISA|::|RES3| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->page: Access the |X86ISA|::|PAGE| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->xd: Access the |X86ISA|::|XD| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->res2: Access the |X86ISA|::|RES2| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->res1: Access the |X86ISA|::|RES1| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->pcd: Access the |X86ISA|::|PCD| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->pat: Access the |X86ISA|::|PAT| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->u/s: Access the |X86ISA|::|U/S| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->r/w: Access the |X86ISA|::|R/W| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->pwt: Access the |X86ISA|::|PWT| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->ps: Access the |X86ISA|::|PS| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->g: Access the |X86ISA|::|G| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->d: Access the |ACL2|::|D| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->a: Access the |ACL2|::|A| field of a ia32e-pde-2mb-pagebits bit structure.
Ia32e-pde-2mb-pagebits->p: Access the |ACL2|::|P| field of a ia32e-pde-2mb-pagebits bit structure.