		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Code-segment-descriptorbits

AMD manual, Jun'23, Vol. 2, Figures 4-20 and 4-14.

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

Fields

limit15-0 — 16bits
base15-0 — 16bits
base23-16 — 8bits
a — bit
r — bit
c — bit
msb-of-type — bit
s — bit
dpl — 2bits
p — bit
limit19-16 — 4bits
avl — bit
l — bit
d — bit
g — bit
base31-24 — 8bits

Definitions and Theorems

Function: code-segment-descriptorbits-p

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

Theorem: code-segment-descriptorbits-p-when-unsigned-byte-p

(defthm code-segment-descriptorbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 64 x)
           (code-segment-descriptorbits-p x)))

Theorem: unsigned-byte-p-when-code-segment-descriptorbits-p

(defthm unsigned-byte-p-when-code-segment-descriptorbits-p
  (implies (code-segment-descriptorbits-p x)
           (unsigned-byte-p 64 x)))

Theorem: code-segment-descriptorbits-p-compound-recognizer

(defthm code-segment-descriptorbits-p-compound-recognizer
  (implies (code-segment-descriptorbits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: code-segment-descriptorbits-fix

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

Theorem: code-segment-descriptorbits-p-of-code-segment-descriptorbits-fix

(defthm
   code-segment-descriptorbits-p-of-code-segment-descriptorbits-fix
  (b* ((fty::fixed (code-segment-descriptorbits-fix x)))
    (code-segment-descriptorbits-p fty::fixed))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits-fix-when-code-segment-descriptorbits-p

(defthm
 code-segment-descriptorbits-fix-when-code-segment-descriptorbits-p
 (implies (code-segment-descriptorbits-p x)
          (equal (code-segment-descriptorbits-fix x)
                 x)))

Function: code-segment-descriptorbits-equiv$inline

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

Theorem: code-segment-descriptorbits-equiv-is-an-equivalence

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

Theorem: code-segment-descriptorbits-equiv-implies-equal-code-segment-descriptorbits-fix-1

(defthm
 code-segment-descriptorbits-equiv-implies-equal-code-segment-descriptorbits-fix-1
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits-fix x)
                 (code-segment-descriptorbits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: code-segment-descriptorbits-fix-under-code-segment-descriptorbits-equiv

(defthm
 code-segment-descriptorbits-fix-under-code-segment-descriptorbits-equiv
 (code-segment-descriptorbits-equiv
      (code-segment-descriptorbits-fix x)
      x)
 :rule-classes (:rewrite :rewrite-quoted-constant))

Function: code-segment-descriptorbits

(defun code-segment-descriptorbits
       (limit15-0 base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24)
 (declare (xargs :guard (and (16bits-p limit15-0)
                             (16bits-p base15-0)
                             (8bits-p base23-16)
                             (bitp a)
                             (bitp r)
                             (bitp c)
                             (bitp msb-of-type)
                             (bitp s)
                             (2bits-p dpl)
                             (bitp p)
                             (4bits-p limit19-16)
                             (bitp avl)
                             (bitp l)
                             (bitp d)
                             (bitp g)
                             (8bits-p base31-24))))
 (let ((__function__ 'code-segment-descriptorbits))
  (declare (ignorable __function__))
  (b* ((limit15-0 (mbe :logic (16bits-fix limit15-0)
                       :exec limit15-0))
       (base15-0 (mbe :logic (16bits-fix base15-0)
                      :exec base15-0))
       (base23-16 (mbe :logic (8bits-fix base23-16)
                       :exec base23-16))
       (a (mbe :logic (bfix a) :exec a))
       (r (mbe :logic (bfix r) :exec r))
       (c (mbe :logic (bfix c) :exec c))
       (msb-of-type (mbe :logic (bfix msb-of-type)
                         :exec msb-of-type))
       (s (mbe :logic (bfix s) :exec s))
       (dpl (mbe :logic (2bits-fix dpl) :exec dpl))
       (p (mbe :logic (bfix p) :exec p))
       (limit19-16 (mbe :logic (4bits-fix limit19-16)
                        :exec limit19-16))
       (avl (mbe :logic (bfix avl) :exec avl))
       (l (mbe :logic (bfix l) :exec l))
       (d (mbe :logic (bfix d) :exec d))
       (g (mbe :logic (bfix g) :exec g))
       (base31-24 (mbe :logic (8bits-fix base31-24)
                       :exec base31-24)))
   (logapp
    16 limit15-0
    (logapp
     16 base15-0
     (logapp
      8 base23-16
      (logapp
       1 a
       (logapp
        1 r
        (logapp
         1 c
         (logapp
          1 msb-of-type
          (logapp
           1 s
           (logapp
            2 dpl
            (logapp
             1 p
             (logapp
              4 limit19-16
              (logapp
                1 avl
                (logapp
                     1 l
                     (logapp 1 d
                             (logapp 1 g base31-24))))))))))))))))))

Theorem: code-segment-descriptorbits-p-of-code-segment-descriptorbits

(defthm code-segment-descriptorbits-p-of-code-segment-descriptorbits
  (b* ((code-segment-descriptorbits
            (code-segment-descriptorbits
                 limit15-0
                 base15-0 base23-16 a r c msb-of-type s
                 dpl p limit19-16 avl l d g base31-24)))
    (code-segment-descriptorbits-p code-segment-descriptorbits))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits-of-16bits-fix-limit15-0

(defthm code-segment-descriptorbits-of-16bits-fix-limit15-0
  (equal (code-segment-descriptorbits
              (16bits-fix limit15-0)
              base15-0 base23-16 a r c msb-of-type
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-16bits-equiv-congruence-on-limit15-0

(defthm
   code-segment-descriptorbits-16bits-equiv-congruence-on-limit15-0
  (implies (16bits-equiv limit15-0 limit15-0-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0-equiv
                       base15-0 base23-16 a r c msb-of-type s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-16bits-fix-base15-0

(defthm code-segment-descriptorbits-of-16bits-fix-base15-0
  (equal (code-segment-descriptorbits
              limit15-0 (16bits-fix base15-0)
              base23-16 a r c msb-of-type
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-16bits-equiv-congruence-on-base15-0

(defthm
    code-segment-descriptorbits-16bits-equiv-congruence-on-base15-0
  (implies (16bits-equiv base15-0 base15-0-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0-equiv
                       base23-16 a r c msb-of-type s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-8bits-fix-base23-16

(defthm code-segment-descriptorbits-of-8bits-fix-base23-16
  (equal (code-segment-descriptorbits
              limit15-0 base15-0 (8bits-fix base23-16)
              a r c msb-of-type
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-8bits-equiv-congruence-on-base23-16

(defthm
    code-segment-descriptorbits-8bits-equiv-congruence-on-base23-16
  (implies (8bits-equiv base23-16 base23-16-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16-equiv a r c msb-of-type s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-a

(defthm code-segment-descriptorbits-of-bfix-a
  (equal (code-segment-descriptorbits
              limit15-0 base15-0 base23-16 (bfix a)
              r c msb-of-type
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-a

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-a
  (implies (bit-equiv a a-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a-equiv r c msb-of-type s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-r

(defthm code-segment-descriptorbits-of-bfix-r
  (equal (code-segment-descriptorbits
              limit15-0 base15-0 base23-16 a (bfix r)
              c msb-of-type
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-r

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-r
  (implies (bit-equiv r r-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r-equiv c msb-of-type s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-c

(defthm code-segment-descriptorbits-of-bfix-c
  (equal (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r (bfix c)
              msb-of-type
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-c

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-c
  (implies (bit-equiv c c-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c-equiv msb-of-type s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-msb-of-type

(defthm code-segment-descriptorbits-of-bfix-msb-of-type
  (equal (code-segment-descriptorbits
              limit15-0 base15-0
              base23-16 a r c (bfix msb-of-type)
              s dpl p limit19-16 avl l d g base31-24)
         (code-segment-descriptorbits
              limit15-0
              base15-0 base23-16 a r c msb-of-type s
              dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-msb-of-type

(defthm
    code-segment-descriptorbits-bit-equiv-congruence-on-msb-of-type
  (implies (bit-equiv msb-of-type msb-of-type-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type-equiv s
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-s

(defthm code-segment-descriptorbits-of-bfix-s
 (equal
  (code-segment-descriptorbits limit15-0 base15-0
                               base23-16 a r c msb-of-type (bfix s)
                               dpl p limit19-16 avl l d g base31-24)
  (code-segment-descriptorbits
       limit15-0
       base15-0 base23-16 a r c msb-of-type s
       dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-s

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-s
  (implies (bit-equiv s s-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s-equiv
                       dpl p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-2bits-fix-dpl

(defthm code-segment-descriptorbits-of-2bits-fix-dpl
 (equal
    (code-segment-descriptorbits limit15-0 base15-0 base23-16
                                 a r c msb-of-type s (2bits-fix dpl)
                                 p limit19-16 avl l d g base31-24)
    (code-segment-descriptorbits
         limit15-0
         base15-0 base23-16 a r c msb-of-type s
         dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-2bits-equiv-congruence-on-dpl

(defthm code-segment-descriptorbits-2bits-equiv-congruence-on-dpl
  (implies (2bits-equiv dpl dpl-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl-equiv
                       p limit19-16 avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-p

(defthm code-segment-descriptorbits-of-bfix-p
  (equal
       (code-segment-descriptorbits limit15-0 base15-0 base23-16
                                    a r c msb-of-type s dpl (bfix p)
                                    limit19-16 avl l d g base31-24)
       (code-segment-descriptorbits
            limit15-0
            base15-0 base23-16 a r c msb-of-type s
            dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-p

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-p
 (implies
  (bit-equiv p p-equiv)
  (equal
      (code-segment-descriptorbits
           limit15-0
           base15-0 base23-16 a r c msb-of-type
           s dpl p limit19-16 avl l d g base31-24)
      (code-segment-descriptorbits limit15-0 base15-0 base23-16
                                   a r c msb-of-type s dpl p-equiv
                                   limit19-16 avl l d g base31-24)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-4bits-fix-limit19-16

(defthm code-segment-descriptorbits-of-4bits-fix-limit19-16
 (equal
   (code-segment-descriptorbits limit15-0
                                base15-0 base23-16 a r c msb-of-type
                                s dpl p (4bits-fix limit19-16)
                                avl l d g base31-24)
   (code-segment-descriptorbits
        limit15-0
        base15-0 base23-16 a r c msb-of-type s
        dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-4bits-equiv-congruence-on-limit19-16

(defthm
   code-segment-descriptorbits-4bits-equiv-congruence-on-limit19-16
  (implies (4bits-equiv limit19-16 limit19-16-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl p
                       limit19-16-equiv avl l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-avl

(defthm code-segment-descriptorbits-of-bfix-avl
 (equal
   (code-segment-descriptorbits limit15-0
                                base15-0 base23-16 a r c msb-of-type
                                s dpl p limit19-16 (bfix avl)
                                l d g base31-24)
   (code-segment-descriptorbits
        limit15-0
        base15-0 base23-16 a r c msb-of-type s
        dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-avl

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-avl
  (implies (bit-equiv avl avl-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl p
                       limit19-16 avl-equiv l d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-l

(defthm code-segment-descriptorbits-of-bfix-l
 (equal
   (code-segment-descriptorbits limit15-0
                                base15-0 base23-16 a r c msb-of-type
                                s dpl p limit19-16 avl (bfix l)
                                d g base31-24)
   (code-segment-descriptorbits
        limit15-0
        base15-0 base23-16 a r c msb-of-type s
        dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-l

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-l
  (implies (bit-equiv l l-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl p
                       limit19-16 avl l-equiv d g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-d

(defthm code-segment-descriptorbits-of-bfix-d
 (equal
   (code-segment-descriptorbits limit15-0
                                base15-0 base23-16 a r c msb-of-type
                                s dpl p limit19-16 avl l (bfix d)
                                g base31-24)
   (code-segment-descriptorbits
        limit15-0
        base15-0 base23-16 a r c msb-of-type s
        dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-d

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-d
  (implies (bit-equiv d d-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl p
                       limit19-16 avl l d-equiv g base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-bfix-g

(defthm code-segment-descriptorbits-of-bfix-g
 (equal
   (code-segment-descriptorbits limit15-0
                                base15-0 base23-16 a r c msb-of-type
                                s dpl p limit19-16 avl l d (bfix g)
                                base31-24)
   (code-segment-descriptorbits
        limit15-0
        base15-0 base23-16 a r c msb-of-type s
        dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-bit-equiv-congruence-on-g

(defthm code-segment-descriptorbits-bit-equiv-congruence-on-g
  (implies (bit-equiv g g-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl p
                       limit19-16 avl l d g-equiv base31-24)))
  :rule-classes :congruence)

Theorem: code-segment-descriptorbits-of-8bits-fix-base31-24

(defthm code-segment-descriptorbits-of-8bits-fix-base31-24
 (equal
   (code-segment-descriptorbits limit15-0 base15-0 base23-16
                                a r c msb-of-type s dpl p limit19-16
                                avl l d g (8bits-fix base31-24))
   (code-segment-descriptorbits
        limit15-0
        base15-0 base23-16 a r c msb-of-type s
        dpl p limit19-16 avl l d g base31-24)))

Theorem: code-segment-descriptorbits-8bits-equiv-congruence-on-base31-24

(defthm
    code-segment-descriptorbits-8bits-equiv-congruence-on-base31-24
  (implies (8bits-equiv base31-24 base31-24-equiv)
           (equal (code-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 a r c msb-of-type
                       s dpl p limit19-16 avl l d g base31-24)
                  (code-segment-descriptorbits
                       limit15-0 base15-0
                       base23-16 a r c msb-of-type s dpl p
                       limit19-16 avl l d g base31-24-equiv)))
  :rule-classes :congruence)

Function: code-segment-descriptorbits-equiv-under-mask

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

Function: code-segment-descriptorbits->limit15-0$inline

(defun code-segment-descriptorbits->limit15-0$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 0 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 64) x)))))

Theorem: 16bits-p-of-code-segment-descriptorbits->limit15-0

(defthm 16bits-p-of-code-segment-descriptorbits->limit15-0
 (b* ((limit15-0 (code-segment-descriptorbits->limit15-0$inline x)))
   (16bits-p limit15-0))
 :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->limit15-0$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->limit15-0$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->limit15-0$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->limit15-0$inline x)))

Theorem: code-segment-descriptorbits->limit15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->limit15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
    (code-segment-descriptorbits-equiv x x-equiv)
    (equal (code-segment-descriptorbits->limit15-0$inline x)
           (code-segment-descriptorbits->limit15-0$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->limit15-0-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits->limit15-0-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits->limit15-0
             (code-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24))
        (16bits-fix limit15-0)))

Theorem: code-segment-descriptorbits->limit15-0-of-write-with-mask

(defthm code-segment-descriptorbits->limit15-0-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask) 65535)
               0))
   (equal (code-segment-descriptorbits->limit15-0 x)
          (code-segment-descriptorbits->limit15-0 y))))

Function: code-segment-descriptorbits->base15-0$inline

(defun code-segment-descriptorbits->base15-0$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 16 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 48)
                               (ash (the (unsigned-byte 64) x)
                                    -16))))))

Theorem: 16bits-p-of-code-segment-descriptorbits->base15-0

(defthm 16bits-p-of-code-segment-descriptorbits->base15-0
  (b* ((base15-0 (code-segment-descriptorbits->base15-0$inline x)))
    (16bits-p base15-0))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->base15-0$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->base15-0$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->base15-0$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->base15-0$inline x)))

Theorem: code-segment-descriptorbits->base15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->base15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
     (code-segment-descriptorbits-equiv x x-equiv)
     (equal (code-segment-descriptorbits->base15-0$inline x)
            (code-segment-descriptorbits->base15-0$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->base15-0-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits->base15-0-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits->base15-0
             (code-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24))
        (16bits-fix base15-0)))

Theorem: code-segment-descriptorbits->base15-0-of-write-with-mask

(defthm code-segment-descriptorbits->base15-0-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask) 4294901760)
               0))
   (equal (code-segment-descriptorbits->base15-0 x)
          (code-segment-descriptorbits->base15-0 y))))

Function: code-segment-descriptorbits->base23-16$inline

(defun code-segment-descriptorbits->base23-16$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 32 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 32)
                               (ash (the (unsigned-byte 64) x)
                                    -32))))))

Theorem: 8bits-p-of-code-segment-descriptorbits->base23-16

(defthm 8bits-p-of-code-segment-descriptorbits->base23-16
 (b* ((base23-16 (code-segment-descriptorbits->base23-16$inline x)))
   (8bits-p base23-16))
 :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->base23-16$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->base23-16$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->base23-16$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->base23-16$inline x)))

Theorem: code-segment-descriptorbits->base23-16$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->base23-16$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
    (code-segment-descriptorbits-equiv x x-equiv)
    (equal (code-segment-descriptorbits->base23-16$inline x)
           (code-segment-descriptorbits->base23-16$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->base23-16-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits->base23-16-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits->base23-16
             (code-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24))
        (8bits-fix base23-16)))

Theorem: code-segment-descriptorbits->base23-16-of-write-with-mask

(defthm code-segment-descriptorbits->base23-16-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       1095216660480)
               0))
   (equal (code-segment-descriptorbits->base23-16 x)
          (code-segment-descriptorbits->base23-16 y))))

Function: code-segment-descriptorbits->a$inline

(defun code-segment-descriptorbits->a$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 40 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 24)
                               (ash (the (unsigned-byte 64) x)
                                    -40))))))

Theorem: bitp-of-code-segment-descriptorbits->a

(defthm bitp-of-code-segment-descriptorbits->a
  (b* ((a (code-segment-descriptorbits->a$inline x)))
    (bitp a))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->a$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->a$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->a$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->a$inline x)))

Theorem: code-segment-descriptorbits->a$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->a$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->a$inline x)
                 (code-segment-descriptorbits->a$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->a-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->a-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->a
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix a)))

Theorem: code-segment-descriptorbits->a-of-write-with-mask

(defthm code-segment-descriptorbits->a-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       1099511627776)
               0))
   (equal (code-segment-descriptorbits->a x)
          (code-segment-descriptorbits->a y))))

Function: code-segment-descriptorbits->r$inline

(defun code-segment-descriptorbits->r$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 41 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 23)
                               (ash (the (unsigned-byte 64) x)
                                    -41))))))

Theorem: bitp-of-code-segment-descriptorbits->r

(defthm bitp-of-code-segment-descriptorbits->r
  (b* ((r (code-segment-descriptorbits->r$inline x)))
    (bitp r))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->r$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->r$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->r$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->r$inline x)))

Theorem: code-segment-descriptorbits->r$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->r$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->r$inline x)
                 (code-segment-descriptorbits->r$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->r-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->r-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->r
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix r)))

Theorem: code-segment-descriptorbits->r-of-write-with-mask

(defthm code-segment-descriptorbits->r-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       2199023255552)
               0))
   (equal (code-segment-descriptorbits->r x)
          (code-segment-descriptorbits->r y))))

Function: code-segment-descriptorbits->c$inline

(defun code-segment-descriptorbits->c$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 42 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 22)
                               (ash (the (unsigned-byte 64) x)
                                    -42))))))

Theorem: bitp-of-code-segment-descriptorbits->c

(defthm bitp-of-code-segment-descriptorbits->c
  (b* ((c (code-segment-descriptorbits->c$inline x)))
    (bitp c))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->c$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->c$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->c$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->c$inline x)))

Theorem: code-segment-descriptorbits->c$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->c$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->c$inline x)
                 (code-segment-descriptorbits->c$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->c-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->c-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->c
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix c)))

Theorem: code-segment-descriptorbits->c-of-write-with-mask

(defthm code-segment-descriptorbits->c-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       4398046511104)
               0))
   (equal (code-segment-descriptorbits->c x)
          (code-segment-descriptorbits->c y))))

Function: code-segment-descriptorbits->msb-of-type$inline

(defun code-segment-descriptorbits->msb-of-type$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 43 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 21)
                               (ash (the (unsigned-byte 64) x)
                                    -43))))))

Theorem: bitp-of-code-segment-descriptorbits->msb-of-type

(defthm bitp-of-code-segment-descriptorbits->msb-of-type
  (b* ((msb-of-type
            (code-segment-descriptorbits->msb-of-type$inline x)))
    (bitp msb-of-type))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->msb-of-type$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->msb-of-type$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->msb-of-type$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->msb-of-type$inline x)))

Theorem: code-segment-descriptorbits->msb-of-type$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->msb-of-type$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (code-segment-descriptorbits-equiv x x-equiv)
  (equal (code-segment-descriptorbits->msb-of-type$inline x)
         (code-segment-descriptorbits->msb-of-type$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->msb-of-type-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits->msb-of-type-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits->msb-of-type
             (code-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24))
        (bfix msb-of-type)))

Theorem: code-segment-descriptorbits->msb-of-type-of-write-with-mask

(defthm code-segment-descriptorbits->msb-of-type-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       8796093022208)
               0))
   (equal (code-segment-descriptorbits->msb-of-type x)
          (code-segment-descriptorbits->msb-of-type y))))

Function: code-segment-descriptorbits->s$inline

(defun code-segment-descriptorbits->s$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 44 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 20)
                               (ash (the (unsigned-byte 64) x)
                                    -44))))))

Theorem: bitp-of-code-segment-descriptorbits->s

(defthm bitp-of-code-segment-descriptorbits->s
  (b* ((s (code-segment-descriptorbits->s$inline x)))
    (bitp s))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->s$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->s$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->s$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->s$inline x)))

Theorem: code-segment-descriptorbits->s$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->s$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->s$inline x)
                 (code-segment-descriptorbits->s$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->s-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->s-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->s
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix s)))

Theorem: code-segment-descriptorbits->s-of-write-with-mask

(defthm code-segment-descriptorbits->s-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       17592186044416)
               0))
   (equal (code-segment-descriptorbits->s x)
          (code-segment-descriptorbits->s y))))

Function: code-segment-descriptorbits->dpl$inline

(defun code-segment-descriptorbits->dpl$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 45 :width 2))
       :exec (the (unsigned-byte 2)
                  (logand (the (unsigned-byte 2) 3)
                          (the (unsigned-byte 19)
                               (ash (the (unsigned-byte 64) x)
                                    -45))))))

Theorem: 2bits-p-of-code-segment-descriptorbits->dpl

(defthm 2bits-p-of-code-segment-descriptorbits->dpl
  (b* ((dpl (code-segment-descriptorbits->dpl$inline x)))
    (2bits-p dpl))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->dpl$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->dpl$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->dpl$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->dpl$inline x)))

Theorem: code-segment-descriptorbits->dpl$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->dpl$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->dpl$inline x)
                 (code-segment-descriptorbits->dpl$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->dpl-of-code-segment-descriptorbits

(defthm
    code-segment-descriptorbits->dpl-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->dpl
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (2bits-fix dpl)))

Theorem: code-segment-descriptorbits->dpl-of-write-with-mask

(defthm code-segment-descriptorbits->dpl-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       105553116266496)
               0))
   (equal (code-segment-descriptorbits->dpl x)
          (code-segment-descriptorbits->dpl y))))

Function: code-segment-descriptorbits->p$inline

(defun code-segment-descriptorbits->p$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 47 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 17)
                               (ash (the (unsigned-byte 64) x)
                                    -47))))))

Theorem: bitp-of-code-segment-descriptorbits->p

(defthm bitp-of-code-segment-descriptorbits->p
  (b* ((p (code-segment-descriptorbits->p$inline x)))
    (bitp p))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->p$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->p$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->p$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->p$inline x)))

Theorem: code-segment-descriptorbits->p$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->p$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->p$inline x)
                 (code-segment-descriptorbits->p$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->p-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->p-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->p
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix p)))

Theorem: code-segment-descriptorbits->p-of-write-with-mask

(defthm code-segment-descriptorbits->p-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       140737488355328)
               0))
   (equal (code-segment-descriptorbits->p x)
          (code-segment-descriptorbits->p y))))

Function: code-segment-descriptorbits->limit19-16$inline

(defun code-segment-descriptorbits->limit19-16$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 48 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 16)
                               (ash (the (unsigned-byte 64) x)
                                    -48))))))

Theorem: 4bits-p-of-code-segment-descriptorbits->limit19-16

(defthm 4bits-p-of-code-segment-descriptorbits->limit19-16
  (b*
   ((limit19-16 (code-segment-descriptorbits->limit19-16$inline x)))
   (4bits-p limit19-16))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->limit19-16$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->limit19-16$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->limit19-16$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->limit19-16$inline x)))

Theorem: code-segment-descriptorbits->limit19-16$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->limit19-16$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
   (code-segment-descriptorbits-equiv x x-equiv)
   (equal (code-segment-descriptorbits->limit19-16$inline x)
          (code-segment-descriptorbits->limit19-16$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->limit19-16-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits->limit19-16-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits->limit19-16
             (code-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24))
        (4bits-fix limit19-16)))

Theorem: code-segment-descriptorbits->limit19-16-of-write-with-mask

(defthm code-segment-descriptorbits->limit19-16-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       4222124650659840)
               0))
   (equal (code-segment-descriptorbits->limit19-16 x)
          (code-segment-descriptorbits->limit19-16 y))))

Function: code-segment-descriptorbits->avl$inline

(defun code-segment-descriptorbits->avl$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 52 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 12)
                               (ash (the (unsigned-byte 64) x)
                                    -52))))))

Theorem: bitp-of-code-segment-descriptorbits->avl

(defthm bitp-of-code-segment-descriptorbits->avl
  (b* ((avl (code-segment-descriptorbits->avl$inline x)))
    (bitp avl))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->avl$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->avl$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->avl$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->avl$inline x)))

Theorem: code-segment-descriptorbits->avl$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->avl$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->avl$inline x)
                 (code-segment-descriptorbits->avl$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->avl-of-code-segment-descriptorbits

(defthm
    code-segment-descriptorbits->avl-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->avl
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix avl)))

Theorem: code-segment-descriptorbits->avl-of-write-with-mask

(defthm code-segment-descriptorbits->avl-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       4503599627370496)
               0))
   (equal (code-segment-descriptorbits->avl x)
          (code-segment-descriptorbits->avl y))))

Function: code-segment-descriptorbits->l$inline

(defun code-segment-descriptorbits->l$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 53 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 11)
                               (ash (the (unsigned-byte 64) x)
                                    -53))))))

Theorem: bitp-of-code-segment-descriptorbits->l

(defthm bitp-of-code-segment-descriptorbits->l
  (b* ((l (code-segment-descriptorbits->l$inline x)))
    (bitp l))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->l$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->l$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->l$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->l$inline x)))

Theorem: code-segment-descriptorbits->l$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->l$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->l$inline x)
                 (code-segment-descriptorbits->l$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->l-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->l-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->l
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix l)))

Theorem: code-segment-descriptorbits->l-of-write-with-mask

(defthm code-segment-descriptorbits->l-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       9007199254740992)
               0))
   (equal (code-segment-descriptorbits->l x)
          (code-segment-descriptorbits->l y))))

Function: code-segment-descriptorbits->d$inline

(defun code-segment-descriptorbits->d$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 54 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 10)
                               (ash (the (unsigned-byte 64) x)
                                    -54))))))

Theorem: bitp-of-code-segment-descriptorbits->d

(defthm bitp-of-code-segment-descriptorbits->d
  (b* ((d (code-segment-descriptorbits->d$inline x)))
    (bitp d))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->d$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->d$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->d$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->d$inline x)))

Theorem: code-segment-descriptorbits->d$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->d$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->d$inline x)
                 (code-segment-descriptorbits->d$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->d-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->d-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->d
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix d)))

Theorem: code-segment-descriptorbits->d-of-write-with-mask

(defthm code-segment-descriptorbits->d-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       18014398509481984)
               0))
   (equal (code-segment-descriptorbits->d x)
          (code-segment-descriptorbits->d y))))

Function: code-segment-descriptorbits->g$inline

(defun code-segment-descriptorbits->g$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 55 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 9)
                               (ash (the (unsigned-byte 64) x)
                                    -55))))))

Theorem: bitp-of-code-segment-descriptorbits->g

(defthm bitp-of-code-segment-descriptorbits->g
  (b* ((g (code-segment-descriptorbits->g$inline x)))
    (bitp g))
  :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->g$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->g$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->g$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->g$inline x)))

Theorem: code-segment-descriptorbits->g$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->g$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies (code-segment-descriptorbits-equiv x x-equiv)
          (equal (code-segment-descriptorbits->g$inline x)
                 (code-segment-descriptorbits->g$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->g-of-code-segment-descriptorbits

(defthm
      code-segment-descriptorbits->g-of-code-segment-descriptorbits
  (equal (code-segment-descriptorbits->g
              (code-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a r c msb-of-type
                   s dpl p limit19-16 avl l d g base31-24))
         (bfix g)))

Theorem: code-segment-descriptorbits->g-of-write-with-mask

(defthm code-segment-descriptorbits->g-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       36028797018963968)
               0))
   (equal (code-segment-descriptorbits->g x)
          (code-segment-descriptorbits->g y))))

Function: code-segment-descriptorbits->base31-24$inline

(defun code-segment-descriptorbits->base31-24$inline (x)
  (declare (xargs :guard (code-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (code-segment-descriptorbits-fix x)))
         (part-select x :low 56 :width 8))
       :exec (the (unsigned-byte 8)
                  (logand (the (unsigned-byte 8) 255)
                          (the (unsigned-byte 8)
                               (ash (the (unsigned-byte 64) x)
                                    -56))))))

Theorem: 8bits-p-of-code-segment-descriptorbits->base31-24

(defthm 8bits-p-of-code-segment-descriptorbits->base31-24
 (b* ((base31-24 (code-segment-descriptorbits->base31-24$inline x)))
   (8bits-p base31-24))
 :rule-classes :rewrite)

Theorem: code-segment-descriptorbits->base31-24$inline-of-code-segment-descriptorbits-fix-x

(defthm
 code-segment-descriptorbits->base31-24$inline-of-code-segment-descriptorbits-fix-x
 (equal (code-segment-descriptorbits->base31-24$inline
             (code-segment-descriptorbits-fix x))
        (code-segment-descriptorbits->base31-24$inline x)))

Theorem: code-segment-descriptorbits->base31-24$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 code-segment-descriptorbits->base31-24$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
    (code-segment-descriptorbits-equiv x x-equiv)
    (equal (code-segment-descriptorbits->base31-24$inline x)
           (code-segment-descriptorbits->base31-24$inline x-equiv)))
 :rule-classes :congruence)

Theorem: code-segment-descriptorbits->base31-24-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits->base31-24-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits->base31-24
             (code-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a r c msb-of-type
                  s dpl p limit19-16 avl l d g base31-24))
        (8bits-fix base31-24)))

Theorem: code-segment-descriptorbits->base31-24-of-write-with-mask

(defthm code-segment-descriptorbits->base31-24-of-write-with-mask
 (implies
   (and (fty::bitstruct-read-over-write-hyps
             x
             code-segment-descriptorbits-equiv-under-mask)
        (code-segment-descriptorbits-equiv-under-mask x y fty::mask)
        (equal (logand (lognot fty::mask)
                       18374686479671623680)
               0))
   (equal (code-segment-descriptorbits->base31-24 x)
          (code-segment-descriptorbits->base31-24 y))))

Theorem: code-segment-descriptorbits-fix-in-terms-of-code-segment-descriptorbits

(defthm
 code-segment-descriptorbits-fix-in-terms-of-code-segment-descriptorbits
 (equal (code-segment-descriptorbits-fix x)
        (change-code-segment-descriptorbits x)))

Function: !code-segment-descriptorbits->limit15-0$inline

(defun !code-segment-descriptorbits->limit15-0$inline (limit15-0 x)
 (declare (xargs :guard (and (16bits-p limit15-0)
                             (code-segment-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((limit15-0 (mbe :logic (16bits-fix limit15-0)
                          :exec limit15-0))
          (x (code-segment-descriptorbits-fix x)))
       (part-install limit15-0 x
                     :width 16
                     :low 0))
     :exec (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64)
                             (logand (the (unsigned-byte 64) x)
                                     (the (signed-byte 17) -65536)))
                        (the (unsigned-byte 16) limit15-0)))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->limit15-0

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->limit15-0
 (b*
  ((new-x
      (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)))
  (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->limit15-0$inline-of-16bits-fix-limit15-0

(defthm
 !code-segment-descriptorbits->limit15-0$inline-of-16bits-fix-limit15-0
 (equal
      (!code-segment-descriptorbits->limit15-0$inline
           (16bits-fix limit15-0)
           x)
      (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)))

Theorem: !code-segment-descriptorbits->limit15-0$inline-16bits-equiv-congruence-on-limit15-0

(defthm
 !code-segment-descriptorbits->limit15-0$inline-16bits-equiv-congruence-on-limit15-0
 (implies
   (16bits-equiv limit15-0 limit15-0-equiv)
   (equal
        (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)
        (!code-segment-descriptorbits->limit15-0$inline
             limit15-0-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->limit15-0$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->limit15-0$inline-of-code-segment-descriptorbits-fix-x
 (equal
      (!code-segment-descriptorbits->limit15-0$inline
           limit15-0
           (code-segment-descriptorbits-fix x))
      (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)))

Theorem: !code-segment-descriptorbits->limit15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->limit15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
   (code-segment-descriptorbits-equiv x x-equiv)
   (equal
        (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)
        (!code-segment-descriptorbits->limit15-0$inline
             limit15-0 x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->limit15-0-is-code-segment-descriptorbits

(defthm
 !code-segment-descriptorbits->limit15-0-is-code-segment-descriptorbits
 (equal (!code-segment-descriptorbits->limit15-0 limit15-0 x)
        (change-code-segment-descriptorbits x
                                            :limit15-0 limit15-0)))

Theorem: code-segment-descriptorbits->limit15-0-of-!code-segment-descriptorbits->limit15-0

(defthm
 code-segment-descriptorbits->limit15-0-of-!code-segment-descriptorbits->limit15-0
 (b*
  ((?new-x
      (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)))
  (equal (code-segment-descriptorbits->limit15-0 new-x)
         (16bits-fix limit15-0))))

Theorem: !code-segment-descriptorbits->limit15-0-equiv-under-mask

(defthm !code-segment-descriptorbits->limit15-0-equiv-under-mask
 (b*
  ((?new-x
      (!code-segment-descriptorbits->limit15-0$inline limit15-0 x)))
  (code-segment-descriptorbits-equiv-under-mask new-x x -65536)))

Function: !code-segment-descriptorbits->base15-0$inline

(defun !code-segment-descriptorbits->base15-0$inline (base15-0 x)
 (declare (xargs :guard (and (16bits-p base15-0)
                             (code-segment-descriptorbits-p x))))
 (mbe :logic
      (b* ((base15-0 (mbe :logic (16bits-fix base15-0)
                          :exec base15-0))
           (x (code-segment-descriptorbits-fix x)))
        (part-install base15-0 x
                      :width 16
                      :low 16))
      :exec
      (the (unsigned-byte 64)
           (logior (the (unsigned-byte 64)
                        (logand (the (unsigned-byte 64) x)
                                (the (signed-byte 33) -4294901761)))
                   (the (unsigned-byte 32)
                        (ash (the (unsigned-byte 16) base15-0)
                             16))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base15-0

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base15-0
 (b*
  ((new-x
        (!code-segment-descriptorbits->base15-0$inline base15-0 x)))
  (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->base15-0$inline-of-16bits-fix-base15-0

(defthm
 !code-segment-descriptorbits->base15-0$inline-of-16bits-fix-base15-0
 (equal (!code-segment-descriptorbits->base15-0$inline
             (16bits-fix base15-0)
             x)
        (!code-segment-descriptorbits->base15-0$inline base15-0 x)))

Theorem: !code-segment-descriptorbits->base15-0$inline-16bits-equiv-congruence-on-base15-0

(defthm
 !code-segment-descriptorbits->base15-0$inline-16bits-equiv-congruence-on-base15-0
 (implies
   (16bits-equiv base15-0 base15-0-equiv)
   (equal (!code-segment-descriptorbits->base15-0$inline base15-0 x)
          (!code-segment-descriptorbits->base15-0$inline
               base15-0-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->base15-0$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->base15-0$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->base15-0$inline
             base15-0
             (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->base15-0$inline base15-0 x)))

Theorem: !code-segment-descriptorbits->base15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->base15-0$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
   (code-segment-descriptorbits-equiv x x-equiv)
   (equal (!code-segment-descriptorbits->base15-0$inline base15-0 x)
          (!code-segment-descriptorbits->base15-0$inline
               base15-0 x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->base15-0-is-code-segment-descriptorbits

(defthm
 !code-segment-descriptorbits->base15-0-is-code-segment-descriptorbits
 (equal (!code-segment-descriptorbits->base15-0 base15-0 x)
        (change-code-segment-descriptorbits x
                                            :base15-0 base15-0)))

Theorem: code-segment-descriptorbits->base15-0-of-!code-segment-descriptorbits->base15-0

(defthm
 code-segment-descriptorbits->base15-0-of-!code-segment-descriptorbits->base15-0
 (b*
  ((?new-x
        (!code-segment-descriptorbits->base15-0$inline base15-0 x)))
  (equal (code-segment-descriptorbits->base15-0 new-x)
         (16bits-fix base15-0))))

Theorem: !code-segment-descriptorbits->base15-0-equiv-under-mask

(defthm !code-segment-descriptorbits->base15-0-equiv-under-mask
 (b*
  ((?new-x
        (!code-segment-descriptorbits->base15-0$inline base15-0 x)))
  (code-segment-descriptorbits-equiv-under-mask
       new-x x -4294901761)))

Function: !code-segment-descriptorbits->base23-16$inline

(defun !code-segment-descriptorbits->base23-16$inline (base23-16 x)
 (declare (xargs :guard (and (8bits-p base23-16)
                             (code-segment-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((base23-16 (mbe :logic (8bits-fix base23-16)
                        :exec base23-16))
        (x (code-segment-descriptorbits-fix x)))
     (part-install base23-16 x
                   :width 8
                   :low 32))
   :exec
   (the (unsigned-byte 64)
        (logior (the (unsigned-byte 64)
                     (logand (the (unsigned-byte 64) x)
                             (the (signed-byte 41) -1095216660481)))
                (the (unsigned-byte 40)
                     (ash (the (unsigned-byte 8) base23-16)
                          32))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base23-16

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base23-16
 (b*
  ((new-x
      (!code-segment-descriptorbits->base23-16$inline base23-16 x)))
  (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->base23-16$inline-of-8bits-fix-base23-16

(defthm
 !code-segment-descriptorbits->base23-16$inline-of-8bits-fix-base23-16
 (equal
      (!code-segment-descriptorbits->base23-16$inline
           (8bits-fix base23-16)
           x)
      (!code-segment-descriptorbits->base23-16$inline base23-16 x)))

Theorem: !code-segment-descriptorbits->base23-16$inline-8bits-equiv-congruence-on-base23-16

(defthm
 !code-segment-descriptorbits->base23-16$inline-8bits-equiv-congruence-on-base23-16
 (implies
   (8bits-equiv base23-16 base23-16-equiv)
   (equal
        (!code-segment-descriptorbits->base23-16$inline base23-16 x)
        (!code-segment-descriptorbits->base23-16$inline
             base23-16-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->base23-16$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->base23-16$inline-of-code-segment-descriptorbits-fix-x
 (equal
      (!code-segment-descriptorbits->base23-16$inline
           base23-16
           (code-segment-descriptorbits-fix x))
      (!code-segment-descriptorbits->base23-16$inline base23-16 x)))

Theorem: !code-segment-descriptorbits->base23-16$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->base23-16$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
   (code-segment-descriptorbits-equiv x x-equiv)
   (equal
        (!code-segment-descriptorbits->base23-16$inline base23-16 x)
        (!code-segment-descriptorbits->base23-16$inline
             base23-16 x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->base23-16-is-code-segment-descriptorbits

(defthm
 !code-segment-descriptorbits->base23-16-is-code-segment-descriptorbits
 (equal (!code-segment-descriptorbits->base23-16 base23-16 x)
        (change-code-segment-descriptorbits x
                                            :base23-16 base23-16)))

Theorem: code-segment-descriptorbits->base23-16-of-!code-segment-descriptorbits->base23-16

(defthm
 code-segment-descriptorbits->base23-16-of-!code-segment-descriptorbits->base23-16
 (b*
  ((?new-x
      (!code-segment-descriptorbits->base23-16$inline base23-16 x)))
  (equal (code-segment-descriptorbits->base23-16 new-x)
         (8bits-fix base23-16))))

Theorem: !code-segment-descriptorbits->base23-16-equiv-under-mask

(defthm !code-segment-descriptorbits->base23-16-equiv-under-mask
 (b*
  ((?new-x
      (!code-segment-descriptorbits->base23-16$inline base23-16 x)))
  (code-segment-descriptorbits-equiv-under-mask
       new-x x -1095216660481)))

Function: !code-segment-descriptorbits->a$inline

(defun !code-segment-descriptorbits->a$inline (a x)
 (declare (xargs :guard (and (bitp a)
                             (code-segment-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((a (mbe :logic (bfix a) :exec a))
        (x (code-segment-descriptorbits-fix x)))
     (part-install a x :width 1 :low 40))
   :exec
   (the (unsigned-byte 64)
        (logior (the (unsigned-byte 64)
                     (logand (the (unsigned-byte 64) x)
                             (the (signed-byte 42) -1099511627777)))
                (the (unsigned-byte 41)
                     (ash (the (unsigned-byte 1) a) 40))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->a

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->a
  (b* ((new-x (!code-segment-descriptorbits->a$inline a x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->a$inline-of-bfix-a

(defthm !code-segment-descriptorbits->a$inline-of-bfix-a
  (equal (!code-segment-descriptorbits->a$inline (bfix a)
                                                 x)
         (!code-segment-descriptorbits->a$inline a x)))

Theorem: !code-segment-descriptorbits->a$inline-bit-equiv-congruence-on-a

(defthm
   !code-segment-descriptorbits->a$inline-bit-equiv-congruence-on-a
  (implies
       (bit-equiv a a-equiv)
       (equal (!code-segment-descriptorbits->a$inline a x)
              (!code-segment-descriptorbits->a$inline a-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->a$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->a$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->a$inline
             a (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->a$inline a x)))

Theorem: !code-segment-descriptorbits->a$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->a$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->a$inline a x)
             (!code-segment-descriptorbits->a$inline a x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->a-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->a-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->a a x)
         (change-code-segment-descriptorbits x
                                             :a a)))

Theorem: code-segment-descriptorbits->a-of-!code-segment-descriptorbits->a

(defthm
  code-segment-descriptorbits->a-of-!code-segment-descriptorbits->a
  (b* ((?new-x (!code-segment-descriptorbits->a$inline a x)))
    (equal (code-segment-descriptorbits->a new-x)
           (bfix a))))

Theorem: !code-segment-descriptorbits->a-equiv-under-mask

(defthm !code-segment-descriptorbits->a-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->a$inline a x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -1099511627777)))

Function: !code-segment-descriptorbits->r$inline

(defun !code-segment-descriptorbits->r$inline (r x)
 (declare (xargs :guard (and (bitp r)
                             (code-segment-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((r (mbe :logic (bfix r) :exec r))
        (x (code-segment-descriptorbits-fix x)))
     (part-install r x :width 1 :low 41))
   :exec
   (the (unsigned-byte 64)
        (logior (the (unsigned-byte 64)
                     (logand (the (unsigned-byte 64) x)
                             (the (signed-byte 43) -2199023255553)))
                (the (unsigned-byte 42)
                     (ash (the (unsigned-byte 1) r) 41))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->r

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->r
  (b* ((new-x (!code-segment-descriptorbits->r$inline r x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->r$inline-of-bfix-r

(defthm !code-segment-descriptorbits->r$inline-of-bfix-r
  (equal (!code-segment-descriptorbits->r$inline (bfix r)
                                                 x)
         (!code-segment-descriptorbits->r$inline r x)))

Theorem: !code-segment-descriptorbits->r$inline-bit-equiv-congruence-on-r

(defthm
   !code-segment-descriptorbits->r$inline-bit-equiv-congruence-on-r
  (implies
       (bit-equiv r r-equiv)
       (equal (!code-segment-descriptorbits->r$inline r x)
              (!code-segment-descriptorbits->r$inline r-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->r$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->r$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->r$inline
             r (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->r$inline r x)))

Theorem: !code-segment-descriptorbits->r$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->r$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->r$inline r x)
             (!code-segment-descriptorbits->r$inline r x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->r-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->r-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->r r x)
         (change-code-segment-descriptorbits x
                                             :r r)))

Theorem: code-segment-descriptorbits->r-of-!code-segment-descriptorbits->r

(defthm
  code-segment-descriptorbits->r-of-!code-segment-descriptorbits->r
  (b* ((?new-x (!code-segment-descriptorbits->r$inline r x)))
    (equal (code-segment-descriptorbits->r new-x)
           (bfix r))))

Theorem: !code-segment-descriptorbits->r-equiv-under-mask

(defthm !code-segment-descriptorbits->r-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->r$inline r x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -2199023255553)))

Function: !code-segment-descriptorbits->c$inline

(defun !code-segment-descriptorbits->c$inline (c x)
 (declare (xargs :guard (and (bitp c)
                             (code-segment-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((c (mbe :logic (bfix c) :exec c))
        (x (code-segment-descriptorbits-fix x)))
     (part-install c x :width 1 :low 42))
   :exec
   (the (unsigned-byte 64)
        (logior (the (unsigned-byte 64)
                     (logand (the (unsigned-byte 64) x)
                             (the (signed-byte 44) -4398046511105)))
                (the (unsigned-byte 43)
                     (ash (the (unsigned-byte 1) c) 42))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->c

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->c
  (b* ((new-x (!code-segment-descriptorbits->c$inline c x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->c$inline-of-bfix-c

(defthm !code-segment-descriptorbits->c$inline-of-bfix-c
  (equal (!code-segment-descriptorbits->c$inline (bfix c)
                                                 x)
         (!code-segment-descriptorbits->c$inline c x)))

Theorem: !code-segment-descriptorbits->c$inline-bit-equiv-congruence-on-c

(defthm
   !code-segment-descriptorbits->c$inline-bit-equiv-congruence-on-c
  (implies
       (bit-equiv c c-equiv)
       (equal (!code-segment-descriptorbits->c$inline c x)
              (!code-segment-descriptorbits->c$inline c-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->c$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->c$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->c$inline
             c (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->c$inline c x)))

Theorem: !code-segment-descriptorbits->c$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->c$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->c$inline c x)
             (!code-segment-descriptorbits->c$inline c x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->c-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->c-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->c c x)
         (change-code-segment-descriptorbits x
                                             :c c)))

Theorem: code-segment-descriptorbits->c-of-!code-segment-descriptorbits->c

(defthm
  code-segment-descriptorbits->c-of-!code-segment-descriptorbits->c
  (b* ((?new-x (!code-segment-descriptorbits->c$inline c x)))
    (equal (code-segment-descriptorbits->c new-x)
           (bfix c))))

Theorem: !code-segment-descriptorbits->c-equiv-under-mask

(defthm !code-segment-descriptorbits->c-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->c$inline c x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -4398046511105)))

Function: !code-segment-descriptorbits->msb-of-type$inline

(defun !code-segment-descriptorbits->msb-of-type$inline
       (msb-of-type x)
 (declare (xargs :guard (and (bitp msb-of-type)
                             (code-segment-descriptorbits-p x))))
 (mbe
   :logic
   (b* ((msb-of-type (mbe :logic (bfix msb-of-type)
                          :exec msb-of-type))
        (x (code-segment-descriptorbits-fix x)))
     (part-install msb-of-type x
                   :width 1
                   :low 43))
   :exec
   (the (unsigned-byte 64)
        (logior (the (unsigned-byte 64)
                     (logand (the (unsigned-byte 64) x)
                             (the (signed-byte 45) -8796093022209)))
                (the (unsigned-byte 44)
                     (ash (the (unsigned-byte 1) msb-of-type)
                          43))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->msb-of-type

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->msb-of-type
 (b* ((new-x (!code-segment-descriptorbits->msb-of-type$inline
                  msb-of-type x)))
   (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->msb-of-type$inline-of-bfix-msb-of-type

(defthm
 !code-segment-descriptorbits->msb-of-type$inline-of-bfix-msb-of-type
 (equal
  (!code-segment-descriptorbits->msb-of-type$inline
       (bfix msb-of-type)
       x)
  (!code-segment-descriptorbits->msb-of-type$inline msb-of-type x)))

Theorem: !code-segment-descriptorbits->msb-of-type$inline-bit-equiv-congruence-on-msb-of-type

(defthm
 !code-segment-descriptorbits->msb-of-type$inline-bit-equiv-congruence-on-msb-of-type
 (implies
  (bit-equiv msb-of-type msb-of-type-equiv)
  (equal
    (!code-segment-descriptorbits->msb-of-type$inline msb-of-type x)
    (!code-segment-descriptorbits->msb-of-type$inline
         msb-of-type-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->msb-of-type$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->msb-of-type$inline-of-code-segment-descriptorbits-fix-x
 (equal
  (!code-segment-descriptorbits->msb-of-type$inline
       msb-of-type
       (code-segment-descriptorbits-fix x))
  (!code-segment-descriptorbits->msb-of-type$inline msb-of-type x)))

Theorem: !code-segment-descriptorbits->msb-of-type$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->msb-of-type$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (code-segment-descriptorbits-equiv x x-equiv)
  (equal
    (!code-segment-descriptorbits->msb-of-type$inline msb-of-type x)
    (!code-segment-descriptorbits->msb-of-type$inline
         msb-of-type x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->msb-of-type-is-code-segment-descriptorbits

(defthm
 !code-segment-descriptorbits->msb-of-type-is-code-segment-descriptorbits
 (equal
     (!code-segment-descriptorbits->msb-of-type msb-of-type x)
     (change-code-segment-descriptorbits x
                                         :msb-of-type msb-of-type)))

Theorem: code-segment-descriptorbits->msb-of-type-of-!code-segment-descriptorbits->msb-of-type

(defthm
 code-segment-descriptorbits->msb-of-type-of-!code-segment-descriptorbits->msb-of-type
 (b* ((?new-x (!code-segment-descriptorbits->msb-of-type$inline
                   msb-of-type x)))
   (equal (code-segment-descriptorbits->msb-of-type new-x)
          (bfix msb-of-type))))

Theorem: !code-segment-descriptorbits->msb-of-type-equiv-under-mask

(defthm !code-segment-descriptorbits->msb-of-type-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->msb-of-type$inline
                    msb-of-type x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -8796093022209)))

Function: !code-segment-descriptorbits->s$inline

(defun !code-segment-descriptorbits->s$inline (s x)
 (declare (xargs :guard (and (bitp s)
                             (code-segment-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((s (mbe :logic (bfix s) :exec s))
       (x (code-segment-descriptorbits-fix x)))
    (part-install s x :width 1 :low 44))
  :exec
  (the (unsigned-byte 64)
       (logior (the (unsigned-byte 64)
                    (logand (the (unsigned-byte 64) x)
                            (the (signed-byte 46) -17592186044417)))
               (the (unsigned-byte 45)
                    (ash (the (unsigned-byte 1) s) 44))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->s

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->s
  (b* ((new-x (!code-segment-descriptorbits->s$inline s x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->s$inline-of-bfix-s

(defthm !code-segment-descriptorbits->s$inline-of-bfix-s
  (equal (!code-segment-descriptorbits->s$inline (bfix s)
                                                 x)
         (!code-segment-descriptorbits->s$inline s x)))

Theorem: !code-segment-descriptorbits->s$inline-bit-equiv-congruence-on-s

(defthm
   !code-segment-descriptorbits->s$inline-bit-equiv-congruence-on-s
  (implies
       (bit-equiv s s-equiv)
       (equal (!code-segment-descriptorbits->s$inline s x)
              (!code-segment-descriptorbits->s$inline s-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->s$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->s$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->s$inline
             s (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->s$inline s x)))

Theorem: !code-segment-descriptorbits->s$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->s$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->s$inline s x)
             (!code-segment-descriptorbits->s$inline s x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->s-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->s-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->s s x)
         (change-code-segment-descriptorbits x
                                             :s s)))

Theorem: code-segment-descriptorbits->s-of-!code-segment-descriptorbits->s

(defthm
  code-segment-descriptorbits->s-of-!code-segment-descriptorbits->s
  (b* ((?new-x (!code-segment-descriptorbits->s$inline s x)))
    (equal (code-segment-descriptorbits->s new-x)
           (bfix s))))

Theorem: !code-segment-descriptorbits->s-equiv-under-mask

(defthm !code-segment-descriptorbits->s-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->s$inline s x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -17592186044417)))

Function: !code-segment-descriptorbits->dpl$inline

(defun !code-segment-descriptorbits->dpl$inline (dpl x)
  (declare (xargs :guard (and (2bits-p dpl)
                              (code-segment-descriptorbits-p x))))
  (mbe :logic
       (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
            (x (code-segment-descriptorbits-fix x)))
         (part-install dpl x :width 2 :low 45))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 48)
                                            -105553116266497)))
                          (the (unsigned-byte 47)
                               (ash (the (unsigned-byte 2) dpl)
                                    45))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->dpl

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->dpl
 (b* ((new-x (!code-segment-descriptorbits->dpl$inline dpl x)))
   (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->dpl$inline-of-2bits-fix-dpl

(defthm !code-segment-descriptorbits->dpl$inline-of-2bits-fix-dpl
  (equal (!code-segment-descriptorbits->dpl$inline (2bits-fix dpl)
                                                   x)
         (!code-segment-descriptorbits->dpl$inline dpl x)))

Theorem: !code-segment-descriptorbits->dpl$inline-2bits-equiv-congruence-on-dpl

(defthm
 !code-segment-descriptorbits->dpl$inline-2bits-equiv-congruence-on-dpl
 (implies
     (2bits-equiv dpl dpl-equiv)
     (equal (!code-segment-descriptorbits->dpl$inline dpl x)
            (!code-segment-descriptorbits->dpl$inline dpl-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->dpl$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->dpl$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->dpl$inline
             dpl (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->dpl$inline dpl x)))

Theorem: !code-segment-descriptorbits->dpl$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->dpl$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
     (code-segment-descriptorbits-equiv x x-equiv)
     (equal (!code-segment-descriptorbits->dpl$inline dpl x)
            (!code-segment-descriptorbits->dpl$inline dpl x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->dpl-is-code-segment-descriptorbits

(defthm
   !code-segment-descriptorbits->dpl-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->dpl dpl x)
         (change-code-segment-descriptorbits x
                                             :dpl dpl)))

Theorem: code-segment-descriptorbits->dpl-of-!code-segment-descriptorbits->dpl

(defthm
 code-segment-descriptorbits->dpl-of-!code-segment-descriptorbits->dpl
 (b* ((?new-x (!code-segment-descriptorbits->dpl$inline dpl x)))
   (equal (code-segment-descriptorbits->dpl new-x)
          (2bits-fix dpl))))

Theorem: !code-segment-descriptorbits->dpl-equiv-under-mask

(defthm !code-segment-descriptorbits->dpl-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->dpl$inline dpl x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -105553116266497)))

Function: !code-segment-descriptorbits->p$inline

(defun !code-segment-descriptorbits->p$inline (p x)
 (declare (xargs :guard (and (bitp p)
                             (code-segment-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((p (mbe :logic (bfix p) :exec p))
          (x (code-segment-descriptorbits-fix x)))
       (part-install p x :width 1 :low 47))
     :exec (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64)
                             (logand (the (unsigned-byte 64) x)
                                     (the (signed-byte 49)
                                          -140737488355329)))
                        (the (unsigned-byte 48)
                             (ash (the (unsigned-byte 1) p) 47))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->p

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

Theorem: !code-segment-descriptorbits->p$inline-of-bfix-p

(defthm !code-segment-descriptorbits->p$inline-of-bfix-p
  (equal (!code-segment-descriptorbits->p$inline (bfix p)
                                                 x)
         (!code-segment-descriptorbits->p$inline p x)))

Theorem: !code-segment-descriptorbits->p$inline-bit-equiv-congruence-on-p

(defthm
   !code-segment-descriptorbits->p$inline-bit-equiv-congruence-on-p
  (implies
       (bit-equiv p p-equiv)
       (equal (!code-segment-descriptorbits->p$inline p x)
              (!code-segment-descriptorbits->p$inline p-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->p$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->p$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->p$inline
             p (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->p$inline p x)))

Theorem: !code-segment-descriptorbits->p$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->p$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->p$inline p x)
             (!code-segment-descriptorbits->p$inline p x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->p-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->p-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->p p x)
         (change-code-segment-descriptorbits x
                                             :p p)))

Theorem: code-segment-descriptorbits->p-of-!code-segment-descriptorbits->p

(defthm
  code-segment-descriptorbits->p-of-!code-segment-descriptorbits->p
  (b* ((?new-x (!code-segment-descriptorbits->p$inline p x)))
    (equal (code-segment-descriptorbits->p new-x)
           (bfix p))))

Theorem: !code-segment-descriptorbits->p-equiv-under-mask

(defthm !code-segment-descriptorbits->p-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->p$inline p x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -140737488355329)))

Function: !code-segment-descriptorbits->limit19-16$inline

(defun !code-segment-descriptorbits->limit19-16$inline
       (limit19-16 x)
 (declare (xargs :guard (and (4bits-p limit19-16)
                             (code-segment-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((limit19-16 (mbe :logic (4bits-fix limit19-16)
                           :exec limit19-16))
          (x (code-segment-descriptorbits-fix x)))
       (part-install limit19-16 x
                     :width 4
                     :low 48))
     :exec (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64)
                             (logand (the (unsigned-byte 64) x)
                                     (the (signed-byte 53)
                                          -4222124650659841)))
                        (the (unsigned-byte 52)
                             (ash (the (unsigned-byte 4) limit19-16)
                                  48))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->limit19-16

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->limit19-16
 (b*
  ((new-x
    (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)))
  (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->limit19-16$inline-of-4bits-fix-limit19-16

(defthm
 !code-segment-descriptorbits->limit19-16$inline-of-4bits-fix-limit19-16
 (equal
    (!code-segment-descriptorbits->limit19-16$inline
         (4bits-fix limit19-16)
         x)
    (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)))

Theorem: !code-segment-descriptorbits->limit19-16$inline-4bits-equiv-congruence-on-limit19-16

(defthm
 !code-segment-descriptorbits->limit19-16$inline-4bits-equiv-congruence-on-limit19-16
 (implies
  (4bits-equiv limit19-16 limit19-16-equiv)
  (equal
      (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)
      (!code-segment-descriptorbits->limit19-16$inline
           limit19-16-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->limit19-16$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->limit19-16$inline-of-code-segment-descriptorbits-fix-x
 (equal
    (!code-segment-descriptorbits->limit19-16$inline
         limit19-16
         (code-segment-descriptorbits-fix x))
    (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)))

Theorem: !code-segment-descriptorbits->limit19-16$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->limit19-16$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (code-segment-descriptorbits-equiv x x-equiv)
  (equal
      (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)
      (!code-segment-descriptorbits->limit19-16$inline
           limit19-16 x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->limit19-16-is-code-segment-descriptorbits

(defthm
 !code-segment-descriptorbits->limit19-16-is-code-segment-descriptorbits
 (equal
      (!code-segment-descriptorbits->limit19-16 limit19-16 x)
      (change-code-segment-descriptorbits x
                                          :limit19-16 limit19-16)))

Theorem: code-segment-descriptorbits->limit19-16-of-!code-segment-descriptorbits->limit19-16

(defthm
 code-segment-descriptorbits->limit19-16-of-!code-segment-descriptorbits->limit19-16
 (b*
  ((?new-x
    (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)))
  (equal (code-segment-descriptorbits->limit19-16 new-x)
         (4bits-fix limit19-16))))

Theorem: !code-segment-descriptorbits->limit19-16-equiv-under-mask

(defthm !code-segment-descriptorbits->limit19-16-equiv-under-mask
 (b*
  ((?new-x
    (!code-segment-descriptorbits->limit19-16$inline limit19-16 x)))
  (code-segment-descriptorbits-equiv-under-mask
       new-x x -4222124650659841)))

Function: !code-segment-descriptorbits->avl$inline

(defun !code-segment-descriptorbits->avl$inline (avl x)
  (declare (xargs :guard (and (bitp avl)
                              (code-segment-descriptorbits-p x))))
  (mbe :logic
       (b* ((avl (mbe :logic (bfix avl) :exec avl))
            (x (code-segment-descriptorbits-fix x)))
         (part-install avl x :width 1 :low 52))
       :exec (the (unsigned-byte 64)
                  (logior (the (unsigned-byte 64)
                               (logand (the (unsigned-byte 64) x)
                                       (the (signed-byte 54)
                                            -4503599627370497)))
                          (the (unsigned-byte 53)
                               (ash (the (unsigned-byte 1) avl)
                                    52))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->avl

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->avl
 (b* ((new-x (!code-segment-descriptorbits->avl$inline avl x)))
   (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->avl$inline-of-bfix-avl

(defthm !code-segment-descriptorbits->avl$inline-of-bfix-avl
  (equal (!code-segment-descriptorbits->avl$inline (bfix avl)
                                                   x)
         (!code-segment-descriptorbits->avl$inline avl x)))

Theorem: !code-segment-descriptorbits->avl$inline-bit-equiv-congruence-on-avl

(defthm
 !code-segment-descriptorbits->avl$inline-bit-equiv-congruence-on-avl
 (implies
     (bit-equiv avl avl-equiv)
     (equal (!code-segment-descriptorbits->avl$inline avl x)
            (!code-segment-descriptorbits->avl$inline avl-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->avl$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->avl$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->avl$inline
             avl (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->avl$inline avl x)))

Theorem: !code-segment-descriptorbits->avl$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->avl$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
     (code-segment-descriptorbits-equiv x x-equiv)
     (equal (!code-segment-descriptorbits->avl$inline avl x)
            (!code-segment-descriptorbits->avl$inline avl x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->avl-is-code-segment-descriptorbits

(defthm
   !code-segment-descriptorbits->avl-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->avl avl x)
         (change-code-segment-descriptorbits x
                                             :avl avl)))

Theorem: code-segment-descriptorbits->avl-of-!code-segment-descriptorbits->avl

(defthm
 code-segment-descriptorbits->avl-of-!code-segment-descriptorbits->avl
 (b* ((?new-x (!code-segment-descriptorbits->avl$inline avl x)))
   (equal (code-segment-descriptorbits->avl new-x)
          (bfix avl))))

Theorem: !code-segment-descriptorbits->avl-equiv-under-mask

(defthm !code-segment-descriptorbits->avl-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->avl$inline avl x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -4503599627370497)))

Function: !code-segment-descriptorbits->l$inline

(defun !code-segment-descriptorbits->l$inline (l x)
 (declare (xargs :guard (and (bitp l)
                             (code-segment-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((l (mbe :logic (bfix l) :exec l))
          (x (code-segment-descriptorbits-fix x)))
       (part-install l x :width 1 :low 53))
     :exec (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64)
                             (logand (the (unsigned-byte 64) x)
                                     (the (signed-byte 55)
                                          -9007199254740993)))
                        (the (unsigned-byte 54)
                             (ash (the (unsigned-byte 1) l) 53))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->l

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->l
  (b* ((new-x (!code-segment-descriptorbits->l$inline l x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->l$inline-of-bfix-l

(defthm !code-segment-descriptorbits->l$inline-of-bfix-l
  (equal (!code-segment-descriptorbits->l$inline (bfix l)
                                                 x)
         (!code-segment-descriptorbits->l$inline l x)))

Theorem: !code-segment-descriptorbits->l$inline-bit-equiv-congruence-on-l

(defthm
   !code-segment-descriptorbits->l$inline-bit-equiv-congruence-on-l
  (implies
       (bit-equiv l l-equiv)
       (equal (!code-segment-descriptorbits->l$inline l x)
              (!code-segment-descriptorbits->l$inline l-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->l$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->l$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->l$inline
             l (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->l$inline l x)))

Theorem: !code-segment-descriptorbits->l$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->l$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->l$inline l x)
             (!code-segment-descriptorbits->l$inline l x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->l-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->l-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->l l x)
         (change-code-segment-descriptorbits x
                                             :l l)))

Theorem: code-segment-descriptorbits->l-of-!code-segment-descriptorbits->l

(defthm
  code-segment-descriptorbits->l-of-!code-segment-descriptorbits->l
  (b* ((?new-x (!code-segment-descriptorbits->l$inline l x)))
    (equal (code-segment-descriptorbits->l new-x)
           (bfix l))))

Theorem: !code-segment-descriptorbits->l-equiv-under-mask

(defthm !code-segment-descriptorbits->l-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->l$inline l x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -9007199254740993)))

Function: !code-segment-descriptorbits->d$inline

(defun !code-segment-descriptorbits->d$inline (d x)
 (declare (xargs :guard (and (bitp d)
                             (code-segment-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((d (mbe :logic (bfix d) :exec d))
          (x (code-segment-descriptorbits-fix x)))
       (part-install d x :width 1 :low 54))
     :exec (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64)
                             (logand (the (unsigned-byte 64) x)
                                     (the (signed-byte 56)
                                          -18014398509481985)))
                        (the (unsigned-byte 55)
                             (ash (the (unsigned-byte 1) d) 54))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->d

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->d
  (b* ((new-x (!code-segment-descriptorbits->d$inline d x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->d$inline-of-bfix-d

(defthm !code-segment-descriptorbits->d$inline-of-bfix-d
  (equal (!code-segment-descriptorbits->d$inline (bfix d)
                                                 x)
         (!code-segment-descriptorbits->d$inline d x)))

Theorem: !code-segment-descriptorbits->d$inline-bit-equiv-congruence-on-d

(defthm
   !code-segment-descriptorbits->d$inline-bit-equiv-congruence-on-d
  (implies
       (bit-equiv d d-equiv)
       (equal (!code-segment-descriptorbits->d$inline d x)
              (!code-segment-descriptorbits->d$inline d-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->d$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->d$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->d$inline
             d (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->d$inline d x)))

Theorem: !code-segment-descriptorbits->d$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->d$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->d$inline d x)
             (!code-segment-descriptorbits->d$inline d x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->d-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->d-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->d d x)
         (change-code-segment-descriptorbits x
                                             :d d)))

Theorem: code-segment-descriptorbits->d-of-!code-segment-descriptorbits->d

(defthm
  code-segment-descriptorbits->d-of-!code-segment-descriptorbits->d
  (b* ((?new-x (!code-segment-descriptorbits->d$inline d x)))
    (equal (code-segment-descriptorbits->d new-x)
           (bfix d))))

Theorem: !code-segment-descriptorbits->d-equiv-under-mask

(defthm !code-segment-descriptorbits->d-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->d$inline d x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -18014398509481985)))

Function: !code-segment-descriptorbits->g$inline

(defun !code-segment-descriptorbits->g$inline (g x)
 (declare (xargs :guard (and (bitp g)
                             (code-segment-descriptorbits-p x))))
 (mbe
     :logic
     (b* ((g (mbe :logic (bfix g) :exec g))
          (x (code-segment-descriptorbits-fix x)))
       (part-install g x :width 1 :low 55))
     :exec (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64)
                             (logand (the (unsigned-byte 64) x)
                                     (the (signed-byte 57)
                                          -36028797018963969)))
                        (the (unsigned-byte 56)
                             (ash (the (unsigned-byte 1) g) 55))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->g

(defthm
   code-segment-descriptorbits-p-of-!code-segment-descriptorbits->g
  (b* ((new-x (!code-segment-descriptorbits->g$inline g x)))
    (code-segment-descriptorbits-p new-x))
  :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->g$inline-of-bfix-g

(defthm !code-segment-descriptorbits->g$inline-of-bfix-g
  (equal (!code-segment-descriptorbits->g$inline (bfix g)
                                                 x)
         (!code-segment-descriptorbits->g$inline g x)))

Theorem: !code-segment-descriptorbits->g$inline-bit-equiv-congruence-on-g

(defthm
   !code-segment-descriptorbits->g$inline-bit-equiv-congruence-on-g
  (implies
       (bit-equiv g g-equiv)
       (equal (!code-segment-descriptorbits->g$inline g x)
              (!code-segment-descriptorbits->g$inline g-equiv x)))
  :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->g$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->g$inline-of-code-segment-descriptorbits-fix-x
 (equal (!code-segment-descriptorbits->g$inline
             g (code-segment-descriptorbits-fix x))
        (!code-segment-descriptorbits->g$inline g x)))

Theorem: !code-segment-descriptorbits->g$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->g$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
      (code-segment-descriptorbits-equiv x x-equiv)
      (equal (!code-segment-descriptorbits->g$inline g x)
             (!code-segment-descriptorbits->g$inline g x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->g-is-code-segment-descriptorbits

(defthm
     !code-segment-descriptorbits->g-is-code-segment-descriptorbits
  (equal (!code-segment-descriptorbits->g g x)
         (change-code-segment-descriptorbits x
                                             :g g)))

Theorem: code-segment-descriptorbits->g-of-!code-segment-descriptorbits->g

(defthm
  code-segment-descriptorbits->g-of-!code-segment-descriptorbits->g
  (b* ((?new-x (!code-segment-descriptorbits->g$inline g x)))
    (equal (code-segment-descriptorbits->g new-x)
           (bfix g))))

Theorem: !code-segment-descriptorbits->g-equiv-under-mask

(defthm !code-segment-descriptorbits->g-equiv-under-mask
  (b* ((?new-x (!code-segment-descriptorbits->g$inline g x)))
    (code-segment-descriptorbits-equiv-under-mask
         new-x x -36028797018963969)))

Function: !code-segment-descriptorbits->base31-24$inline

(defun !code-segment-descriptorbits->base31-24$inline (base31-24 x)
 (declare (xargs :guard (and (8bits-p base31-24)
                             (code-segment-descriptorbits-p x))))
 (mbe :logic
      (b* ((base31-24 (mbe :logic (8bits-fix base31-24)
                           :exec base31-24))
           (x (code-segment-descriptorbits-fix x)))
        (part-install base31-24 x
                      :width 8
                      :low 56))
      :exec (the (unsigned-byte 64)
                 (logior (the (unsigned-byte 64)
                              (logand (the (unsigned-byte 64) x)
                                      (the (signed-byte 65)
                                           -18374686479671623681)))
                         (the (unsigned-byte 64)
                              (ash (the (unsigned-byte 8) base31-24)
                                   56))))))

Theorem: code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base31-24

(defthm
 code-segment-descriptorbits-p-of-!code-segment-descriptorbits->base31-24
 (b*
  ((new-x
      (!code-segment-descriptorbits->base31-24$inline base31-24 x)))
  (code-segment-descriptorbits-p new-x))
 :rule-classes :rewrite)

Theorem: !code-segment-descriptorbits->base31-24$inline-of-8bits-fix-base31-24

(defthm
 !code-segment-descriptorbits->base31-24$inline-of-8bits-fix-base31-24
 (equal
      (!code-segment-descriptorbits->base31-24$inline
           (8bits-fix base31-24)
           x)
      (!code-segment-descriptorbits->base31-24$inline base31-24 x)))

Theorem: !code-segment-descriptorbits->base31-24$inline-8bits-equiv-congruence-on-base31-24

(defthm
 !code-segment-descriptorbits->base31-24$inline-8bits-equiv-congruence-on-base31-24
 (implies
   (8bits-equiv base31-24 base31-24-equiv)
   (equal
        (!code-segment-descriptorbits->base31-24$inline base31-24 x)
        (!code-segment-descriptorbits->base31-24$inline
             base31-24-equiv x)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->base31-24$inline-of-code-segment-descriptorbits-fix-x

(defthm
 !code-segment-descriptorbits->base31-24$inline-of-code-segment-descriptorbits-fix-x
 (equal
      (!code-segment-descriptorbits->base31-24$inline
           base31-24
           (code-segment-descriptorbits-fix x))
      (!code-segment-descriptorbits->base31-24$inline base31-24 x)))

Theorem: !code-segment-descriptorbits->base31-24$inline-code-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !code-segment-descriptorbits->base31-24$inline-code-segment-descriptorbits-equiv-congruence-on-x
 (implies
   (code-segment-descriptorbits-equiv x x-equiv)
   (equal
        (!code-segment-descriptorbits->base31-24$inline base31-24 x)
        (!code-segment-descriptorbits->base31-24$inline
             base31-24 x-equiv)))
 :rule-classes :congruence)

Theorem: !code-segment-descriptorbits->base31-24-is-code-segment-descriptorbits

(defthm
 !code-segment-descriptorbits->base31-24-is-code-segment-descriptorbits
 (equal (!code-segment-descriptorbits->base31-24 base31-24 x)
        (change-code-segment-descriptorbits x
                                            :base31-24 base31-24)))

Theorem: code-segment-descriptorbits->base31-24-of-!code-segment-descriptorbits->base31-24

(defthm
 code-segment-descriptorbits->base31-24-of-!code-segment-descriptorbits->base31-24
 (b*
  ((?new-x
      (!code-segment-descriptorbits->base31-24$inline base31-24 x)))
  (equal (code-segment-descriptorbits->base31-24 new-x)
         (8bits-fix base31-24))))

Theorem: !code-segment-descriptorbits->base31-24-equiv-under-mask

(defthm !code-segment-descriptorbits->base31-24-equiv-under-mask
 (b*
  ((?new-x
      (!code-segment-descriptorbits->base31-24$inline base31-24 x)))
  (code-segment-descriptorbits-equiv-under-mask
       new-x x 72057594037927935)))

Function: code-segment-descriptorbits-debug

(defun code-segment-descriptorbits-debug (x)
 (declare (xargs :guard (code-segment-descriptorbits-p x)))
 (let ((__function__ 'code-segment-descriptorbits-debug))
  (declare (ignorable __function__))
  (b* (((code-segment-descriptorbits x)))
   (cons
    (cons 'limit15-0 x.limit15-0)
    (cons
     (cons 'base15-0 x.base15-0)
     (cons
      (cons 'base23-16 x.base23-16)
      (cons
       (cons 'a x.a)
       (cons
        (cons 'r x.r)
        (cons
         (cons 'c x.c)
         (cons
          (cons 'msb-of-type x.msb-of-type)
          (cons
           (cons 's x.s)
           (cons
            (cons 'dpl x.dpl)
            (cons
             (cons 'p x.p)
             (cons
              (cons 'limit19-16 x.limit19-16)
              (cons
               (cons 'avl x.avl)
               (cons (cons 'l x.l)
                     (cons (cons 'd x.d)
                           (cons (cons 'g x.g)
                                 (cons (cons 'base31-24 x.base31-24)
                                       nil)))))))))))))))))))

Subtopics

Code-segment-descriptorbits-p: Recognizer for code-segment-descriptorbits bit structures.
!code-segment-descriptorbits->msb-of-type: Update the |X86ISA|::|MSB-OF-TYPE| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->limit19-16: Update the |X86ISA|::|LIMIT19-16| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->base31-24: Update the |X86ISA|::|BASE31-24| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->limit15-0: Update the |X86ISA|::|LIMIT15-0| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->base23-16: Update the |X86ISA|::|BASE23-16| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->base15-0: Update the |X86ISA|::|BASE15-0| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->dpl: Update the |X86ISA|::|DPL| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->avl: Update the |X86ISA|::|AVL| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->s: Update the |X86ISA|::|S| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->r: Update the |ACL2|::|R| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->p: Update the |ACL2|::|P| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->l: Update the |ACL2|::|L| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->g: Update the |X86ISA|::|G| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->d: Update the |ACL2|::|D| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->c: Update the |ACL2|::|C| field of a code-segment-descriptorbits bit structure.
!code-segment-descriptorbits->a: Update the |ACL2|::|A| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->msb-of-type: Access the |X86ISA|::|MSB-OF-TYPE| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->limit19-16: Access the |X86ISA|::|LIMIT19-16| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits-fix: Fixing function for code-segment-descriptorbits bit structures.
Code-segment-descriptorbits->limit15-0: Access the |X86ISA|::|LIMIT15-0| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->base31-24: Access the |X86ISA|::|BASE31-24| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->base23-16: Access the |X86ISA|::|BASE23-16| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->base15-0: Access the |X86ISA|::|BASE15-0| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->dpl: Access the |X86ISA|::|DPL| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->s: Access the |X86ISA|::|S| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->r: Access the |ACL2|::|R| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->p: Access the |ACL2|::|P| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->l: Access the |ACL2|::|L| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->g: Access the |X86ISA|::|G| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->d: Access the |ACL2|::|D| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->c: Access the |ACL2|::|C| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->avl: Access the |X86ISA|::|AVL| field of a code-segment-descriptorbits bit structure.
Code-segment-descriptorbits->a: Access the |ACL2|::|A| field of a code-segment-descriptorbits bit structure.