		Search-engine friendly clone of the ACL2 documentation.

Paging-bitstructs

Ia32e-page-tablesbits

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
res1 — 4bits
reference-addr — 40bits
res2 — 11bits
xd — bit

Definitions and Theorems

Function: ia32e-page-tablesbits-p

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

Theorem: ia32e-page-tablesbits-p-when-unsigned-byte-p

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

Theorem: unsigned-byte-p-when-ia32e-page-tablesbits-p

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

Theorem: ia32e-page-tablesbits-p-compound-recognizer

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

Function: ia32e-page-tablesbits-fix

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

Theorem: ia32e-page-tablesbits-p-of-ia32e-page-tablesbits-fix

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

Theorem: ia32e-page-tablesbits-fix-when-ia32e-page-tablesbits-p

(defthm ia32e-page-tablesbits-fix-when-ia32e-page-tablesbits-p
  (implies (ia32e-page-tablesbits-p x)
           (equal (ia32e-page-tablesbits-fix x)
                  x)))

Function: ia32e-page-tablesbits-equiv$inline

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

Theorem: ia32e-page-tablesbits-equiv-is-an-equivalence

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

Theorem: ia32e-page-tablesbits-equiv-implies-equal-ia32e-page-tablesbits-fix-1

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

Theorem: ia32e-page-tablesbits-fix-under-ia32e-page-tablesbits-equiv

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

Function: ia32e-page-tablesbits

(defun ia32e-page-tablesbits
       (p r/w u/s pwt
          pcd a d ps res1 reference-addr res2 xd)
 (declare (xargs :guard (and (bitp p)
                             (bitp r/w)
                             (bitp u/s)
                             (bitp pwt)
                             (bitp pcd)
                             (bitp a)
                             (bitp d)
                             (bitp ps)
                             (4bits-p res1)
                             (40bits-p reference-addr)
                             (11bits-p res2)
                             (bitp xd))))
 (let ((__function__ 'ia32e-page-tablesbits))
  (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))
       (res1 (mbe :logic (4bits-fix res1)
                  :exec res1))
       (reference-addr (mbe :logic (40bits-fix reference-addr)
                            :exec reference-addr))
       (res2 (mbe :logic (11bits-fix res2)
                  :exec res2))
       (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 4 res1
                            (logapp 40 reference-addr
                                    (logapp 11 res2 xd))))))))))))))

Theorem: ia32e-page-tablesbits-p-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits-p-of-ia32e-page-tablesbits
 (b*
  ((ia32e-page-tablesbits
        (ia32e-page-tablesbits p r/w u/s pwt pcd
                               a d ps res1 reference-addr res2 xd)))
  (ia32e-page-tablesbits-p ia32e-page-tablesbits))
 :rule-classes :rewrite)

Theorem: ia32e-page-tablesbits-of-bfix-p

(defthm ia32e-page-tablesbits-of-bfix-p
 (equal
      (ia32e-page-tablesbits (bfix p)
                             r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-p

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-p
 (implies
  (bit-equiv p p-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p-equiv r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-r/w

(defthm ia32e-page-tablesbits-of-bfix-r/w
 (equal
      (ia32e-page-tablesbits p (bfix r/w)
                             u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-r/w

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-r/w
 (implies
  (bit-equiv r/w r/w-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w-equiv u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-u/s

(defthm ia32e-page-tablesbits-of-bfix-u/s
 (equal
      (ia32e-page-tablesbits p r/w (bfix u/s)
                             pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-u/s

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-u/s
 (implies
  (bit-equiv u/s u/s-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s-equiv pwt pcd
                             a d ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-pwt

(defthm ia32e-page-tablesbits-of-bfix-pwt
 (equal
      (ia32e-page-tablesbits p r/w u/s (bfix pwt)
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-pwt

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-pwt
 (implies
  (bit-equiv pwt pwt-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt-equiv pcd
                             a d ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-pcd

(defthm ia32e-page-tablesbits-of-bfix-pcd
 (equal (ia32e-page-tablesbits p r/w u/s pwt (bfix pcd)
                               a d ps res1 reference-addr res2 xd)
        (ia32e-page-tablesbits p r/w u/s pwt pcd
                               a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-pcd

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-pcd
 (implies
  (bit-equiv pcd pcd-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd-equiv
                             a d ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-a

(defthm ia32e-page-tablesbits-of-bfix-a
 (equal (ia32e-page-tablesbits p r/w u/s pwt pcd (bfix a)
                               d ps res1 reference-addr res2 xd)
        (ia32e-page-tablesbits p r/w u/s pwt pcd
                               a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-a

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-a
 (implies
  (bit-equiv a a-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a-equiv
                             d ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-d

(defthm ia32e-page-tablesbits-of-bfix-d
 (equal (ia32e-page-tablesbits p r/w u/s pwt pcd a (bfix d)
                               ps res1 reference-addr res2 xd)
        (ia32e-page-tablesbits p r/w u/s pwt pcd
                               a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-d

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-d
 (implies
  (bit-equiv d d-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a d-equiv
                             ps res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-ps

(defthm ia32e-page-tablesbits-of-bfix-ps
 (equal (ia32e-page-tablesbits p r/w u/s pwt pcd a d (bfix ps)
                               res1 reference-addr res2 xd)
        (ia32e-page-tablesbits p r/w u/s pwt pcd
                               a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-ps

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-ps
 (implies
  (bit-equiv ps ps-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a d
                             ps-equiv res1 reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-4bits-fix-res1

(defthm ia32e-page-tablesbits-of-4bits-fix-res1
 (equal
      (ia32e-page-tablesbits p
                             r/w u/s pwt pcd a d ps (4bits-fix res1)
                             reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-4bits-equiv-congruence-on-res1

(defthm ia32e-page-tablesbits-4bits-equiv-congruence-on-res1
 (implies
  (4bits-equiv res1 res1-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a d
                             ps res1-equiv reference-addr res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-40bits-fix-reference-addr

(defthm ia32e-page-tablesbits-of-40bits-fix-reference-addr
 (equal
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 (40bits-fix reference-addr)
                             res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd
                             a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-40bits-equiv-congruence-on-reference-addr

(defthm
    ia32e-page-tablesbits-40bits-equiv-congruence-on-reference-addr
 (implies
  (40bits-equiv reference-addr reference-addr-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a d
                             ps res1 reference-addr-equiv res2 xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-11bits-fix-res2

(defthm ia32e-page-tablesbits-of-11bits-fix-res2
 (equal
     (ia32e-page-tablesbits p r/w u/s pwt pcd a d
                            ps res1 reference-addr (11bits-fix res2)
                            xd)
     (ia32e-page-tablesbits p r/w u/s pwt pcd
                            a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-11bits-equiv-congruence-on-res2

(defthm ia32e-page-tablesbits-11bits-equiv-congruence-on-res2
 (implies
  (11bits-equiv res2 res2-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a d
                             ps res1 reference-addr res2-equiv xd)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits-of-bfix-xd

(defthm ia32e-page-tablesbits-of-bfix-xd
 (equal
     (ia32e-page-tablesbits p r/w u/s pwt pcd a
                            d ps res1 reference-addr res2 (bfix xd))
     (ia32e-page-tablesbits p r/w u/s pwt pcd
                            a d ps res1 reference-addr res2 xd)))

Theorem: ia32e-page-tablesbits-bit-equiv-congruence-on-xd

(defthm ia32e-page-tablesbits-bit-equiv-congruence-on-xd
 (implies
  (bit-equiv xd xd-equiv)
  (equal
      (ia32e-page-tablesbits p r/w u/s pwt
                             pcd a d ps res1 reference-addr res2 xd)
      (ia32e-page-tablesbits p r/w u/s pwt pcd a d
                             ps res1 reference-addr res2 xd-equiv)))
 :rule-classes :congruence)

Function: ia32e-page-tablesbits-equiv-under-mask

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

Function: ia32e-page-tablesbits->p$inline

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

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

Theorem: ia32e-page-tablesbits->p$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->p-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->p-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->p
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix p)))

Theorem: ia32e-page-tablesbits->p-of-write-with-mask

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

Function: ia32e-page-tablesbits->r/w$inline

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

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

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

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

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

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

Theorem: ia32e-page-tablesbits->r/w-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->r/w-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->r/w
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix r/w)))

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

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

Function: ia32e-page-tablesbits->u/s$inline

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

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

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

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

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

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

Theorem: ia32e-page-tablesbits->u/s-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->u/s-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->u/s
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix u/s)))

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

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

Function: ia32e-page-tablesbits->pwt$inline

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

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

Theorem: ia32e-page-tablesbits->pwt$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->pwt-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->pwt-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->pwt
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix pwt)))

Theorem: ia32e-page-tablesbits->pwt-of-write-with-mask

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

Function: ia32e-page-tablesbits->pcd$inline

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

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

Theorem: ia32e-page-tablesbits->pcd$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->pcd-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->pcd-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->pcd
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix pcd)))

Theorem: ia32e-page-tablesbits->pcd-of-write-with-mask

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

Function: ia32e-page-tablesbits->a$inline

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

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

Theorem: ia32e-page-tablesbits->a$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->a-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->a-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->a
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix a)))

Theorem: ia32e-page-tablesbits->a-of-write-with-mask

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

Function: ia32e-page-tablesbits->d$inline

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

(defthm bitp-of-ia32e-page-tablesbits->d
  (b* ((d (ia32e-page-tablesbits->d$inline x)))
    (bitp d))
  :rule-classes :rewrite)

Theorem: ia32e-page-tablesbits->d$inline-of-ia32e-page-tablesbits-fix-x

(defthm
     ia32e-page-tablesbits->d$inline-of-ia32e-page-tablesbits-fix-x
 (equal
     (ia32e-page-tablesbits->d$inline (ia32e-page-tablesbits-fix x))
     (ia32e-page-tablesbits->d$inline x)))

Theorem: ia32e-page-tablesbits->d$inline-ia32e-page-tablesbits-equiv-congruence-on-x

(defthm
 ia32e-page-tablesbits->d$inline-ia32e-page-tablesbits-equiv-congruence-on-x
 (implies (ia32e-page-tablesbits-equiv x x-equiv)
          (equal (ia32e-page-tablesbits->d$inline x)
                 (ia32e-page-tablesbits->d$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits->d-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->d-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->d
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix d)))

Theorem: ia32e-page-tablesbits->d-of-write-with-mask

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

Function: ia32e-page-tablesbits->ps$inline

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

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

Theorem: ia32e-page-tablesbits->ps$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->ps-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->ps-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->ps
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix ps)))

Theorem: ia32e-page-tablesbits->ps-of-write-with-mask

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

Function: ia32e-page-tablesbits->res1$inline

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

Theorem: 4bits-p-of-ia32e-page-tablesbits->res1

(defthm 4bits-p-of-ia32e-page-tablesbits->res1
  (b* ((res1 (ia32e-page-tablesbits->res1$inline x)))
    (4bits-p res1))
  :rule-classes :rewrite)

Theorem: ia32e-page-tablesbits->res1$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->res1-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->res1-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->res1
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (4bits-fix res1)))

Theorem: ia32e-page-tablesbits->res1-of-write-with-mask

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

Function: ia32e-page-tablesbits->reference-addr$inline

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

Theorem: 40bits-p-of-ia32e-page-tablesbits->reference-addr

(defthm 40bits-p-of-ia32e-page-tablesbits->reference-addr
  (b* ((reference-addr
            (ia32e-page-tablesbits->reference-addr$inline x)))
    (40bits-p reference-addr))
  :rule-classes :rewrite)

Theorem: ia32e-page-tablesbits->reference-addr$inline-of-ia32e-page-tablesbits-fix-x

(defthm
 ia32e-page-tablesbits->reference-addr$inline-of-ia32e-page-tablesbits-fix-x
 (equal (ia32e-page-tablesbits->reference-addr$inline
             (ia32e-page-tablesbits-fix x))
        (ia32e-page-tablesbits->reference-addr$inline x)))

Theorem: ia32e-page-tablesbits->reference-addr$inline-ia32e-page-tablesbits-equiv-congruence-on-x

(defthm
 ia32e-page-tablesbits->reference-addr$inline-ia32e-page-tablesbits-equiv-congruence-on-x
 (implies
     (ia32e-page-tablesbits-equiv x x-equiv)
     (equal (ia32e-page-tablesbits->reference-addr$inline x)
            (ia32e-page-tablesbits->reference-addr$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-page-tablesbits->reference-addr-of-ia32e-page-tablesbits

(defthm
     ia32e-page-tablesbits->reference-addr-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->reference-addr
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (40bits-fix reference-addr)))

Theorem: ia32e-page-tablesbits->reference-addr-of-write-with-mask

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

Function: ia32e-page-tablesbits->res2$inline

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

(defthm 11bits-p-of-ia32e-page-tablesbits->res2
  (b* ((res2 (ia32e-page-tablesbits->res2$inline x)))
    (11bits-p res2))
  :rule-classes :rewrite)

Theorem: ia32e-page-tablesbits->res2$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->res2-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->res2-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->res2
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (11bits-fix res2)))

Theorem: ia32e-page-tablesbits->res2-of-write-with-mask

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

Function: ia32e-page-tablesbits->xd$inline

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

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

Theorem: ia32e-page-tablesbits->xd$inline-of-ia32e-page-tablesbits-fix-x

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

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

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

Theorem: ia32e-page-tablesbits->xd-of-ia32e-page-tablesbits

(defthm ia32e-page-tablesbits->xd-of-ia32e-page-tablesbits
 (equal
  (ia32e-page-tablesbits->xd
     (ia32e-page-tablesbits p r/w u/s pwt
                            pcd a d ps res1 reference-addr res2 xd))
  (bfix xd)))

Theorem: ia32e-page-tablesbits->xd-of-write-with-mask

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

Theorem: ia32e-page-tablesbits-fix-in-terms-of-ia32e-page-tablesbits

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

Function: !ia32e-page-tablesbits->p$inline

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

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

Theorem: !ia32e-page-tablesbits->p$inline-of-bfix-p

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->p-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->p-of-!ia32e-page-tablesbits->p

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

Theorem: !ia32e-page-tablesbits->p-equiv-under-mask

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

Function: !ia32e-page-tablesbits->r/w$inline

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

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

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

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->r/w-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->r/w-of-!ia32e-page-tablesbits->r/w

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

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

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

Function: !ia32e-page-tablesbits->u/s$inline

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

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

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

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->u/s-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->u/s-of-!ia32e-page-tablesbits->u/s

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

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

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

Function: !ia32e-page-tablesbits->pwt$inline

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

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

Theorem: !ia32e-page-tablesbits->pwt$inline-of-bfix-pwt

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->pwt-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->pwt-of-!ia32e-page-tablesbits->pwt

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

Theorem: !ia32e-page-tablesbits->pwt-equiv-under-mask

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

Function: !ia32e-page-tablesbits->pcd$inline

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

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

Theorem: !ia32e-page-tablesbits->pcd$inline-of-bfix-pcd

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->pcd-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->pcd-of-!ia32e-page-tablesbits->pcd

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

Theorem: !ia32e-page-tablesbits->pcd-equiv-under-mask

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

Function: !ia32e-page-tablesbits->a$inline

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

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

Theorem: !ia32e-page-tablesbits->a$inline-of-bfix-a

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->a-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->a-of-!ia32e-page-tablesbits->a

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

Theorem: !ia32e-page-tablesbits->a-equiv-under-mask

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

Function: !ia32e-page-tablesbits->d$inline

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

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

Theorem: !ia32e-page-tablesbits->d$inline-of-bfix-d

(defthm !ia32e-page-tablesbits->d$inline-of-bfix-d
  (equal (!ia32e-page-tablesbits->d$inline (bfix d)
                                           x)
         (!ia32e-page-tablesbits->d$inline d x)))

Theorem: !ia32e-page-tablesbits->d$inline-bit-equiv-congruence-on-d

(defthm !ia32e-page-tablesbits->d$inline-bit-equiv-congruence-on-d
  (implies (bit-equiv d d-equiv)
           (equal (!ia32e-page-tablesbits->d$inline d x)
                  (!ia32e-page-tablesbits->d$inline d-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-page-tablesbits->d$inline-of-ia32e-page-tablesbits-fix-x

(defthm
    !ia32e-page-tablesbits->d$inline-of-ia32e-page-tablesbits-fix-x
 (equal
  (!ia32e-page-tablesbits->d$inline d (ia32e-page-tablesbits-fix x))
  (!ia32e-page-tablesbits->d$inline d x)))

Theorem: !ia32e-page-tablesbits->d$inline-ia32e-page-tablesbits-equiv-congruence-on-x

(defthm
 !ia32e-page-tablesbits->d$inline-ia32e-page-tablesbits-equiv-congruence-on-x
 (implies (ia32e-page-tablesbits-equiv x x-equiv)
          (equal (!ia32e-page-tablesbits->d$inline d x)
                 (!ia32e-page-tablesbits->d$inline d x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-page-tablesbits->d-is-ia32e-page-tablesbits

(defthm !ia32e-page-tablesbits->d-is-ia32e-page-tablesbits
  (equal (!ia32e-page-tablesbits->d d x)
         (change-ia32e-page-tablesbits x :d d)))

Theorem: ia32e-page-tablesbits->d-of-!ia32e-page-tablesbits->d

(defthm ia32e-page-tablesbits->d-of-!ia32e-page-tablesbits->d
  (b* ((?new-x (!ia32e-page-tablesbits->d$inline d x)))
    (equal (ia32e-page-tablesbits->d new-x)
           (bfix d))))

Theorem: !ia32e-page-tablesbits->d-equiv-under-mask

(defthm !ia32e-page-tablesbits->d-equiv-under-mask
  (b* ((?new-x (!ia32e-page-tablesbits->d$inline d x)))
    (ia32e-page-tablesbits-equiv-under-mask new-x x -65)))

Function: !ia32e-page-tablesbits->ps$inline

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

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

Theorem: !ia32e-page-tablesbits->ps$inline-of-bfix-ps

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->ps-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->ps-of-!ia32e-page-tablesbits->ps

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

Theorem: !ia32e-page-tablesbits->ps-equiv-under-mask

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

Function: !ia32e-page-tablesbits->res1$inline

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

Theorem: ia32e-page-tablesbits-p-of-!ia32e-page-tablesbits->res1

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

Theorem: !ia32e-page-tablesbits->res1$inline-of-4bits-fix-res1

(defthm !ia32e-page-tablesbits->res1$inline-of-4bits-fix-res1
  (equal (!ia32e-page-tablesbits->res1$inline (4bits-fix res1)
                                              x)
         (!ia32e-page-tablesbits->res1$inline res1 x)))

Theorem: !ia32e-page-tablesbits->res1$inline-4bits-equiv-congruence-on-res1

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->res1-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->res1-of-!ia32e-page-tablesbits->res1

(defthm ia32e-page-tablesbits->res1-of-!ia32e-page-tablesbits->res1
  (b* ((?new-x (!ia32e-page-tablesbits->res1$inline res1 x)))
    (equal (ia32e-page-tablesbits->res1 new-x)
           (4bits-fix res1))))

Theorem: !ia32e-page-tablesbits->res1-equiv-under-mask

(defthm !ia32e-page-tablesbits->res1-equiv-under-mask
  (b* ((?new-x (!ia32e-page-tablesbits->res1$inline res1 x)))
    (ia32e-page-tablesbits-equiv-under-mask new-x x -3841)))

Function: !ia32e-page-tablesbits->reference-addr$inline

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

Theorem: ia32e-page-tablesbits-p-of-!ia32e-page-tablesbits->reference-addr

(defthm
  ia32e-page-tablesbits-p-of-!ia32e-page-tablesbits->reference-addr
  (b* ((new-x (!ia32e-page-tablesbits->reference-addr$inline
                   reference-addr x)))
    (ia32e-page-tablesbits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-page-tablesbits->reference-addr$inline-of-40bits-fix-reference-addr

(defthm
 !ia32e-page-tablesbits->reference-addr$inline-of-40bits-fix-reference-addr
 (equal
  (!ia32e-page-tablesbits->reference-addr$inline
       (40bits-fix reference-addr)
       x)
  (!ia32e-page-tablesbits->reference-addr$inline reference-addr x)))

Theorem: !ia32e-page-tablesbits->reference-addr$inline-40bits-equiv-congruence-on-reference-addr

(defthm
 !ia32e-page-tablesbits->reference-addr$inline-40bits-equiv-congruence-on-reference-addr
 (implies
  (40bits-equiv reference-addr reference-addr-equiv)
  (equal
    (!ia32e-page-tablesbits->reference-addr$inline reference-addr x)
    (!ia32e-page-tablesbits->reference-addr$inline
         reference-addr-equiv x)))
 :rule-classes :congruence)

Theorem: !ia32e-page-tablesbits->reference-addr$inline-of-ia32e-page-tablesbits-fix-x

(defthm
 !ia32e-page-tablesbits->reference-addr$inline-of-ia32e-page-tablesbits-fix-x
 (equal
  (!ia32e-page-tablesbits->reference-addr$inline
       reference-addr
       (ia32e-page-tablesbits-fix x))
  (!ia32e-page-tablesbits->reference-addr$inline reference-addr x)))

Theorem: !ia32e-page-tablesbits->reference-addr$inline-ia32e-page-tablesbits-equiv-congruence-on-x

(defthm
 !ia32e-page-tablesbits->reference-addr$inline-ia32e-page-tablesbits-equiv-congruence-on-x
 (implies
  (ia32e-page-tablesbits-equiv x x-equiv)
  (equal
    (!ia32e-page-tablesbits->reference-addr$inline reference-addr x)
    (!ia32e-page-tablesbits->reference-addr$inline
         reference-addr x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-page-tablesbits->reference-addr-is-ia32e-page-tablesbits

(defthm
    !ia32e-page-tablesbits->reference-addr-is-ia32e-page-tablesbits
 (equal
     (!ia32e-page-tablesbits->reference-addr reference-addr x)
     (change-ia32e-page-tablesbits x
                                   :reference-addr reference-addr)))

Theorem: ia32e-page-tablesbits->reference-addr-of-!ia32e-page-tablesbits->reference-addr

(defthm
 ia32e-page-tablesbits->reference-addr-of-!ia32e-page-tablesbits->reference-addr
 (b* ((?new-x (!ia32e-page-tablesbits->reference-addr$inline
                   reference-addr x)))
   (equal (ia32e-page-tablesbits->reference-addr new-x)
          (40bits-fix reference-addr))))

Theorem: !ia32e-page-tablesbits->reference-addr-equiv-under-mask

(defthm !ia32e-page-tablesbits->reference-addr-equiv-under-mask
  (b* ((?new-x (!ia32e-page-tablesbits->reference-addr$inline
                    reference-addr x)))
    (ia32e-page-tablesbits-equiv-under-mask
         new-x x -4503599627366401)))

Function: !ia32e-page-tablesbits->res2$inline

(defun !ia32e-page-tablesbits->res2$inline (res2 x)
  (declare (xargs :guard (and (11bits-p res2)
                              (ia32e-page-tablesbits-p x))))
  (mbe :logic
       (b* ((res2 (mbe :logic (11bits-fix res2)
                       :exec res2))
            (x (ia32e-page-tablesbits-fix x)))
         (part-install res2 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) res2)
                                    52))))))

Theorem: ia32e-page-tablesbits-p-of-!ia32e-page-tablesbits->res2

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

Theorem: !ia32e-page-tablesbits->res2$inline-of-11bits-fix-res2

(defthm !ia32e-page-tablesbits->res2$inline-of-11bits-fix-res2
  (equal (!ia32e-page-tablesbits->res2$inline (11bits-fix res2)
                                              x)
         (!ia32e-page-tablesbits->res2$inline res2 x)))

Theorem: !ia32e-page-tablesbits->res2$inline-11bits-equiv-congruence-on-res2

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->res2-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->res2-of-!ia32e-page-tablesbits->res2

(defthm ia32e-page-tablesbits->res2-of-!ia32e-page-tablesbits->res2
  (b* ((?new-x (!ia32e-page-tablesbits->res2$inline res2 x)))
    (equal (ia32e-page-tablesbits->res2 new-x)
           (11bits-fix res2))))

Theorem: !ia32e-page-tablesbits->res2-equiv-under-mask

(defthm !ia32e-page-tablesbits->res2-equiv-under-mask
  (b* ((?new-x (!ia32e-page-tablesbits->res2$inline res2 x)))
    (ia32e-page-tablesbits-equiv-under-mask
         new-x x -9218868437227405313)))

Function: !ia32e-page-tablesbits->xd$inline

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

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

Theorem: !ia32e-page-tablesbits->xd$inline-of-bfix-xd

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

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

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

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

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

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

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

Theorem: !ia32e-page-tablesbits->xd-is-ia32e-page-tablesbits

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

Theorem: ia32e-page-tablesbits->xd-of-!ia32e-page-tablesbits->xd

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

Theorem: !ia32e-page-tablesbits->xd-equiv-under-mask

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

Function: ia32e-page-tablesbits-debug

(defun ia32e-page-tablesbits-debug (x)
 (declare (xargs :guard (ia32e-page-tablesbits-p x)))
 (let ((__function__ 'ia32e-page-tablesbits-debug))
  (declare (ignorable __function__))
  (b* (((ia32e-page-tablesbits 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 'res1 x.res1)
                (cons (cons 'reference-addr x.reference-addr)
                      (cons (cons 'res2 x.res2)
                            (cons (cons 'xd x.xd) nil)))))))))))))))

Subtopics

Ia32e-page-tablesbits-p: Recognizer for ia32e-page-tablesbits bit structures.
!ia32e-page-tablesbits->reference-addr: Update the |X86ISA|::|REFERENCE-ADDR| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->res2: Update the |X86ISA|::|RES2| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->res1: Update the |X86ISA|::|RES1| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->xd: Update the |X86ISA|::|XD| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->u/s: Update the |X86ISA|::|U/S| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->r/w: Update the |X86ISA|::|R/W| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->pwt: Update the |X86ISA|::|PWT| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->ps: Update the |X86ISA|::|PS| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->pcd: Update the |X86ISA|::|PCD| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->d: Update the |ACL2|::|D| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->a: Update the |ACL2|::|A| field of a ia32e-page-tablesbits bit structure.
!ia32e-page-tablesbits->p: Update the |ACL2|::|P| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->reference-addr: Access the |X86ISA|::|REFERENCE-ADDR| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits-fix: Fixing function for ia32e-page-tablesbits bit structures.
Ia32e-page-tablesbits->res2: Access the |X86ISA|::|RES2| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->res1: Access the |X86ISA|::|RES1| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->xd: Access the |X86ISA|::|XD| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->u/s: Access the |X86ISA|::|U/S| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->r/w: Access the |X86ISA|::|R/W| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->pwt: Access the |X86ISA|::|PWT| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->ps: Access the |X86ISA|::|PS| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->pcd: Access the |X86ISA|::|PCD| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->p: Access the |ACL2|::|P| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->d: Access the |ACL2|::|D| field of a ia32e-page-tablesbits bit structure.
Ia32e-page-tablesbits->a: Access the |ACL2|::|A| field of a ia32e-page-tablesbits bit structure.