		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Data-segment-descriptor-attributesbits

Subset of data-segment-descriptorBits.

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

Fields

a — bit
w — bit
e — bit
msb-of-type — bit
s — bit
dpl — 2bits
p — bit
avl — bit
l — bit
d/b — bit
g — bit
unknownbits — 4bits

Definitions and Theorems

Function: data-segment-descriptor-attributesbits-p

(defun data-segment-descriptor-attributesbits-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'data-segment-descriptor-attributesbits-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 16 x)
         :exec (and (natp x) (< x 65536)))))

Theorem: data-segment-descriptor-attributesbits-p-when-unsigned-byte-p

(defthm
      data-segment-descriptor-attributesbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 16 x)
           (data-segment-descriptor-attributesbits-p x)))

Theorem: unsigned-byte-p-when-data-segment-descriptor-attributesbits-p

(defthm
      unsigned-byte-p-when-data-segment-descriptor-attributesbits-p
  (implies (data-segment-descriptor-attributesbits-p x)
           (unsigned-byte-p 16 x)))

Theorem: data-segment-descriptor-attributesbits-p-compound-recognizer

(defthm data-segment-descriptor-attributesbits-p-compound-recognizer
  (implies (data-segment-descriptor-attributesbits-p x)
           (natp x))
  :rule-classes :compound-recognizer)

Function: data-segment-descriptor-attributesbits-fix

(defun data-segment-descriptor-attributesbits-fix (x)
  (declare
       (xargs :guard (data-segment-descriptor-attributesbits-p x)))
  (let ((__function__ 'data-segment-descriptor-attributesbits-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 16 x) :exec x)))

Theorem: data-segment-descriptor-attributesbits-p-of-data-segment-descriptor-attributesbits-fix

(defthm
 data-segment-descriptor-attributesbits-p-of-data-segment-descriptor-attributesbits-fix
 (b* ((fty::fixed (data-segment-descriptor-attributesbits-fix x)))
   (data-segment-descriptor-attributesbits-p fty::fixed))
 :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits-fix-when-data-segment-descriptor-attributesbits-p

(defthm
 data-segment-descriptor-attributesbits-fix-when-data-segment-descriptor-attributesbits-p
 (implies (data-segment-descriptor-attributesbits-p x)
          (equal (data-segment-descriptor-attributesbits-fix x)
                 x)))

Function: data-segment-descriptor-attributesbits-equiv$inline

(defun data-segment-descriptor-attributesbits-equiv$inline (x y)
 (declare
  (xargs :guard (and (data-segment-descriptor-attributesbits-p x)
                     (data-segment-descriptor-attributesbits-p y))))
 (equal (data-segment-descriptor-attributesbits-fix x)
        (data-segment-descriptor-attributesbits-fix y)))

Theorem: data-segment-descriptor-attributesbits-equiv-is-an-equivalence

(defthm
     data-segment-descriptor-attributesbits-equiv-is-an-equivalence
 (and
   (booleanp (data-segment-descriptor-attributesbits-equiv x y))
   (data-segment-descriptor-attributesbits-equiv x x)
   (implies (data-segment-descriptor-attributesbits-equiv x y)
            (data-segment-descriptor-attributesbits-equiv y x))
   (implies (and (data-segment-descriptor-attributesbits-equiv x y)
                 (data-segment-descriptor-attributesbits-equiv y z))
            (data-segment-descriptor-attributesbits-equiv x z)))
 :rule-classes (:equivalence))

Theorem: data-segment-descriptor-attributesbits-equiv-implies-equal-data-segment-descriptor-attributesbits-fix-1

(defthm
 data-segment-descriptor-attributesbits-equiv-implies-equal-data-segment-descriptor-attributesbits-fix-1
 (implies
      (data-segment-descriptor-attributesbits-equiv x x-equiv)
      (equal (data-segment-descriptor-attributesbits-fix x)
             (data-segment-descriptor-attributesbits-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: data-segment-descriptor-attributesbits-fix-under-data-segment-descriptor-attributesbits-equiv

(defthm
 data-segment-descriptor-attributesbits-fix-under-data-segment-descriptor-attributesbits-equiv
 (data-segment-descriptor-attributesbits-equiv
      (data-segment-descriptor-attributesbits-fix x)
      x)
 :rule-classes (:rewrite :rewrite-quoted-constant))

Function: data-segment-descriptor-attributesbits

(defun data-segment-descriptor-attributesbits
       (a w e msb-of-type
          s dpl p avl l d/b g unknownbits)
 (declare (xargs :guard (and (bitp a)
                             (bitp w)
                             (bitp e)
                             (bitp msb-of-type)
                             (bitp s)
                             (2bits-p dpl)
                             (bitp p)
                             (bitp avl)
                             (bitp l)
                             (bitp d/b)
                             (bitp g)
                             (4bits-p unknownbits))))
 (let ((__function__ 'data-segment-descriptor-attributesbits))
  (declare (ignorable __function__))
  (b* ((a (mbe :logic (bfix a) :exec a))
       (w (mbe :logic (bfix w) :exec w))
       (e (mbe :logic (bfix e) :exec e))
       (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))
       (avl (mbe :logic (bfix avl) :exec avl))
       (l (mbe :logic (bfix l) :exec l))
       (d/b (mbe :logic (bfix d/b) :exec d/b))
       (g (mbe :logic (bfix g) :exec g))
       (unknownbits (mbe :logic (4bits-fix unknownbits)
                         :exec unknownbits)))
   (logapp
    1 a
    (logapp
     1 w
     (logapp
      1 e
      (logapp
       1 msb-of-type
       (logapp
        1 s
        (logapp
         2 dpl
         (logapp
          1 p
          (logapp
               1 avl
               (logapp 1 l
                       (logapp 1 d/b
                               (logapp 1 g unknownbits))))))))))))))

Theorem: data-segment-descriptor-attributesbits-p-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits-p-of-data-segment-descriptor-attributesbits
 (b* ((data-segment-descriptor-attributesbits
           (data-segment-descriptor-attributesbits
                a w e msb-of-type
                s dpl p avl l d/b g unknownbits)))
   (data-segment-descriptor-attributesbits-p
        data-segment-descriptor-attributesbits))
 :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits-of-bfix-a

(defthm data-segment-descriptor-attributesbits-of-bfix-a
  (equal (data-segment-descriptor-attributesbits
              (bfix a)
              w e msb-of-type
              s dpl p avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-a

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-a
  (implies (bit-equiv a a-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a-equiv w e msb-of-type
                       s dpl p avl l d/b g unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-w

(defthm data-segment-descriptor-attributesbits-of-bfix-w
  (equal (data-segment-descriptor-attributesbits
              a (bfix w)
              e msb-of-type
              s dpl p avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-w

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-w
  (implies (bit-equiv w w-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a w-equiv e msb-of-type
                       s dpl p avl l d/b g unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-e

(defthm data-segment-descriptor-attributesbits-of-bfix-e
  (equal (data-segment-descriptor-attributesbits
              a w (bfix e)
              msb-of-type
              s dpl p avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-e

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-e
  (implies (bit-equiv e e-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a w e-equiv msb-of-type
                       s dpl p avl l d/b g unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-msb-of-type

(defthm data-segment-descriptor-attributesbits-of-bfix-msb-of-type
  (equal (data-segment-descriptor-attributesbits
              a w e (bfix msb-of-type)
              s dpl p avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-msb-of-type

(defthm
 data-segment-descriptor-attributesbits-bit-equiv-congruence-on-msb-of-type
 (implies (bit-equiv msb-of-type msb-of-type-equiv)
          (equal (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b g unknownbits)
                 (data-segment-descriptor-attributesbits
                      a w e msb-of-type-equiv
                      s dpl p avl l d/b g unknownbits)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-s

(defthm data-segment-descriptor-attributesbits-of-bfix-s
  (equal (data-segment-descriptor-attributesbits
              a w e msb-of-type (bfix s)
              dpl p avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-s

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-s
  (implies (bit-equiv s s-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s-equiv dpl p avl l d/b g unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-2bits-fix-dpl

(defthm data-segment-descriptor-attributesbits-of-2bits-fix-dpl
  (equal (data-segment-descriptor-attributesbits
              a w e msb-of-type s (2bits-fix dpl)
              p avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-2bits-equiv-congruence-on-dpl

(defthm
 data-segment-descriptor-attributesbits-2bits-equiv-congruence-on-dpl
 (implies (2bits-equiv dpl dpl-equiv)
          (equal (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b g unknownbits)
                 (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl-equiv p avl l d/b g unknownbits)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-p

(defthm data-segment-descriptor-attributesbits-of-bfix-p
  (equal (data-segment-descriptor-attributesbits
              a w e msb-of-type s dpl (bfix p)
              avl l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-p

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-p
  (implies (bit-equiv p p-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p-equiv avl l d/b g unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-avl

(defthm data-segment-descriptor-attributesbits-of-bfix-avl
  (equal (data-segment-descriptor-attributesbits
              a w e msb-of-type s dpl p (bfix avl)
              l d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-avl

(defthm
 data-segment-descriptor-attributesbits-bit-equiv-congruence-on-avl
 (implies (bit-equiv avl avl-equiv)
          (equal (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b g unknownbits)
                 (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl-equiv l d/b g unknownbits)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-l

(defthm data-segment-descriptor-attributesbits-of-bfix-l
  (equal (data-segment-descriptor-attributesbits
              a w e msb-of-type s dpl p avl (bfix l)
              d/b g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-l

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-l
  (implies (bit-equiv l l-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l-equiv d/b g unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-d/b

(defthm data-segment-descriptor-attributesbits-of-bfix-d/b
  (equal (data-segment-descriptor-attributesbits
              a
              w e msb-of-type s dpl p avl l (bfix d/b)
              g unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-d/b

(defthm
 data-segment-descriptor-attributesbits-bit-equiv-congruence-on-d/b
 (implies (bit-equiv d/b d/b-equiv)
          (equal (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b g unknownbits)
                 (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b-equiv g unknownbits)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-bfix-g

(defthm data-segment-descriptor-attributesbits-of-bfix-g
  (equal (data-segment-descriptor-attributesbits
              a w
              e msb-of-type s dpl p avl l d/b (bfix g)
              unknownbits)
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-bit-equiv-congruence-on-g

(defthm
   data-segment-descriptor-attributesbits-bit-equiv-congruence-on-g
  (implies (bit-equiv g g-equiv)
           (equal (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g unknownbits)
                  (data-segment-descriptor-attributesbits
                       a w e msb-of-type
                       s dpl p avl l d/b g-equiv unknownbits)))
  :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits-of-4bits-fix-unknownbits

(defthm
    data-segment-descriptor-attributesbits-of-4bits-fix-unknownbits
  (equal (data-segment-descriptor-attributesbits
              a w e msb-of-type s dpl
              p avl l d/b g (4bits-fix unknownbits))
         (data-segment-descriptor-attributesbits
              a w e msb-of-type
              s dpl p avl l d/b g unknownbits)))

Theorem: data-segment-descriptor-attributesbits-4bits-equiv-congruence-on-unknownbits

(defthm
 data-segment-descriptor-attributesbits-4bits-equiv-congruence-on-unknownbits
 (implies (4bits-equiv unknownbits unknownbits-equiv)
          (equal (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b g unknownbits)
                 (data-segment-descriptor-attributesbits
                      a w e msb-of-type
                      s dpl p avl l d/b g unknownbits-equiv)))
 :rule-classes :congruence)

Function: data-segment-descriptor-attributesbits-equiv-under-mask

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

Function: data-segment-descriptor-attributesbits->a$inline

(defun data-segment-descriptor-attributesbits->a$inline (x)
  (declare
       (xargs :guard (data-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (data-segment-descriptor-attributesbits-fix x)))
         (part-select x :low 0 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 16) x)))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->a

(defthm bitp-of-data-segment-descriptor-attributesbits->a
  (b* ((a (data-segment-descriptor-attributesbits->a$inline x)))
    (bitp a))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->a$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->a$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->a$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->a$inline x)))

Theorem: data-segment-descriptor-attributesbits->a$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->a$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->a$inline x)
        (data-segment-descriptor-attributesbits->a$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->a-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->a-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->a
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix a)))

Theorem: data-segment-descriptor-attributesbits->a-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->a-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 1) 0))
  (equal (data-segment-descriptor-attributesbits->a x)
         (data-segment-descriptor-attributesbits->a y))))

Function: data-segment-descriptor-attributesbits->w$inline

(defun data-segment-descriptor-attributesbits->w$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 1 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 15)
                            (ash (the (unsigned-byte 16) x) -1))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->w

(defthm bitp-of-data-segment-descriptor-attributesbits->w
  (b* ((w (data-segment-descriptor-attributesbits->w$inline x)))
    (bitp w))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->w$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->w$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->w$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->w$inline x)))

Theorem: data-segment-descriptor-attributesbits->w$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->w$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->w$inline x)
        (data-segment-descriptor-attributesbits->w$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->w-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->w-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->w
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix w)))

Theorem: data-segment-descriptor-attributesbits->w-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->w-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 2) 0))
  (equal (data-segment-descriptor-attributesbits->w x)
         (data-segment-descriptor-attributesbits->w y))))

Function: data-segment-descriptor-attributesbits->e$inline

(defun data-segment-descriptor-attributesbits->e$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 2 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 14)
                            (ash (the (unsigned-byte 16) x) -2))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->e

(defthm bitp-of-data-segment-descriptor-attributesbits->e
  (b* ((e (data-segment-descriptor-attributesbits->e$inline x)))
    (bitp e))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->e$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->e$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->e$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->e$inline x)))

Theorem: data-segment-descriptor-attributesbits->e$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->e$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->e$inline x)
        (data-segment-descriptor-attributesbits->e$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->e-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->e-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->e
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix e)))

Theorem: data-segment-descriptor-attributesbits->e-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->e-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 4) 0))
  (equal (data-segment-descriptor-attributesbits->e x)
         (data-segment-descriptor-attributesbits->e y))))

Function: data-segment-descriptor-attributesbits->msb-of-type$inline

(defun data-segment-descriptor-attributesbits->msb-of-type$inline
       (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 3 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 13)
                            (ash (the (unsigned-byte 16) x) -3))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->msb-of-type

(defthm bitp-of-data-segment-descriptor-attributesbits->msb-of-type
 (b*
  ((msb-of-type
    (data-segment-descriptor-attributesbits->msb-of-type$inline x)))
  (bitp msb-of-type))
 :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->msb-of-type$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->msb-of-type$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal
    (data-segment-descriptor-attributesbits->msb-of-type$inline
         (data-segment-descriptor-attributesbits-fix x))
    (data-segment-descriptor-attributesbits->msb-of-type$inline x)))

Theorem: data-segment-descriptor-attributesbits->msb-of-type$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

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

Theorem: data-segment-descriptor-attributesbits->msb-of-type-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->msb-of-type-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->msb-of-type
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix msb-of-type)))

Theorem: data-segment-descriptor-attributesbits->msb-of-type-of-write-with-mask

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

Function: data-segment-descriptor-attributesbits->s$inline

(defun data-segment-descriptor-attributesbits->s$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 4 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 12)
                            (ash (the (unsigned-byte 16) x) -4))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->s

(defthm bitp-of-data-segment-descriptor-attributesbits->s
  (b* ((s (data-segment-descriptor-attributesbits->s$inline x)))
    (bitp s))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->s$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->s$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->s$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->s$inline x)))

Theorem: data-segment-descriptor-attributesbits->s$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->s$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->s$inline x)
        (data-segment-descriptor-attributesbits->s$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->s-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->s-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->s
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix s)))

Theorem: data-segment-descriptor-attributesbits->s-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->s-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 16)
              0))
  (equal (data-segment-descriptor-attributesbits->s x)
         (data-segment-descriptor-attributesbits->s y))))

Function: data-segment-descriptor-attributesbits->dpl$inline

(defun data-segment-descriptor-attributesbits->dpl$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 5 :width 2))
    :exec (the (unsigned-byte 2)
               (logand (the (unsigned-byte 2) 3)
                       (the (unsigned-byte 11)
                            (ash (the (unsigned-byte 16) x) -5))))))

Theorem: 2bits-p-of-data-segment-descriptor-attributesbits->dpl

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

Theorem: data-segment-descriptor-attributesbits->dpl$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->dpl$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->dpl$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->dpl$inline x)))

Theorem: data-segment-descriptor-attributesbits->dpl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->dpl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
      (data-segment-descriptor-attributesbits->dpl$inline x)
      (data-segment-descriptor-attributesbits->dpl$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->dpl-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->dpl-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->dpl
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (2bits-fix dpl)))

Theorem: data-segment-descriptor-attributesbits->dpl-of-write-with-mask

(defthm
     data-segment-descriptor-attributesbits->dpl-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 96)
              0))
  (equal (data-segment-descriptor-attributesbits->dpl x)
         (data-segment-descriptor-attributesbits->dpl y))))

Function: data-segment-descriptor-attributesbits->p$inline

(defun data-segment-descriptor-attributesbits->p$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 7 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 9)
                            (ash (the (unsigned-byte 16) x) -7))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->p

(defthm bitp-of-data-segment-descriptor-attributesbits->p
  (b* ((p (data-segment-descriptor-attributesbits->p$inline x)))
    (bitp p))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->p$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->p$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->p$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->p$inline x)))

Theorem: data-segment-descriptor-attributesbits->p$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->p$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->p$inline x)
        (data-segment-descriptor-attributesbits->p$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->p-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->p-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->p
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix p)))

Theorem: data-segment-descriptor-attributesbits->p-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->p-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 128)
              0))
  (equal (data-segment-descriptor-attributesbits->p x)
         (data-segment-descriptor-attributesbits->p y))))

Function: data-segment-descriptor-attributesbits->avl$inline

(defun data-segment-descriptor-attributesbits->avl$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 8 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 8)
                            (ash (the (unsigned-byte 16) x) -8))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->avl

(defthm bitp-of-data-segment-descriptor-attributesbits->avl
  (b* ((avl (data-segment-descriptor-attributesbits->avl$inline x)))
    (bitp avl))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->avl$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->avl$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->avl$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->avl$inline x)))

Theorem: data-segment-descriptor-attributesbits->avl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->avl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
      (data-segment-descriptor-attributesbits->avl$inline x)
      (data-segment-descriptor-attributesbits->avl$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->avl-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->avl-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->avl
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix avl)))

Theorem: data-segment-descriptor-attributesbits->avl-of-write-with-mask

(defthm
     data-segment-descriptor-attributesbits->avl-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 256)
              0))
  (equal (data-segment-descriptor-attributesbits->avl x)
         (data-segment-descriptor-attributesbits->avl y))))

Function: data-segment-descriptor-attributesbits->l$inline

(defun data-segment-descriptor-attributesbits->l$inline (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (data-segment-descriptor-attributesbits-fix x)))
      (part-select x :low 9 :width 1))
    :exec (the (unsigned-byte 1)
               (logand (the (unsigned-byte 1) 1)
                       (the (unsigned-byte 7)
                            (ash (the (unsigned-byte 16) x) -9))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->l

(defthm bitp-of-data-segment-descriptor-attributesbits->l
  (b* ((l (data-segment-descriptor-attributesbits->l$inline x)))
    (bitp l))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->l$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->l$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->l$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->l$inline x)))

Theorem: data-segment-descriptor-attributesbits->l$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->l$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->l$inline x)
        (data-segment-descriptor-attributesbits->l$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->l-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->l-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->l
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix l)))

Theorem: data-segment-descriptor-attributesbits->l-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->l-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 512)
              0))
  (equal (data-segment-descriptor-attributesbits->l x)
         (data-segment-descriptor-attributesbits->l y))))

Function: data-segment-descriptor-attributesbits->d/b$inline

(defun data-segment-descriptor-attributesbits->d/b$inline (x)
  (declare
       (xargs :guard (data-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (data-segment-descriptor-attributesbits-fix x)))
         (part-select x :low 10 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 16) x)
                                    -10))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->d/b

(defthm bitp-of-data-segment-descriptor-attributesbits->d/b
  (b* ((d/b (data-segment-descriptor-attributesbits->d/b$inline x)))
    (bitp d/b))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->d/b$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->d/b$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->d/b$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->d/b$inline x)))

Theorem: data-segment-descriptor-attributesbits->d/b$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->d/b$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
      (data-segment-descriptor-attributesbits->d/b$inline x)
      (data-segment-descriptor-attributesbits->d/b$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->d/b-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->d/b-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->d/b
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix d/b)))

Theorem: data-segment-descriptor-attributesbits->d/b-of-write-with-mask

(defthm
     data-segment-descriptor-attributesbits->d/b-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 1024)
              0))
  (equal (data-segment-descriptor-attributesbits->d/b x)
         (data-segment-descriptor-attributesbits->d/b y))))

Function: data-segment-descriptor-attributesbits->g$inline

(defun data-segment-descriptor-attributesbits->g$inline (x)
  (declare
       (xargs :guard (data-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (data-segment-descriptor-attributesbits-fix x)))
         (part-select x :low 11 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 5)
                               (ash (the (unsigned-byte 16) x)
                                    -11))))))

Theorem: bitp-of-data-segment-descriptor-attributesbits->g

(defthm bitp-of-data-segment-descriptor-attributesbits->g
  (b* ((g (data-segment-descriptor-attributesbits->g$inline x)))
    (bitp g))
  :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->g$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->g$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (data-segment-descriptor-attributesbits->g$inline
             (data-segment-descriptor-attributesbits-fix x))
        (data-segment-descriptor-attributesbits->g$inline x)))

Theorem: data-segment-descriptor-attributesbits->g$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->g$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
   (data-segment-descriptor-attributesbits-equiv x x-equiv)
   (equal
        (data-segment-descriptor-attributesbits->g$inline x)
        (data-segment-descriptor-attributesbits->g$inline x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->g-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->g-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->g
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (bfix g)))

Theorem: data-segment-descriptor-attributesbits->g-of-write-with-mask

(defthm data-segment-descriptor-attributesbits->g-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 2048)
              0))
  (equal (data-segment-descriptor-attributesbits->g x)
         (data-segment-descriptor-attributesbits->g y))))

Function: data-segment-descriptor-attributesbits->unknownbits$inline

(defun data-segment-descriptor-attributesbits->unknownbits$inline
       (x)
  (declare
       (xargs :guard (data-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (data-segment-descriptor-attributesbits-fix x)))
         (part-select x :low 12 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 4)
                               (ash (the (unsigned-byte 16) x)
                                    -12))))))

Theorem: 4bits-p-of-data-segment-descriptor-attributesbits->unknownbits

(defthm
     4bits-p-of-data-segment-descriptor-attributesbits->unknownbits
 (b*
  ((unknownbits
    (data-segment-descriptor-attributesbits->unknownbits$inline x)))
  (4bits-p unknownbits))
 :rule-classes :rewrite)

Theorem: data-segment-descriptor-attributesbits->unknownbits$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 data-segment-descriptor-attributesbits->unknownbits$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal
    (data-segment-descriptor-attributesbits->unknownbits$inline
         (data-segment-descriptor-attributesbits-fix x))
    (data-segment-descriptor-attributesbits->unknownbits$inline x)))

Theorem: data-segment-descriptor-attributesbits->unknownbits$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 data-segment-descriptor-attributesbits->unknownbits$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
      (data-segment-descriptor-attributesbits->unknownbits$inline x)
      (data-segment-descriptor-attributesbits->unknownbits$inline
           x-equiv)))
 :rule-classes :congruence)

Theorem: data-segment-descriptor-attributesbits->unknownbits-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits->unknownbits-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits->unknownbits
             (data-segment-descriptor-attributesbits
                  a w e msb-of-type
                  s dpl p avl l d/b g unknownbits))
        (4bits-fix unknownbits)))

Theorem: data-segment-descriptor-attributesbits->unknownbits-of-write-with-mask

(defthm
 data-segment-descriptor-attributesbits->unknownbits-of-write-with-mask
 (implies
  (and (fty::bitstruct-read-over-write-hyps
            x
            data-segment-descriptor-attributesbits-equiv-under-mask)
       (data-segment-descriptor-attributesbits-equiv-under-mask
            x y fty::mask)
       (equal (logand (lognot fty::mask) 61440)
              0))
  (equal (data-segment-descriptor-attributesbits->unknownbits x)
         (data-segment-descriptor-attributesbits->unknownbits y))))

Theorem: data-segment-descriptor-attributesbits-fix-in-terms-of-data-segment-descriptor-attributesbits

(defthm
 data-segment-descriptor-attributesbits-fix-in-terms-of-data-segment-descriptor-attributesbits
 (equal (data-segment-descriptor-attributesbits-fix x)
        (change-data-segment-descriptor-attributesbits x)))

Function: !data-segment-descriptor-attributesbits->a$inline

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

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->a

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

Theorem: !data-segment-descriptor-attributesbits->a$inline-of-bfix-a

(defthm !data-segment-descriptor-attributesbits->a$inline-of-bfix-a
  (equal (!data-segment-descriptor-attributesbits->a$inline (bfix a)
                                                            x)
         (!data-segment-descriptor-attributesbits->a$inline a x)))

Theorem: !data-segment-descriptor-attributesbits->a$inline-bit-equiv-congruence-on-a

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

Theorem: !data-segment-descriptor-attributesbits->a$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->a$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->a$inline
             a
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->a$inline a x)))

Theorem: !data-segment-descriptor-attributesbits->a$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->a$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->a$inline a x)
     (!data-segment-descriptor-attributesbits->a$inline a x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->a-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->a-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->a a x)
        (change-data-segment-descriptor-attributesbits x
                                                       :a a)))

Theorem: data-segment-descriptor-attributesbits->a-of-!data-segment-descriptor-attributesbits->a

(defthm
 data-segment-descriptor-attributesbits->a-of-!data-segment-descriptor-attributesbits->a
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->a$inline a x)))
  (equal (data-segment-descriptor-attributesbits->a new-x)
         (bfix a))))

Theorem: !data-segment-descriptor-attributesbits->a-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->a-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->a$inline a x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -2)))

Function: !data-segment-descriptor-attributesbits->w$inline

(defun !data-segment-descriptor-attributesbits->w$inline (w x)
 (declare
  (xargs :guard (and (bitp w)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((w (mbe :logic (bfix w) :exec w))
           (x (data-segment-descriptor-attributesbits-fix x)))
        (part-install w x :width 1 :low 1))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 3) -3)))
                         (the (unsigned-byte 2)
                              (ash (the (unsigned-byte 1) w) 1))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->w

(defthm
 data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->w
 (b*
  ((new-x (!data-segment-descriptor-attributesbits->w$inline w x)))
  (data-segment-descriptor-attributesbits-p new-x))
 :rule-classes :rewrite)

Theorem: !data-segment-descriptor-attributesbits->w$inline-of-bfix-w

(defthm !data-segment-descriptor-attributesbits->w$inline-of-bfix-w
  (equal (!data-segment-descriptor-attributesbits->w$inline (bfix w)
                                                            x)
         (!data-segment-descriptor-attributesbits->w$inline w x)))

Theorem: !data-segment-descriptor-attributesbits->w$inline-bit-equiv-congruence-on-w

(defthm
 !data-segment-descriptor-attributesbits->w$inline-bit-equiv-congruence-on-w
 (implies
  (bit-equiv w w-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->w$inline w x)
     (!data-segment-descriptor-attributesbits->w$inline w-equiv x)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->w$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->w$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->w$inline
             w
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->w$inline w x)))

Theorem: !data-segment-descriptor-attributesbits->w$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->w$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->w$inline w x)
     (!data-segment-descriptor-attributesbits->w$inline w x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->w-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->w-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->w w x)
        (change-data-segment-descriptor-attributesbits x
                                                       :w w)))

Theorem: data-segment-descriptor-attributesbits->w-of-!data-segment-descriptor-attributesbits->w

(defthm
 data-segment-descriptor-attributesbits->w-of-!data-segment-descriptor-attributesbits->w
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->w$inline w x)))
  (equal (data-segment-descriptor-attributesbits->w new-x)
         (bfix w))))

Theorem: !data-segment-descriptor-attributesbits->w-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->w-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->w$inline w x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -3)))

Function: !data-segment-descriptor-attributesbits->e$inline

(defun !data-segment-descriptor-attributesbits->e$inline (e x)
 (declare
  (xargs :guard (and (bitp e)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((e (mbe :logic (bfix e) :exec e))
           (x (data-segment-descriptor-attributesbits-fix x)))
        (part-install e x :width 1 :low 2))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 4) -5)))
                         (the (unsigned-byte 3)
                              (ash (the (unsigned-byte 1) e) 2))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->e

(defthm
 data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->e
 (b*
  ((new-x (!data-segment-descriptor-attributesbits->e$inline e x)))
  (data-segment-descriptor-attributesbits-p new-x))
 :rule-classes :rewrite)

Theorem: !data-segment-descriptor-attributesbits->e$inline-of-bfix-e

(defthm !data-segment-descriptor-attributesbits->e$inline-of-bfix-e
  (equal (!data-segment-descriptor-attributesbits->e$inline (bfix e)
                                                            x)
         (!data-segment-descriptor-attributesbits->e$inline e x)))

Theorem: !data-segment-descriptor-attributesbits->e$inline-bit-equiv-congruence-on-e

(defthm
 !data-segment-descriptor-attributesbits->e$inline-bit-equiv-congruence-on-e
 (implies
  (bit-equiv e e-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->e$inline e x)
     (!data-segment-descriptor-attributesbits->e$inline e-equiv x)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->e$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->e$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->e$inline
             e
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->e$inline e x)))

Theorem: !data-segment-descriptor-attributesbits->e$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->e$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->e$inline e x)
     (!data-segment-descriptor-attributesbits->e$inline e x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->e-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->e-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->e e x)
        (change-data-segment-descriptor-attributesbits x
                                                       :e e)))

Theorem: data-segment-descriptor-attributesbits->e-of-!data-segment-descriptor-attributesbits->e

(defthm
 data-segment-descriptor-attributesbits->e-of-!data-segment-descriptor-attributesbits->e
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->e$inline e x)))
  (equal (data-segment-descriptor-attributesbits->e new-x)
         (bfix e))))

Theorem: !data-segment-descriptor-attributesbits->e-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->e-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->e$inline e x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -5)))

Function: !data-segment-descriptor-attributesbits->msb-of-type$inline

(defun !data-segment-descriptor-attributesbits->msb-of-type$inline
       (msb-of-type x)
 (declare
  (xargs :guard (and (bitp msb-of-type)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((msb-of-type (mbe :logic (bfix msb-of-type)
                           :exec msb-of-type))
         (x (data-segment-descriptor-attributesbits-fix x)))
      (part-install msb-of-type x
                    :width 1
                    :low 3))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 5) -9)))
                       (the (unsigned-byte 4)
                            (ash (the (unsigned-byte 1) msb-of-type)
                                 3))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->msb-of-type

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

Theorem: !data-segment-descriptor-attributesbits->msb-of-type$inline-of-bfix-msb-of-type

(defthm
 !data-segment-descriptor-attributesbits->msb-of-type$inline-of-bfix-msb-of-type
 (equal (!data-segment-descriptor-attributesbits->msb-of-type$inline
             (bfix msb-of-type)
             x)
        (!data-segment-descriptor-attributesbits->msb-of-type$inline
             msb-of-type x)))

Theorem: !data-segment-descriptor-attributesbits->msb-of-type$inline-bit-equiv-congruence-on-msb-of-type

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

Theorem: !data-segment-descriptor-attributesbits->msb-of-type$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->msb-of-type$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->msb-of-type$inline
             msb-of-type
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->msb-of-type$inline
             msb-of-type x)))

Theorem: !data-segment-descriptor-attributesbits->msb-of-type$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

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

Theorem: !data-segment-descriptor-attributesbits->msb-of-type-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->msb-of-type-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->msb-of-type
             msb-of-type x)
        (change-data-segment-descriptor-attributesbits
             x
             :msb-of-type msb-of-type)))

Theorem: data-segment-descriptor-attributesbits->msb-of-type-of-!data-segment-descriptor-attributesbits->msb-of-type

(defthm
 data-segment-descriptor-attributesbits->msb-of-type-of-!data-segment-descriptor-attributesbits->msb-of-type
 (b* ((?new-x (!data-segment-descriptor-attributesbits->msb-of-type$inline
                   msb-of-type x)))
  (equal (data-segment-descriptor-attributesbits->msb-of-type new-x)
         (bfix msb-of-type))))

Theorem: !data-segment-descriptor-attributesbits->msb-of-type-equiv-under-mask

(defthm
 !data-segment-descriptor-attributesbits->msb-of-type-equiv-under-mask
 (b* ((?new-x (!data-segment-descriptor-attributesbits->msb-of-type$inline
                   msb-of-type x)))
   (data-segment-descriptor-attributesbits-equiv-under-mask
        new-x x -9)))

Function: !data-segment-descriptor-attributesbits->s$inline

(defun !data-segment-descriptor-attributesbits->s$inline (s x)
 (declare
  (xargs :guard (and (bitp s)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((s (mbe :logic (bfix s) :exec s))
           (x (data-segment-descriptor-attributesbits-fix x)))
        (part-install s x :width 1 :low 4))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 6) -17)))
                         (the (unsigned-byte 5)
                              (ash (the (unsigned-byte 1) s) 4))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->s

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

Theorem: !data-segment-descriptor-attributesbits->s$inline-of-bfix-s

(defthm !data-segment-descriptor-attributesbits->s$inline-of-bfix-s
  (equal (!data-segment-descriptor-attributesbits->s$inline (bfix s)
                                                            x)
         (!data-segment-descriptor-attributesbits->s$inline s x)))

Theorem: !data-segment-descriptor-attributesbits->s$inline-bit-equiv-congruence-on-s

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

Theorem: !data-segment-descriptor-attributesbits->s$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->s$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->s$inline
             s
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->s$inline s x)))

Theorem: !data-segment-descriptor-attributesbits->s$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->s$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->s$inline s x)
     (!data-segment-descriptor-attributesbits->s$inline s x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->s-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->s-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->s s x)
        (change-data-segment-descriptor-attributesbits x
                                                       :s s)))

Theorem: data-segment-descriptor-attributesbits->s-of-!data-segment-descriptor-attributesbits->s

(defthm
 data-segment-descriptor-attributesbits->s-of-!data-segment-descriptor-attributesbits->s
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->s$inline s x)))
  (equal (data-segment-descriptor-attributesbits->s new-x)
         (bfix s))))

Theorem: !data-segment-descriptor-attributesbits->s-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->s-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->s$inline s x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -17)))

Function: !data-segment-descriptor-attributesbits->dpl$inline

(defun !data-segment-descriptor-attributesbits->dpl$inline (dpl x)
 (declare
  (xargs :guard (and (2bits-p dpl)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
         (x (data-segment-descriptor-attributesbits-fix x)))
      (part-install dpl x :width 2 :low 5))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 8) -97)))
                       (the (unsigned-byte 7)
                            (ash (the (unsigned-byte 2) dpl) 5))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->dpl

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

Theorem: !data-segment-descriptor-attributesbits->dpl$inline-of-2bits-fix-dpl

(defthm
 !data-segment-descriptor-attributesbits->dpl$inline-of-2bits-fix-dpl
 (equal
      (!data-segment-descriptor-attributesbits->dpl$inline
           (2bits-fix dpl)
           x)
      (!data-segment-descriptor-attributesbits->dpl$inline dpl x)))

Theorem: !data-segment-descriptor-attributesbits->dpl$inline-2bits-equiv-congruence-on-dpl

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

Theorem: !data-segment-descriptor-attributesbits->dpl$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->dpl$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal
      (!data-segment-descriptor-attributesbits->dpl$inline
           dpl
           (data-segment-descriptor-attributesbits-fix x))
      (!data-segment-descriptor-attributesbits->dpl$inline dpl x)))

Theorem: !data-segment-descriptor-attributesbits->dpl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->dpl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal (!data-segment-descriptor-attributesbits->dpl$inline dpl x)
         (!data-segment-descriptor-attributesbits->dpl$inline
              dpl x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->dpl-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->dpl-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->dpl dpl x)
        (change-data-segment-descriptor-attributesbits x
                                                       :dpl dpl)))

Theorem: data-segment-descriptor-attributesbits->dpl-of-!data-segment-descriptor-attributesbits->dpl

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

Theorem: !data-segment-descriptor-attributesbits->dpl-equiv-under-mask

(defthm
      !data-segment-descriptor-attributesbits->dpl-equiv-under-mask
 (b*
  ((?new-x
       (!data-segment-descriptor-attributesbits->dpl$inline dpl x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -97)))

Function: !data-segment-descriptor-attributesbits->p$inline

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

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->p

(defthm
 data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->p
 (b*
  ((new-x (!data-segment-descriptor-attributesbits->p$inline p x)))
  (data-segment-descriptor-attributesbits-p new-x))
 :rule-classes :rewrite)

Theorem: !data-segment-descriptor-attributesbits->p$inline-of-bfix-p

(defthm !data-segment-descriptor-attributesbits->p$inline-of-bfix-p
  (equal (!data-segment-descriptor-attributesbits->p$inline (bfix p)
                                                            x)
         (!data-segment-descriptor-attributesbits->p$inline p x)))

Theorem: !data-segment-descriptor-attributesbits->p$inline-bit-equiv-congruence-on-p

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

Theorem: !data-segment-descriptor-attributesbits->p$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->p$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->p$inline
             p
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->p$inline p x)))

Theorem: !data-segment-descriptor-attributesbits->p$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->p$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->p$inline p x)
     (!data-segment-descriptor-attributesbits->p$inline p x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->p-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->p-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->p p x)
        (change-data-segment-descriptor-attributesbits x
                                                       :p p)))

Theorem: data-segment-descriptor-attributesbits->p-of-!data-segment-descriptor-attributesbits->p

(defthm
 data-segment-descriptor-attributesbits->p-of-!data-segment-descriptor-attributesbits->p
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->p$inline p x)))
  (equal (data-segment-descriptor-attributesbits->p new-x)
         (bfix p))))

Theorem: !data-segment-descriptor-attributesbits->p-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->p-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->p$inline p x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -129)))

Function: !data-segment-descriptor-attributesbits->avl$inline

(defun !data-segment-descriptor-attributesbits->avl$inline (avl x)
 (declare
  (xargs :guard (and (bitp avl)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((avl (mbe :logic (bfix avl) :exec avl))
         (x (data-segment-descriptor-attributesbits-fix x)))
      (part-install avl x :width 1 :low 8))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 10) -257)))
                       (the (unsigned-byte 9)
                            (ash (the (unsigned-byte 1) avl) 8))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->avl

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

Theorem: !data-segment-descriptor-attributesbits->avl$inline-of-bfix-avl

(defthm
    !data-segment-descriptor-attributesbits->avl$inline-of-bfix-avl
 (equal
     (!data-segment-descriptor-attributesbits->avl$inline (bfix avl)
                                                          x)
     (!data-segment-descriptor-attributesbits->avl$inline avl x)))

Theorem: !data-segment-descriptor-attributesbits->avl$inline-bit-equiv-congruence-on-avl

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

Theorem: !data-segment-descriptor-attributesbits->avl$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->avl$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal
      (!data-segment-descriptor-attributesbits->avl$inline
           avl
           (data-segment-descriptor-attributesbits-fix x))
      (!data-segment-descriptor-attributesbits->avl$inline avl x)))

Theorem: !data-segment-descriptor-attributesbits->avl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->avl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal (!data-segment-descriptor-attributesbits->avl$inline avl x)
         (!data-segment-descriptor-attributesbits->avl$inline
              avl x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->avl-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->avl-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->avl avl x)
        (change-data-segment-descriptor-attributesbits x
                                                       :avl avl)))

Theorem: data-segment-descriptor-attributesbits->avl-of-!data-segment-descriptor-attributesbits->avl

(defthm
 data-segment-descriptor-attributesbits->avl-of-!data-segment-descriptor-attributesbits->avl
 (b*
  ((?new-x
       (!data-segment-descriptor-attributesbits->avl$inline avl x)))
  (equal (data-segment-descriptor-attributesbits->avl new-x)
         (bfix avl))))

Theorem: !data-segment-descriptor-attributesbits->avl-equiv-under-mask

(defthm
      !data-segment-descriptor-attributesbits->avl-equiv-under-mask
 (b*
  ((?new-x
       (!data-segment-descriptor-attributesbits->avl$inline avl x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -257)))

Function: !data-segment-descriptor-attributesbits->l$inline

(defun !data-segment-descriptor-attributesbits->l$inline (l x)
 (declare
  (xargs :guard (and (bitp l)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((l (mbe :logic (bfix l) :exec l))
           (x (data-segment-descriptor-attributesbits-fix x)))
        (part-install l x :width 1 :low 9))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 11) -513)))
                         (the (unsigned-byte 10)
                              (ash (the (unsigned-byte 1) l) 9))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->l

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

Theorem: !data-segment-descriptor-attributesbits->l$inline-of-bfix-l

(defthm !data-segment-descriptor-attributesbits->l$inline-of-bfix-l
  (equal (!data-segment-descriptor-attributesbits->l$inline (bfix l)
                                                            x)
         (!data-segment-descriptor-attributesbits->l$inline l x)))

Theorem: !data-segment-descriptor-attributesbits->l$inline-bit-equiv-congruence-on-l

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

Theorem: !data-segment-descriptor-attributesbits->l$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->l$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->l$inline
             l
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->l$inline l x)))

Theorem: !data-segment-descriptor-attributesbits->l$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->l$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->l$inline l x)
     (!data-segment-descriptor-attributesbits->l$inline l x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->l-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->l-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->l l x)
        (change-data-segment-descriptor-attributesbits x
                                                       :l l)))

Theorem: data-segment-descriptor-attributesbits->l-of-!data-segment-descriptor-attributesbits->l

(defthm
 data-segment-descriptor-attributesbits->l-of-!data-segment-descriptor-attributesbits->l
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->l$inline l x)))
  (equal (data-segment-descriptor-attributesbits->l new-x)
         (bfix l))))

Theorem: !data-segment-descriptor-attributesbits->l-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->l-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->l$inline l x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -513)))

Function: !data-segment-descriptor-attributesbits->d/b$inline

(defun !data-segment-descriptor-attributesbits->d/b$inline (d/b x)
 (declare
  (xargs :guard (and (bitp d/b)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((d/b (mbe :logic (bfix d/b) :exec d/b))
           (x (data-segment-descriptor-attributesbits-fix x)))
        (part-install d/b x :width 1 :low 10))
      :exec (the (unsigned-byte 16)
                 (logior (the (unsigned-byte 16)
                              (logand (the (unsigned-byte 16) x)
                                      (the (signed-byte 12) -1025)))
                         (the (unsigned-byte 11)
                              (ash (the (unsigned-byte 1) d/b)
                                   10))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->d/b

(defthm
 data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->d/b
 (b*
  ((new-x
       (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))
  (data-segment-descriptor-attributesbits-p new-x))
 :rule-classes :rewrite)

Theorem: !data-segment-descriptor-attributesbits->d/b$inline-of-bfix-d/b

(defthm
    !data-segment-descriptor-attributesbits->d/b$inline-of-bfix-d/b
 (equal
     (!data-segment-descriptor-attributesbits->d/b$inline (bfix d/b)
                                                          x)
     (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))

Theorem: !data-segment-descriptor-attributesbits->d/b$inline-bit-equiv-congruence-on-d/b

(defthm
 !data-segment-descriptor-attributesbits->d/b$inline-bit-equiv-congruence-on-d/b
 (implies
  (bit-equiv d/b d/b-equiv)
  (equal (!data-segment-descriptor-attributesbits->d/b$inline d/b x)
         (!data-segment-descriptor-attributesbits->d/b$inline
              d/b-equiv x)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->d/b$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->d/b$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal
      (!data-segment-descriptor-attributesbits->d/b$inline
           d/b
           (data-segment-descriptor-attributesbits-fix x))
      (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))

Theorem: !data-segment-descriptor-attributesbits->d/b$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->d/b$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal (!data-segment-descriptor-attributesbits->d/b$inline d/b x)
         (!data-segment-descriptor-attributesbits->d/b$inline
              d/b x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->d/b-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->d/b-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->d/b d/b x)
        (change-data-segment-descriptor-attributesbits x
                                                       :d/b d/b)))

Theorem: data-segment-descriptor-attributesbits->d/b-of-!data-segment-descriptor-attributesbits->d/b

(defthm
 data-segment-descriptor-attributesbits->d/b-of-!data-segment-descriptor-attributesbits->d/b
 (b*
  ((?new-x
       (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))
  (equal (data-segment-descriptor-attributesbits->d/b new-x)
         (bfix d/b))))

Theorem: !data-segment-descriptor-attributesbits->d/b-equiv-under-mask

(defthm
      !data-segment-descriptor-attributesbits->d/b-equiv-under-mask
 (b*
  ((?new-x
       (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -1025)))

Function: !data-segment-descriptor-attributesbits->g$inline

(defun !data-segment-descriptor-attributesbits->g$inline (g x)
 (declare
  (xargs :guard (and (bitp g)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe
     :logic
     (b* ((g (mbe :logic (bfix g) :exec g))
          (x (data-segment-descriptor-attributesbits-fix x)))
       (part-install g x :width 1 :low 11))
     :exec (the (unsigned-byte 16)
                (logior (the (unsigned-byte 16)
                             (logand (the (unsigned-byte 16) x)
                                     (the (signed-byte 13) -2049)))
                        (the (unsigned-byte 12)
                             (ash (the (unsigned-byte 1) g) 11))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->g

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

Theorem: !data-segment-descriptor-attributesbits->g$inline-of-bfix-g

(defthm !data-segment-descriptor-attributesbits->g$inline-of-bfix-g
  (equal (!data-segment-descriptor-attributesbits->g$inline (bfix g)
                                                            x)
         (!data-segment-descriptor-attributesbits->g$inline g x)))

Theorem: !data-segment-descriptor-attributesbits->g$inline-bit-equiv-congruence-on-g

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

Theorem: !data-segment-descriptor-attributesbits->g$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->g$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->g$inline
             g
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->g$inline g x)))

Theorem: !data-segment-descriptor-attributesbits->g$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->g$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies
  (data-segment-descriptor-attributesbits-equiv x x-equiv)
  (equal
     (!data-segment-descriptor-attributesbits->g$inline g x)
     (!data-segment-descriptor-attributesbits->g$inline g x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->g-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->g-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->g g x)
        (change-data-segment-descriptor-attributesbits x
                                                       :g g)))

Theorem: data-segment-descriptor-attributesbits->g-of-!data-segment-descriptor-attributesbits->g

(defthm
 data-segment-descriptor-attributesbits->g-of-!data-segment-descriptor-attributesbits->g
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->g$inline g x)))
  (equal (data-segment-descriptor-attributesbits->g new-x)
         (bfix g))))

Theorem: !data-segment-descriptor-attributesbits->g-equiv-under-mask

(defthm !data-segment-descriptor-attributesbits->g-equiv-under-mask
 (b*
  ((?new-x (!data-segment-descriptor-attributesbits->g$inline g x)))
  (data-segment-descriptor-attributesbits-equiv-under-mask
       new-x x -2049)))

Function: !data-segment-descriptor-attributesbits->unknownbits$inline

(defun !data-segment-descriptor-attributesbits->unknownbits$inline
       (unknownbits x)
 (declare
  (xargs :guard (and (4bits-p unknownbits)
                     (data-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((unknownbits (mbe :logic (4bits-fix unknownbits)
                           :exec unknownbits))
         (x (data-segment-descriptor-attributesbits-fix x)))
      (part-install unknownbits x
                    :width 4
                    :low 12))
    :exec (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16)
                            (logand (the (unsigned-byte 16) x)
                                    (the (signed-byte 17) -61441)))
                       (the (unsigned-byte 16)
                            (ash (the (unsigned-byte 4) unknownbits)
                                 12))))))

Theorem: data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->unknownbits

(defthm
 data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->unknownbits
 (b* ((new-x (!data-segment-descriptor-attributesbits->unknownbits$inline
                  unknownbits x)))
   (data-segment-descriptor-attributesbits-p new-x))
 :rule-classes :rewrite)

Theorem: !data-segment-descriptor-attributesbits->unknownbits$inline-of-4bits-fix-unknownbits

(defthm
 !data-segment-descriptor-attributesbits->unknownbits$inline-of-4bits-fix-unknownbits
 (equal (!data-segment-descriptor-attributesbits->unknownbits$inline
             (4bits-fix unknownbits)
             x)
        (!data-segment-descriptor-attributesbits->unknownbits$inline
             unknownbits x)))

Theorem: !data-segment-descriptor-attributesbits->unknownbits$inline-4bits-equiv-congruence-on-unknownbits

(defthm
 !data-segment-descriptor-attributesbits->unknownbits$inline-4bits-equiv-congruence-on-unknownbits
 (implies (4bits-equiv unknownbits unknownbits-equiv)
          (equal (!data-segment-descriptor-attributesbits->unknownbits$inline
                      unknownbits x)
                 (!data-segment-descriptor-attributesbits->unknownbits$inline
                      unknownbits-equiv x)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->unknownbits$inline-of-data-segment-descriptor-attributesbits-fix-x

(defthm
 !data-segment-descriptor-attributesbits->unknownbits$inline-of-data-segment-descriptor-attributesbits-fix-x
 (equal (!data-segment-descriptor-attributesbits->unknownbits$inline
             unknownbits
             (data-segment-descriptor-attributesbits-fix x))
        (!data-segment-descriptor-attributesbits->unknownbits$inline
             unknownbits x)))

Theorem: !data-segment-descriptor-attributesbits->unknownbits$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x

(defthm
 !data-segment-descriptor-attributesbits->unknownbits$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x
 (implies (data-segment-descriptor-attributesbits-equiv x x-equiv)
          (equal (!data-segment-descriptor-attributesbits->unknownbits$inline
                      unknownbits x)
                 (!data-segment-descriptor-attributesbits->unknownbits$inline
                      unknownbits x-equiv)))
 :rule-classes :congruence)

Theorem: !data-segment-descriptor-attributesbits->unknownbits-is-data-segment-descriptor-attributesbits

(defthm
 !data-segment-descriptor-attributesbits->unknownbits-is-data-segment-descriptor-attributesbits
 (equal (!data-segment-descriptor-attributesbits->unknownbits
             unknownbits x)
        (change-data-segment-descriptor-attributesbits
             x
             :unknownbits unknownbits)))

Theorem: data-segment-descriptor-attributesbits->unknownbits-of-!data-segment-descriptor-attributesbits->unknownbits

(defthm
 data-segment-descriptor-attributesbits->unknownbits-of-!data-segment-descriptor-attributesbits->unknownbits
 (b* ((?new-x (!data-segment-descriptor-attributesbits->unknownbits$inline
                   unknownbits x)))
  (equal (data-segment-descriptor-attributesbits->unknownbits new-x)
         (4bits-fix unknownbits))))

Theorem: !data-segment-descriptor-attributesbits->unknownbits-equiv-under-mask

(defthm
 !data-segment-descriptor-attributesbits->unknownbits-equiv-under-mask
 (b* ((?new-x (!data-segment-descriptor-attributesbits->unknownbits$inline
                   unknownbits x)))
   (data-segment-descriptor-attributesbits-equiv-under-mask
        new-x x 4095)))

Function: data-segment-descriptor-attributesbits-debug

(defun data-segment-descriptor-attributesbits-debug (x)
 (declare
      (xargs :guard (data-segment-descriptor-attributesbits-p x)))
 (let ((__function__ 'data-segment-descriptor-attributesbits-debug))
  (declare (ignorable __function__))
  (b* (((data-segment-descriptor-attributesbits x)))
   (cons
    (cons 'a x.a)
    (cons
     (cons 'w x.w)
     (cons
      (cons 'e x.e)
      (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 'avl x.avl)
           (cons (cons 'l x.l)
                 (cons (cons 'd/b x.d/b)
                       (cons (cons 'g x.g)
                             (cons (cons 'unknownbits x.unknownbits)
                                   nil)))))))))))))))

Subtopics

!data-segment-descriptor-attributesbits->unknownbits: Update the |X86ISA|::|UNKNOWNBITS| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->msb-of-type: Update the |X86ISA|::|MSB-OF-TYPE| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits-p: Recognizer for data-segment-descriptor-attributesbits bit structures.
!data-segment-descriptor-attributesbits->d/b: Update the |X86ISA|::|D/B| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->dpl: Update the |X86ISA|::|DPL| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->avl: Update the |X86ISA|::|AVL| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->w: Update the |ACL2|::|W| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->s: Update the |X86ISA|::|S| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->p: Update the |ACL2|::|P| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->l: Update the |ACL2|::|L| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->g: Update the |X86ISA|::|G| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->e: Update the |ACL2|::|E| field of a data-segment-descriptor-attributesbits bit structure.
!data-segment-descriptor-attributesbits->a: Update the |ACL2|::|A| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits-fix: Fixing function for data-segment-descriptor-attributesbits bit structures.
Data-segment-descriptor-attributesbits->unknownbits: Access the |X86ISA|::|UNKNOWNBITS| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->msb-of-type: Access the |X86ISA|::|MSB-OF-TYPE| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->g: Access the |X86ISA|::|G| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->d/b: Access the |X86ISA|::|D/B| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->dpl: Access the |X86ISA|::|DPL| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->avl: Access the |X86ISA|::|AVL| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->w: Access the |ACL2|::|W| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->s: Access the |X86ISA|::|S| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->p: Access the |ACL2|::|P| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->l: Access the |ACL2|::|L| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->e: Access the |ACL2|::|E| field of a data-segment-descriptor-attributesbits bit structure.
Data-segment-descriptor-attributesbits->a: Access the |ACL2|::|A| field of a data-segment-descriptor-attributesbits bit structure.