• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
        • Structures
          • Rflagsbits
          • Cr4bits
          • Cr0bits
          • Xcr0bits
          • Prefixes
          • Ia32_eferbits
          • Evex-byte1
          • Cr3bits
          • Evex-byte3
          • Vex3-byte2
          • Vex3-byte1
          • Vex2-byte1
          • Evex-prefixes
          • Evex-byte2
          • Vex-prefixes
          • Sib
          • Modr/m-structures
          • Vex-prefixes-layout-structures
          • Sib-structures
          • Legacy-prefixes-layout-structure
          • Evex-prefixes-layout-structures
          • Cr8bits
          • Opcode-maps-structures
          • Segmentation-bitstructs
          • 8bits
          • 2bits
          • 4bits
          • 16bits
          • Paging-bitstructs
            • Ia32e-pdpte-1gb-pagebits
            • Ia32e-pde-2mb-pagebits
            • Ia32e-pte-4k-pagebits
            • Ia32e-pml4ebits
            • Ia32e-pdpte-pg-dirbits
            • Ia32e-pde-pg-tablebits
              • Ia32e-pde-pg-tablebits-p
              • !ia32e-pde-pg-tablebits->res3
              • !ia32e-pde-pg-tablebits->res2
              • !ia32e-pde-pg-tablebits->res1
              • !ia32e-pde-pg-tablebits->xd
              • !ia32e-pde-pg-tablebits->u/s
              • !ia32e-pde-pg-tablebits->r/w
              • !ia32e-pde-pg-tablebits->pwt
              • !ia32e-pde-pg-tablebits->pt
              • !ia32e-pde-pg-tablebits->pcd
              • !ia32e-pde-pg-tablebits->ps
              • !ia32e-pde-pg-tablebits->p
              • !ia32e-pde-pg-tablebits->a
              • Ia32e-pde-pg-tablebits-fix
              • Ia32e-pde-pg-tablebits->res3
              • Ia32e-pde-pg-tablebits->xd
              • Ia32e-pde-pg-tablebits->res2
              • Ia32e-pde-pg-tablebits->res1
              • Ia32e-pde-pg-tablebits->pt
              • Ia32e-pde-pg-tablebits->u/s
              • Ia32e-pde-pg-tablebits->r/w
              • Ia32e-pde-pg-tablebits->pwt
              • Ia32e-pde-pg-tablebits->ps
              • Ia32e-pde-pg-tablebits->pcd
              • Ia32e-pde-pg-tablebits->a
              • Ia32e-pde-pg-tablebits->p
            • Ia32e-page-tablesbits
            • Ia32e-pdpte-1gb-pagebits-equiv-under-mask
            • Ia32e-pdpte-1gb-pagebits-debug
            • Ia32e-pte-4k-pagebits-equiv-under-mask
            • Ia32e-pte-4k-pagebits-debug
            • Ia32e-pml4ebits-equiv-under-mask
            • Ia32e-pdpte-pg-dirbits-equiv-under-mask
            • Ia32e-pde-pg-tablebits-equiv-under-mask
            • Ia32e-pde-2mb-pagebits-equiv-under-mask
            • Ia32e-pde-2mb-pagebits-debug
            • Ia32e-page-tablesbits-equiv-under-mask
            • Ia32e-pml4ebits-debug
            • Ia32e-pdpte-pg-dirbits-debug
            • Ia32e-pde-pg-tablebits-debug
            • Ia32e-page-tablesbits-debug
          • 3bits
          • 11bits
          • 40bits
          • 5bits
          • 32bits
          • 19bits
          • 10bits
          • 64bits
          • 7bits
          • 54bits
          • 31bits
          • 24bits
          • 22bits
          • 17bits
          • 13bits
          • 12bits
          • 6bits
          • Vex-prefixes-map-p
          • Vex-prefixes-byte0-p
          • Vex->w
          • Vex->vvvv
          • Fp-bitstructs
          • Vex->pp
          • Vex->l
          • Rflagsbits-debug
          • Evex->v-prime
          • Cr4bits-debug
          • Evex->z
          • Evex->w
          • Evex->vvvv
          • Evex->vl/rc
          • Evex->pp
          • Evex->aaa
          • Vex3-byte1-equiv-under-mask
          • Xcr0bits-debug
          • Vex3-byte2-equiv-under-mask
          • Vex2-byte1-equiv-under-mask
          • Vex-prefixes-equiv-under-mask
          • Rflagsbits-equiv-under-mask
          • Ia32_eferbits-equiv-under-mask
          • Evex-prefixes-equiv-under-mask
          • Evex-byte3-equiv-under-mask
          • Evex-byte2-equiv-under-mask
          • Evex-byte1-equiv-under-mask
          • Cr0bits-debug
          • Xcr0bits-equiv-under-mask
          • Sib-equiv-under-mask
          • Prefixes-equiv-under-mask
          • Cr8bits-equiv-under-mask
          • Cr4bits-equiv-under-mask
          • Cr3bits-equiv-under-mask
          • Cr0bits-equiv-under-mask
          • Vex3-byte1-debug
          • Prefixes-debug
          • Ia32_eferbits-debug
          • Evex-byte1-debug
          • Vex3-byte2-debug
          • Vex2-byte1-debug
          • Vex-prefixes-debug
          • Evex-prefixes-debug
          • Evex-byte3-debug
          • Evex-byte2-debug
          • Cr3bits-debug
          • Sib-debug
          • Cr8bits-debug
        • Utilities
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Testing-utilities
  • Math

• Paging-bitstructs

Ia32e-pde-pg-tablebits

An 64-bit unsigned bitstruct type.

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

Fields

p — bit

r/w — bit

u/s — bit

pwt — bit

pcd — bit

a — bit

res1 — bit

ps — bit

res2 — 4bits

pt — 40bits

res3 — 11bits

xd — bit

Definitions and Theorems

Function: ia32e-pde-pg-tablebits-p

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

Theorem: ia32e-pde-pg-tablebits-p-when-unsigned-byte-p

(defthm ia32e-pde-pg-tablebits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (ia32e-pde-pg-tablebits-p x)))

Theorem: unsigned-byte-p-when-ia32e-pde-pg-tablebits-p

(defthm unsigned-byte-p-when-ia32e-pde-pg-tablebits-p
  (implies (ia32e-pde-pg-tablebits-p x)
           (unsigned-byte-p 64 x)))

Theorem: ia32e-pde-pg-tablebits-p-compound-recognizer

(defthm ia32e-pde-pg-tablebits-p-compound-recognizer
  (implies (ia32e-pde-pg-tablebits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: ia32e-pde-pg-tablebits-fix

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

Theorem: ia32e-pde-pg-tablebits-p-of-ia32e-pde-pg-tablebits-fix

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

Theorem: ia32e-pde-pg-tablebits-fix-when-ia32e-pde-pg-tablebits-p

(defthm ia32e-pde-pg-tablebits-fix-when-ia32e-pde-pg-tablebits-p
  (implies (ia32e-pde-pg-tablebits-p x)
           (equal (ia32e-pde-pg-tablebits-fix x)
                  x)))

Function: ia32e-pde-pg-tablebits-equiv$inline

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

Theorem: ia32e-pde-pg-tablebits-equiv-is-an-equivalence

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

Theorem: ia32e-pde-pg-tablebits-equiv-implies-equal-ia32e-pde-pg-tablebits-fix-1

(defthm
 ia32e-pde-pg-tablebits-equiv-implies-equal-ia32e-pde-pg-tablebits-fix-1
 (implies (ia32e-pde-pg-tablebits-equiv x x-equiv)
          (equal (ia32e-pde-pg-tablebits-fix x)
                 (ia32e-pde-pg-tablebits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: ia32e-pde-pg-tablebits-fix-under-ia32e-pde-pg-tablebits-equiv

(defthm
      ia32e-pde-pg-tablebits-fix-under-ia32e-pde-pg-tablebits-equiv
  (ia32e-pde-pg-tablebits-equiv (ia32e-pde-pg-tablebits-fix x)
                                x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: ia32e-pde-pg-tablebits

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

Theorem: ia32e-pde-pg-tablebits-p-of-ia32e-pde-pg-tablebits

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-p

(defthm ia32e-pde-pg-tablebits-of-bfix-p
 (equal
    (ia32e-pde-pg-tablebits (bfix p)
                            r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-p

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-r/w

(defthm ia32e-pde-pg-tablebits-of-bfix-r/w
 (equal
    (ia32e-pde-pg-tablebits p (bfix r/w)
                            u/s pwt pcd a res1 ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-r/w

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-u/s

(defthm ia32e-pde-pg-tablebits-of-bfix-u/s
 (equal
    (ia32e-pde-pg-tablebits p r/w (bfix u/s)
                            pwt pcd a res1 ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-u/s

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-pwt

(defthm ia32e-pde-pg-tablebits-of-bfix-pwt
 (equal
    (ia32e-pde-pg-tablebits p r/w u/s (bfix pwt)
                            pcd a res1 ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-pwt

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-pcd

(defthm ia32e-pde-pg-tablebits-of-bfix-pcd
 (equal
    (ia32e-pde-pg-tablebits p r/w u/s pwt (bfix pcd)
                            a res1 ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-pcd

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-a

(defthm ia32e-pde-pg-tablebits-of-bfix-a
 (equal
    (ia32e-pde-pg-tablebits p r/w u/s pwt pcd (bfix a)
                            res1 ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-a

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-res1

(defthm ia32e-pde-pg-tablebits-of-bfix-res1
 (equal
    (ia32e-pde-pg-tablebits p r/w u/s pwt pcd a (bfix res1)
                            ps res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-res1

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-ps

(defthm ia32e-pde-pg-tablebits-of-bfix-ps
 (equal
    (ia32e-pde-pg-tablebits p r/w u/s pwt pcd a res1 (bfix ps)
                            res2 pt res3 xd)
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-ps

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

Theorem: ia32e-pde-pg-tablebits-of-4bits-fix-res2

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

Theorem: ia32e-pde-pg-tablebits-4bits-equiv-congruence-on-res2

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

Theorem: ia32e-pde-pg-tablebits-of-40bits-fix-pt

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

Theorem: ia32e-pde-pg-tablebits-40bits-equiv-congruence-on-pt

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

Theorem: ia32e-pde-pg-tablebits-of-11bits-fix-res3

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

Theorem: ia32e-pde-pg-tablebits-11bits-equiv-congruence-on-res3

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

Theorem: ia32e-pde-pg-tablebits-of-bfix-xd

(defthm ia32e-pde-pg-tablebits-of-bfix-xd
 (equal
    (ia32e-pde-pg-tablebits p r/w u/s pwt
                            pcd a res1 ps res2 pt res3 (bfix xd))
    (ia32e-pde-pg-tablebits p r/w
                            u/s pwt pcd a res1 ps res2 pt res3 xd)))

Theorem: ia32e-pde-pg-tablebits-bit-equiv-congruence-on-xd

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

Function: ia32e-pde-pg-tablebits-equiv-under-mask

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

Function: ia32e-pde-pg-tablebits->p$inline

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

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

Theorem: ia32e-pde-pg-tablebits->p$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
   ia32e-pde-pg-tablebits->p$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal
   (ia32e-pde-pg-tablebits->p$inline (ia32e-pde-pg-tablebits-fix x))
   (ia32e-pde-pg-tablebits->p$inline x)))

Theorem: ia32e-pde-pg-tablebits->p$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->p-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->p-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->p
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix p)))

Theorem: ia32e-pde-pg-tablebits->p-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->r/w$inline

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

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

Theorem: ia32e-pde-pg-tablebits->r/w$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->r/w$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->r/w$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->r/w$inline x)))

Theorem: ia32e-pde-pg-tablebits->r/w$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->r/w-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->r/w-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->r/w
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix r/w)))

Theorem: ia32e-pde-pg-tablebits->r/w-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->u/s$inline

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

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

Theorem: ia32e-pde-pg-tablebits->u/s$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->u/s$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->u/s$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->u/s$inline x)))

Theorem: ia32e-pde-pg-tablebits->u/s$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->u/s-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->u/s-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->u/s
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix u/s)))

Theorem: ia32e-pde-pg-tablebits->u/s-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->pwt$inline

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

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

Theorem: ia32e-pde-pg-tablebits->pwt$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->pwt$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->pwt$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->pwt$inline x)))

Theorem: ia32e-pde-pg-tablebits->pwt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->pwt-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->pwt-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->pwt
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix pwt)))

Theorem: ia32e-pde-pg-tablebits->pwt-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->pcd$inline

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

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

Theorem: ia32e-pde-pg-tablebits->pcd$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->pcd$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->pcd$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->pcd$inline x)))

Theorem: ia32e-pde-pg-tablebits->pcd$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->pcd-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->pcd-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->pcd
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix pcd)))

Theorem: ia32e-pde-pg-tablebits->pcd-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->a$inline

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

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

Theorem: ia32e-pde-pg-tablebits->a$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
   ia32e-pde-pg-tablebits->a$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal
   (ia32e-pde-pg-tablebits->a$inline (ia32e-pde-pg-tablebits-fix x))
   (ia32e-pde-pg-tablebits->a$inline x)))

Theorem: ia32e-pde-pg-tablebits->a$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->a-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->a-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->a
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix a)))

Theorem: ia32e-pde-pg-tablebits->a-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->res1$inline

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

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

Theorem: ia32e-pde-pg-tablebits->res1$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->res1$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->res1$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->res1$inline x)))

Theorem: ia32e-pde-pg-tablebits->res1$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->res1-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->res1-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->res1
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix res1)))

Theorem: ia32e-pde-pg-tablebits->res1-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->ps$inline

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

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

Theorem: ia32e-pde-pg-tablebits->ps$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
  ia32e-pde-pg-tablebits->ps$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal
  (ia32e-pde-pg-tablebits->ps$inline (ia32e-pde-pg-tablebits-fix x))
  (ia32e-pde-pg-tablebits->ps$inline x)))

Theorem: ia32e-pde-pg-tablebits->ps$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->ps-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->ps-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->ps
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix ps)))

Theorem: ia32e-pde-pg-tablebits->ps-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->res2$inline

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

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

Theorem: ia32e-pde-pg-tablebits->res2$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->res2$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->res2$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->res2$inline x)))

Theorem: ia32e-pde-pg-tablebits->res2$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->res2-of-ia32e-pde-pg-tablebits

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

Theorem: ia32e-pde-pg-tablebits->res2-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->pt$inline

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

(defthm 40bits-p-of-ia32e-pde-pg-tablebits->pt
  (b* ((pt (ia32e-pde-pg-tablebits->pt$inline x)))
    (40bits-p pt))
  :rule-classes :rewrite)

Theorem: ia32e-pde-pg-tablebits->pt$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
  ia32e-pde-pg-tablebits->pt$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal
  (ia32e-pde-pg-tablebits->pt$inline (ia32e-pde-pg-tablebits-fix x))
  (ia32e-pde-pg-tablebits->pt$inline x)))

Theorem: ia32e-pde-pg-tablebits->pt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

(defthm
 ia32e-pde-pg-tablebits->pt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x
 (implies (ia32e-pde-pg-tablebits-equiv x x-equiv)
          (equal (ia32e-pde-pg-tablebits->pt$inline x)
                 (ia32e-pde-pg-tablebits->pt$inline x-equiv)))
 :rule-classes :congruence)

Theorem: ia32e-pde-pg-tablebits->pt-of-ia32e-pde-pg-tablebits

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

Theorem: ia32e-pde-pg-tablebits->pt-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->res3$inline

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

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

Theorem: ia32e-pde-pg-tablebits->res3$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 ia32e-pde-pg-tablebits->res3$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (ia32e-pde-pg-tablebits->res3$inline
             (ia32e-pde-pg-tablebits-fix x))
        (ia32e-pde-pg-tablebits->res3$inline x)))

Theorem: ia32e-pde-pg-tablebits->res3$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->res3-of-ia32e-pde-pg-tablebits

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

Theorem: ia32e-pde-pg-tablebits->res3-of-write-with-mask

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

Function: ia32e-pde-pg-tablebits->xd$inline

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

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

Theorem: ia32e-pde-pg-tablebits->xd$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
  ia32e-pde-pg-tablebits->xd$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal
  (ia32e-pde-pg-tablebits->xd$inline (ia32e-pde-pg-tablebits-fix x))
  (ia32e-pde-pg-tablebits->xd$inline x)))

Theorem: ia32e-pde-pg-tablebits->xd$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: ia32e-pde-pg-tablebits->xd-of-ia32e-pde-pg-tablebits

(defthm ia32e-pde-pg-tablebits->xd-of-ia32e-pde-pg-tablebits
 (equal
  (ia32e-pde-pg-tablebits->xd
     (ia32e-pde-pg-tablebits p r/w
                             u/s pwt pcd a res1 ps res2 pt res3 xd))
  (bfix xd)))

Theorem: ia32e-pde-pg-tablebits->xd-of-write-with-mask

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

Theorem: ia32e-pde-pg-tablebits-fix-in-terms-of-ia32e-pde-pg-tablebits

(defthm
      ia32e-pde-pg-tablebits-fix-in-terms-of-ia32e-pde-pg-tablebits
  (equal (ia32e-pde-pg-tablebits-fix x)
         (change-ia32e-pde-pg-tablebits x)))

Function: !ia32e-pde-pg-tablebits->p$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->p$inline-of-bfix-p

(defthm !ia32e-pde-pg-tablebits->p$inline-of-bfix-p
  (equal (!ia32e-pde-pg-tablebits->p$inline (bfix p)
                                            x)
         (!ia32e-pde-pg-tablebits->p$inline p x)))

Theorem: !ia32e-pde-pg-tablebits->p$inline-bit-equiv-congruence-on-p

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

Theorem: !ia32e-pde-pg-tablebits->p$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
  !ia32e-pde-pg-tablebits->p$inline-of-ia32e-pde-pg-tablebits-fix-x
  (equal (!ia32e-pde-pg-tablebits->p$inline
              p (ia32e-pde-pg-tablebits-fix x))
         (!ia32e-pde-pg-tablebits->p$inline p x)))

Theorem: !ia32e-pde-pg-tablebits->p$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->p-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->p-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->p p x)
         (change-ia32e-pde-pg-tablebits x :p p)))

Theorem: ia32e-pde-pg-tablebits->p-of-!ia32e-pde-pg-tablebits->p

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

Theorem: !ia32e-pde-pg-tablebits->p-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->r/w$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->r/w$inline-of-bfix-r/w

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

Theorem: !ia32e-pde-pg-tablebits->r/w$inline-bit-equiv-congruence-on-r/w

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

Theorem: !ia32e-pde-pg-tablebits->r/w$inline-of-ia32e-pde-pg-tablebits-fix-x

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

Theorem: !ia32e-pde-pg-tablebits->r/w$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->r/w-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->r/w-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->r/w r/w x)
         (change-ia32e-pde-pg-tablebits x
                                        :r/w r/w)))

Theorem: ia32e-pde-pg-tablebits->r/w-of-!ia32e-pde-pg-tablebits->r/w

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

Theorem: !ia32e-pde-pg-tablebits->r/w-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->u/s$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->u/s$inline-of-bfix-u/s

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

Theorem: !ia32e-pde-pg-tablebits->u/s$inline-bit-equiv-congruence-on-u/s

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

Theorem: !ia32e-pde-pg-tablebits->u/s$inline-of-ia32e-pde-pg-tablebits-fix-x

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

Theorem: !ia32e-pde-pg-tablebits->u/s$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->u/s-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->u/s-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->u/s u/s x)
         (change-ia32e-pde-pg-tablebits x
                                        :u/s u/s)))

Theorem: ia32e-pde-pg-tablebits->u/s-of-!ia32e-pde-pg-tablebits->u/s

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

Theorem: !ia32e-pde-pg-tablebits->u/s-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->pwt$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->pwt$inline-of-bfix-pwt

(defthm !ia32e-pde-pg-tablebits->pwt$inline-of-bfix-pwt
  (equal (!ia32e-pde-pg-tablebits->pwt$inline (bfix pwt)
                                              x)
         (!ia32e-pde-pg-tablebits->pwt$inline pwt x)))

Theorem: !ia32e-pde-pg-tablebits->pwt$inline-bit-equiv-congruence-on-pwt

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

Theorem: !ia32e-pde-pg-tablebits->pwt$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->pwt$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->pwt$inline
             pwt (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->pwt$inline pwt x)))

Theorem: !ia32e-pde-pg-tablebits->pwt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->pwt-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->pwt-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->pwt pwt x)
         (change-ia32e-pde-pg-tablebits x
                                        :pwt pwt)))

Theorem: ia32e-pde-pg-tablebits->pwt-of-!ia32e-pde-pg-tablebits->pwt

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

Theorem: !ia32e-pde-pg-tablebits->pwt-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->pcd$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->pcd$inline-of-bfix-pcd

(defthm !ia32e-pde-pg-tablebits->pcd$inline-of-bfix-pcd
  (equal (!ia32e-pde-pg-tablebits->pcd$inline (bfix pcd)
                                              x)
         (!ia32e-pde-pg-tablebits->pcd$inline pcd x)))

Theorem: !ia32e-pde-pg-tablebits->pcd$inline-bit-equiv-congruence-on-pcd

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

Theorem: !ia32e-pde-pg-tablebits->pcd$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->pcd$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->pcd$inline
             pcd (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->pcd$inline pcd x)))

Theorem: !ia32e-pde-pg-tablebits->pcd$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->pcd-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->pcd-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->pcd pcd x)
         (change-ia32e-pde-pg-tablebits x
                                        :pcd pcd)))

Theorem: ia32e-pde-pg-tablebits->pcd-of-!ia32e-pde-pg-tablebits->pcd

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

Theorem: !ia32e-pde-pg-tablebits->pcd-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->a$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->a$inline-of-bfix-a

(defthm !ia32e-pde-pg-tablebits->a$inline-of-bfix-a
  (equal (!ia32e-pde-pg-tablebits->a$inline (bfix a)
                                            x)
         (!ia32e-pde-pg-tablebits->a$inline a x)))

Theorem: !ia32e-pde-pg-tablebits->a$inline-bit-equiv-congruence-on-a

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

Theorem: !ia32e-pde-pg-tablebits->a$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
  !ia32e-pde-pg-tablebits->a$inline-of-ia32e-pde-pg-tablebits-fix-x
  (equal (!ia32e-pde-pg-tablebits->a$inline
              a (ia32e-pde-pg-tablebits-fix x))
         (!ia32e-pde-pg-tablebits->a$inline a x)))

Theorem: !ia32e-pde-pg-tablebits->a$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->a-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->a-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->a a x)
         (change-ia32e-pde-pg-tablebits x :a a)))

Theorem: ia32e-pde-pg-tablebits->a-of-!ia32e-pde-pg-tablebits->a

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

Theorem: !ia32e-pde-pg-tablebits->a-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->res1$inline

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

Theorem: ia32e-pde-pg-tablebits-p-of-!ia32e-pde-pg-tablebits->res1

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

Theorem: !ia32e-pde-pg-tablebits->res1$inline-of-bfix-res1

(defthm !ia32e-pde-pg-tablebits->res1$inline-of-bfix-res1
  (equal (!ia32e-pde-pg-tablebits->res1$inline (bfix res1)
                                               x)
         (!ia32e-pde-pg-tablebits->res1$inline res1 x)))

Theorem: !ia32e-pde-pg-tablebits->res1$inline-bit-equiv-congruence-on-res1

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

Theorem: !ia32e-pde-pg-tablebits->res1$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->res1$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->res1$inline
             res1 (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->res1$inline res1 x)))

Theorem: !ia32e-pde-pg-tablebits->res1$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->res1-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->res1-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->res1 res1 x)
         (change-ia32e-pde-pg-tablebits x
                                        :res1 res1)))

Theorem: ia32e-pde-pg-tablebits->res1-of-!ia32e-pde-pg-tablebits->res1

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

Theorem: !ia32e-pde-pg-tablebits->res1-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->ps$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->ps$inline-of-bfix-ps

(defthm !ia32e-pde-pg-tablebits->ps$inline-of-bfix-ps
  (equal (!ia32e-pde-pg-tablebits->ps$inline (bfix ps)
                                             x)
         (!ia32e-pde-pg-tablebits->ps$inline ps x)))

Theorem: !ia32e-pde-pg-tablebits->ps$inline-bit-equiv-congruence-on-ps

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

Theorem: !ia32e-pde-pg-tablebits->ps$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->ps$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->ps$inline
             ps (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->ps$inline ps x)))

Theorem: !ia32e-pde-pg-tablebits->ps$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->ps-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->ps-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->ps ps x)
         (change-ia32e-pde-pg-tablebits x
                                        :ps ps)))

Theorem: ia32e-pde-pg-tablebits->ps-of-!ia32e-pde-pg-tablebits->ps

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

Theorem: !ia32e-pde-pg-tablebits->ps-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->res2$inline

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

Theorem: ia32e-pde-pg-tablebits-p-of-!ia32e-pde-pg-tablebits->res2

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

Theorem: !ia32e-pde-pg-tablebits->res2$inline-of-4bits-fix-res2

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

Theorem: !ia32e-pde-pg-tablebits->res2$inline-4bits-equiv-congruence-on-res2

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

Theorem: !ia32e-pde-pg-tablebits->res2$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->res2$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->res2$inline
             res2 (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->res2$inline res2 x)))

Theorem: !ia32e-pde-pg-tablebits->res2$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->res2-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->res2-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->res2 res2 x)
         (change-ia32e-pde-pg-tablebits x
                                        :res2 res2)))

Theorem: ia32e-pde-pg-tablebits->res2-of-!ia32e-pde-pg-tablebits->res2

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

Theorem: !ia32e-pde-pg-tablebits->res2-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->pt$inline

(defun !ia32e-pde-pg-tablebits->pt$inline (pt x)
  (declare (xargs :guard (and (40bits-p pt)
                              (ia32e-pde-pg-tablebits-p x))))
  (mbe :logic
       (b* ((pt (mbe :logic (40bits-fix pt) :exec pt))
            (x (ia32e-pde-pg-tablebits-fix x)))
         (part-install pt 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) pt)
                                    12))))))

Theorem: ia32e-pde-pg-tablebits-p-of-!ia32e-pde-pg-tablebits->pt

(defthm ia32e-pde-pg-tablebits-p-of-!ia32e-pde-pg-tablebits->pt
  (b* ((new-x (!ia32e-pde-pg-tablebits->pt$inline pt x)))
    (ia32e-pde-pg-tablebits-p new-x))
  :rule-classes :rewrite)

Theorem: !ia32e-pde-pg-tablebits->pt$inline-of-40bits-fix-pt

(defthm !ia32e-pde-pg-tablebits->pt$inline-of-40bits-fix-pt
  (equal (!ia32e-pde-pg-tablebits->pt$inline (40bits-fix pt)
                                             x)
         (!ia32e-pde-pg-tablebits->pt$inline pt x)))

Theorem: !ia32e-pde-pg-tablebits->pt$inline-40bits-equiv-congruence-on-pt

(defthm
   !ia32e-pde-pg-tablebits->pt$inline-40bits-equiv-congruence-on-pt
  (implies (40bits-equiv pt pt-equiv)
           (equal (!ia32e-pde-pg-tablebits->pt$inline pt x)
                  (!ia32e-pde-pg-tablebits->pt$inline pt-equiv x)))
  :rule-classes :congruence)

Theorem: !ia32e-pde-pg-tablebits->pt$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->pt$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->pt$inline
             pt (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->pt$inline pt x)))

Theorem: !ia32e-pde-pg-tablebits->pt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

(defthm
 !ia32e-pde-pg-tablebits->pt$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x
 (implies (ia32e-pde-pg-tablebits-equiv x x-equiv)
          (equal (!ia32e-pde-pg-tablebits->pt$inline pt x)
                 (!ia32e-pde-pg-tablebits->pt$inline pt x-equiv)))
 :rule-classes :congruence)

Theorem: !ia32e-pde-pg-tablebits->pt-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->pt-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->pt pt x)
         (change-ia32e-pde-pg-tablebits x
                                        :pt pt)))

Theorem: ia32e-pde-pg-tablebits->pt-of-!ia32e-pde-pg-tablebits->pt

(defthm ia32e-pde-pg-tablebits->pt-of-!ia32e-pde-pg-tablebits->pt
  (b* ((?new-x (!ia32e-pde-pg-tablebits->pt$inline pt x)))
    (equal (ia32e-pde-pg-tablebits->pt new-x)
           (40bits-fix pt))))

Theorem: !ia32e-pde-pg-tablebits->pt-equiv-under-mask

(defthm !ia32e-pde-pg-tablebits->pt-equiv-under-mask
  (b* ((?new-x (!ia32e-pde-pg-tablebits->pt$inline pt x)))
    (ia32e-pde-pg-tablebits-equiv-under-mask
         new-x x -4503599627366401)))

Function: !ia32e-pde-pg-tablebits->res3$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->res3$inline-of-11bits-fix-res3

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

Theorem: !ia32e-pde-pg-tablebits->res3$inline-11bits-equiv-congruence-on-res3

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

Theorem: !ia32e-pde-pg-tablebits->res3$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->res3$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->res3$inline
             res3 (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->res3$inline res3 x)))

Theorem: !ia32e-pde-pg-tablebits->res3$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->res3-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->res3-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->res3 res3 x)
         (change-ia32e-pde-pg-tablebits x
                                        :res3 res3)))

Theorem: ia32e-pde-pg-tablebits->res3-of-!ia32e-pde-pg-tablebits->res3

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

Theorem: !ia32e-pde-pg-tablebits->res3-equiv-under-mask

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

Function: !ia32e-pde-pg-tablebits->xd$inline

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

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

Theorem: !ia32e-pde-pg-tablebits->xd$inline-of-bfix-xd

(defthm !ia32e-pde-pg-tablebits->xd$inline-of-bfix-xd
  (equal (!ia32e-pde-pg-tablebits->xd$inline (bfix xd)
                                             x)
         (!ia32e-pde-pg-tablebits->xd$inline xd x)))

Theorem: !ia32e-pde-pg-tablebits->xd$inline-bit-equiv-congruence-on-xd

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

Theorem: !ia32e-pde-pg-tablebits->xd$inline-of-ia32e-pde-pg-tablebits-fix-x

(defthm
 !ia32e-pde-pg-tablebits->xd$inline-of-ia32e-pde-pg-tablebits-fix-x
 (equal (!ia32e-pde-pg-tablebits->xd$inline
             xd (ia32e-pde-pg-tablebits-fix x))
        (!ia32e-pde-pg-tablebits->xd$inline xd x)))

Theorem: !ia32e-pde-pg-tablebits->xd$inline-ia32e-pde-pg-tablebits-equiv-congruence-on-x

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

Theorem: !ia32e-pde-pg-tablebits->xd-is-ia32e-pde-pg-tablebits

(defthm !ia32e-pde-pg-tablebits->xd-is-ia32e-pde-pg-tablebits
  (equal (!ia32e-pde-pg-tablebits->xd xd x)
         (change-ia32e-pde-pg-tablebits x
                                        :xd xd)))

Theorem: ia32e-pde-pg-tablebits->xd-of-!ia32e-pde-pg-tablebits->xd

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

Theorem: !ia32e-pde-pg-tablebits->xd-equiv-under-mask

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

Function: ia32e-pde-pg-tablebits-debug

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

Subtopics

Ia32e-pde-pg-tablebits-p

Recognizer for ia32e-pde-pg-tablebits bit structures.

!ia32e-pde-pg-tablebits->res3

Update the |X86ISA|::|RES3| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->res2

Update the |X86ISA|::|RES2| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->res1

Update the |X86ISA|::|RES1| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->xd

Update the |X86ISA|::|XD| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->u/s

Update the |X86ISA|::|U/S| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->r/w

Update the |X86ISA|::|R/W| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->pwt

Update the |X86ISA|::|PWT| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->pt

Update the |X86ISA|::|PT| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->pcd

Update the |X86ISA|::|PCD| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->ps

Update the |X86ISA|::|PS| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->p

Update the |ACL2|::|P| field of a ia32e-pde-pg-tablebits bit structure.

!ia32e-pde-pg-tablebits->a

Update the |ACL2|::|A| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits-fix

Fixing function for ia32e-pde-pg-tablebits bit structures.

Ia32e-pde-pg-tablebits->res3

Access the |X86ISA|::|RES3| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->xd

Access the |X86ISA|::|XD| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->res2

Access the |X86ISA|::|RES2| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->res1

Access the |X86ISA|::|RES1| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->pt

Access the |X86ISA|::|PT| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->u/s

Access the |X86ISA|::|U/S| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->r/w

Access the |X86ISA|::|R/W| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->pwt

Access the |X86ISA|::|PWT| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->ps

Access the |X86ISA|::|PS| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->pcd

Access the |X86ISA|::|PCD| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->a

Access the |ACL2|::|A| field of a ia32e-pde-pg-tablebits bit structure.

Ia32e-pde-pg-tablebits->p

Access the |ACL2|::|P| field of a ia32e-pde-pg-tablebits bit structure.