		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Code-segment-descriptor-attributesbits

Subset of code-segment-descriptorBits.

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

Fields

a — bit
r — bit
c — bit
msb-of-type — bit
s — bit
dpl — 2bits
p — bit
avl — bit
l — bit
d — bit
g — bit
unknownbits — 4bits

Definitions and Theorems

Function: code-segment-descriptor-attributesbits-p

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

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

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

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

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

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

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

Function: code-segment-descriptor-attributesbits-fix

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: code-segment-descriptor-attributesbits

(defun code-segment-descriptor-attributesbits
       (a r c msb-of-type
          s dpl p avl l d g unknownbits)
 (declare (xargs :guard (and (bitp a)
                             (bitp r)
                             (bitp c)
                             (bitp msb-of-type)
                             (bitp s)
                             (2bits-p dpl)
                             (bitp p)
                             (bitp avl)
                             (bitp l)
                             (bitp d)
                             (bitp g)
                             (4bits-p unknownbits))))
 (let ((__function__ 'code-segment-descriptor-attributesbits))
  (declare (ignorable __function__))
  (b* ((a (mbe :logic (bfix a) :exec a))
       (r (mbe :logic (bfix r) :exec r))
       (c (mbe :logic (bfix c) :exec c))
       (msb-of-type (mbe :logic (bfix msb-of-type)
                         :exec msb-of-type))
       (s (mbe :logic (bfix s) :exec s))
       (dpl (mbe :logic (2bits-fix dpl) :exec dpl))
       (p (mbe :logic (bfix p) :exec p))
       (avl (mbe :logic (bfix avl) :exec avl))
       (l (mbe :logic (bfix l) :exec l))
       (d (mbe :logic (bfix d) :exec d))
       (g (mbe :logic (bfix g) :exec g))
       (unknownbits (mbe :logic (4bits-fix unknownbits)
                         :exec unknownbits)))
   (logapp
    1 a
    (logapp
     1 r
     (logapp
      1 c
      (logapp
       1 msb-of-type
       (logapp
        1 s
        (logapp
         2 dpl
         (logapp
          1 p
          (logapp
             1 avl
             (logapp 1 l
                     (logapp 1
                             d (logapp 1 g unknownbits))))))))))))))

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

(defthm
 code-segment-descriptor-attributesbits-p-of-code-segment-descriptor-attributesbits
 (b* ((code-segment-descriptor-attributesbits
           (code-segment-descriptor-attributesbits
                a r c msb-of-type
                s dpl p avl l d g unknownbits)))
   (code-segment-descriptor-attributesbits-p
        code-segment-descriptor-attributesbits))
 :rule-classes :rewrite)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-a
  (equal (code-segment-descriptor-attributesbits
              (bfix a)
              r c msb-of-type
              s dpl p avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-a
  (implies (bit-equiv a a-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a-equiv r c msb-of-type
                       s dpl p avl l d g unknownbits)))
  :rule-classes :congruence)

Theorem: code-segment-descriptor-attributesbits-of-bfix-r

(defthm code-segment-descriptor-attributesbits-of-bfix-r
  (equal (code-segment-descriptor-attributesbits
              a (bfix r)
              c msb-of-type
              s dpl p avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

Theorem: code-segment-descriptor-attributesbits-bit-equiv-congruence-on-r

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-r
  (implies (bit-equiv r r-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r-equiv c msb-of-type
                       s dpl p avl l d g unknownbits)))
  :rule-classes :congruence)

Theorem: code-segment-descriptor-attributesbits-of-bfix-c

(defthm code-segment-descriptor-attributesbits-of-bfix-c
  (equal (code-segment-descriptor-attributesbits
              a r (bfix c)
              msb-of-type
              s dpl p avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

Theorem: code-segment-descriptor-attributesbits-bit-equiv-congruence-on-c

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-c
  (implies (bit-equiv c c-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r c-equiv msb-of-type
                       s dpl p avl l d g unknownbits)))
  :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-msb-of-type
  (equal (code-segment-descriptor-attributesbits
              a r c (bfix msb-of-type)
              s dpl p avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
 code-segment-descriptor-attributesbits-bit-equiv-congruence-on-msb-of-type
 (implies (bit-equiv msb-of-type msb-of-type-equiv)
          (equal (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl p avl l d g unknownbits)
                 (code-segment-descriptor-attributesbits
                      a r c msb-of-type-equiv
                      s dpl p avl l d g unknownbits)))
 :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-s
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type (bfix s)
              dpl p avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-s
  (implies (bit-equiv s s-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s-equiv dpl p avl l d g unknownbits)))
  :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-2bits-fix-dpl
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type s (2bits-fix dpl)
              p avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
 code-segment-descriptor-attributesbits-2bits-equiv-congruence-on-dpl
 (implies (2bits-equiv dpl dpl-equiv)
          (equal (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl p avl l d g unknownbits)
                 (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl-equiv p avl l d g unknownbits)))
 :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-p
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type s dpl (bfix p)
              avl l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-p
  (implies (bit-equiv p p-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p-equiv avl l d g unknownbits)))
  :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-avl
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type s dpl p (bfix avl)
              l d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
 code-segment-descriptor-attributesbits-bit-equiv-congruence-on-avl
 (implies (bit-equiv avl avl-equiv)
          (equal (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl p avl l d g unknownbits)
                 (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl p avl-equiv l d g unknownbits)))
 :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-l
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type s dpl p avl (bfix l)
              d g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-l
  (implies (bit-equiv l l-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l-equiv d g unknownbits)))
  :rule-classes :congruence)

Theorem: code-segment-descriptor-attributesbits-of-bfix-d

(defthm code-segment-descriptor-attributesbits-of-bfix-d
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type s dpl p avl l (bfix d)
              g unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

Theorem: code-segment-descriptor-attributesbits-bit-equiv-congruence-on-d

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-d
  (implies (bit-equiv d d-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d-equiv g unknownbits)))
  :rule-classes :congruence)

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

(defthm code-segment-descriptor-attributesbits-of-bfix-g
  (equal (code-segment-descriptor-attributesbits
              a
              r c msb-of-type s dpl p avl l d (bfix g)
              unknownbits)
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
   code-segment-descriptor-attributesbits-bit-equiv-congruence-on-g
  (implies (bit-equiv g g-equiv)
           (equal (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g unknownbits)
                  (code-segment-descriptor-attributesbits
                       a r c msb-of-type
                       s dpl p avl l d g-equiv unknownbits)))
  :rule-classes :congruence)

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

(defthm
    code-segment-descriptor-attributesbits-of-4bits-fix-unknownbits
  (equal (code-segment-descriptor-attributesbits
              a r c msb-of-type s
              dpl p avl l d g (4bits-fix unknownbits))
         (code-segment-descriptor-attributesbits
              a r c msb-of-type
              s dpl p avl l d g unknownbits)))

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

(defthm
 code-segment-descriptor-attributesbits-4bits-equiv-congruence-on-unknownbits
 (implies (4bits-equiv unknownbits unknownbits-equiv)
          (equal (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl p avl l d g unknownbits)
                 (code-segment-descriptor-attributesbits
                      a r c msb-of-type
                      s dpl p avl l d g unknownbits-equiv)))
 :rule-classes :congruence)

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

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

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

(defun code-segment-descriptor-attributesbits->a$inline (x)
  (declare
       (xargs :guard (code-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (code-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-code-segment-descriptor-attributesbits->a

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->a-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->a
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix a)))

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

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

Function: code-segment-descriptor-attributesbits->r$inline

(defun code-segment-descriptor-attributesbits->r$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->r

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

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

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

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

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

Theorem: code-segment-descriptor-attributesbits->r-of-code-segment-descriptor-attributesbits

(defthm
 code-segment-descriptor-attributesbits->r-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->r
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix r)))

Theorem: code-segment-descriptor-attributesbits->r-of-write-with-mask

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

Function: code-segment-descriptor-attributesbits->c$inline

(defun code-segment-descriptor-attributesbits->c$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->c

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

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

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

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

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

Theorem: code-segment-descriptor-attributesbits->c-of-code-segment-descriptor-attributesbits

(defthm
 code-segment-descriptor-attributesbits->c-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->c
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix c)))

Theorem: code-segment-descriptor-attributesbits->c-of-write-with-mask

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

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

(defun code-segment-descriptor-attributesbits->msb-of-type$inline
       (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->msb-of-type

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->msb-of-type-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->msb-of-type
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix msb-of-type)))

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

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

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

(defun code-segment-descriptor-attributesbits->s$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->s

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->s-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->s
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix s)))

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

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

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

(defun code-segment-descriptor-attributesbits->dpl$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->dpl

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->dpl-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->dpl
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (2bits-fix dpl)))

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

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

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

(defun code-segment-descriptor-attributesbits->p$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->p

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->p-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->p
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix p)))

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

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

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

(defun code-segment-descriptor-attributesbits->avl$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->avl

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->avl-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->avl
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix avl)))

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

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

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

(defun code-segment-descriptor-attributesbits->l$inline (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (mbe
    :logic
    (let ((x (code-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-code-segment-descriptor-attributesbits->l

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->l-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->l
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix l)))

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

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

Function: code-segment-descriptor-attributesbits->d$inline

(defun code-segment-descriptor-attributesbits->d$inline (x)
  (declare
       (xargs :guard (code-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (code-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-code-segment-descriptor-attributesbits->d

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

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

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

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

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

Theorem: code-segment-descriptor-attributesbits->d-of-code-segment-descriptor-attributesbits

(defthm
 code-segment-descriptor-attributesbits->d-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->d
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix d)))

Theorem: code-segment-descriptor-attributesbits->d-of-write-with-mask

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

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

(defun code-segment-descriptor-attributesbits->g$inline (x)
  (declare
       (xargs :guard (code-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (code-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-code-segment-descriptor-attributesbits->g

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->g-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->g
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (bfix g)))

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

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

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

(defun code-segment-descriptor-attributesbits->unknownbits$inline
       (x)
  (declare
       (xargs :guard (code-segment-descriptor-attributesbits-p x)))
  (mbe :logic
       (let ((x (code-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-code-segment-descriptor-attributesbits->unknownbits

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

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

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

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

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

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

(defthm
 code-segment-descriptor-attributesbits->unknownbits-of-code-segment-descriptor-attributesbits
 (equal (code-segment-descriptor-attributesbits->unknownbits
             (code-segment-descriptor-attributesbits
                  a r c msb-of-type
                  s dpl p avl l d g unknownbits))
        (4bits-fix unknownbits)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: !code-segment-descriptor-attributesbits->r$inline

(defun !code-segment-descriptor-attributesbits->r$inline (r x)
 (declare
  (xargs :guard (and (bitp r)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((r (mbe :logic (bfix r) :exec r))
           (x (code-segment-descriptor-attributesbits-fix x)))
        (part-install r 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) r) 1))))))

Theorem: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->r

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

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

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

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

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

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

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

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

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

Theorem: !code-segment-descriptor-attributesbits->r-is-code-segment-descriptor-attributesbits

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

Theorem: code-segment-descriptor-attributesbits->r-of-!code-segment-descriptor-attributesbits->r

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

Theorem: !code-segment-descriptor-attributesbits->r-equiv-under-mask

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

Function: !code-segment-descriptor-attributesbits->c$inline

(defun !code-segment-descriptor-attributesbits->c$inline (c x)
 (declare
  (xargs :guard (and (bitp c)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((c (mbe :logic (bfix c) :exec c))
           (x (code-segment-descriptor-attributesbits-fix x)))
        (part-install c 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) c) 2))))))

Theorem: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->c

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

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

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

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

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

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

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

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

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

Theorem: !code-segment-descriptor-attributesbits->c-is-code-segment-descriptor-attributesbits

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

Theorem: code-segment-descriptor-attributesbits->c-of-!code-segment-descriptor-attributesbits->c

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

Theorem: !code-segment-descriptor-attributesbits->c-equiv-under-mask

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

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

(defun !code-segment-descriptor-attributesbits->msb-of-type$inline
       (msb-of-type x)
 (declare
  (xargs :guard (and (bitp msb-of-type)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((msb-of-type (mbe :logic (bfix msb-of-type)
                           :exec msb-of-type))
         (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->msb-of-type

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

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

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

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

(defthm
 !code-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 (!code-segment-descriptor-attributesbits->msb-of-type$inline
                      msb-of-type x)
                 (!code-segment-descriptor-attributesbits->msb-of-type$inline
                      msb-of-type-equiv x)))
 :rule-classes :congruence)

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

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

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

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

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

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

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

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

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

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

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

(defun !code-segment-descriptor-attributesbits->s$inline (s x)
 (declare
  (xargs :guard (and (bitp s)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((s (mbe :logic (bfix s) :exec s))
           (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->s

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defun !code-segment-descriptor-attributesbits->dpl$inline (dpl x)
 (declare
  (xargs :guard (and (2bits-p dpl)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl))
         (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->dpl

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defun !code-segment-descriptor-attributesbits->avl$inline (avl x)
 (declare
  (xargs :guard (and (bitp avl)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((avl (mbe :logic (bfix avl) :exec avl))
         (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->avl

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defun !code-segment-descriptor-attributesbits->l$inline (l x)
 (declare
  (xargs :guard (and (bitp l)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe :logic
      (b* ((l (mbe :logic (bfix l) :exec l))
           (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->l

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: !code-segment-descriptor-attributesbits->d$inline

(defun !code-segment-descriptor-attributesbits->d$inline (d x)
 (declare
  (xargs :guard (and (bitp d)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe
     :logic
     (b* ((d (mbe :logic (bfix d) :exec d))
          (x (code-segment-descriptor-attributesbits-fix x)))
       (part-install d 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) 10))))))

Theorem: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->d

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

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

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

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

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

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

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

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

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

Theorem: !code-segment-descriptor-attributesbits->d-is-code-segment-descriptor-attributesbits

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

Theorem: code-segment-descriptor-attributesbits->d-of-!code-segment-descriptor-attributesbits->d

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

Theorem: !code-segment-descriptor-attributesbits->d-equiv-under-mask

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

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

(defun !code-segment-descriptor-attributesbits->g$inline (g x)
 (declare
  (xargs :guard (and (bitp g)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe
     :logic
     (b* ((g (mbe :logic (bfix g) :exec g))
          (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->g

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defun !code-segment-descriptor-attributesbits->unknownbits$inline
       (unknownbits x)
 (declare
  (xargs :guard (and (4bits-p unknownbits)
                     (code-segment-descriptor-attributesbits-p x))))
 (mbe
    :logic
    (b* ((unknownbits (mbe :logic (4bits-fix unknownbits)
                           :exec unknownbits))
         (x (code-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: code-segment-descriptor-attributesbits-p-of-!code-segment-descriptor-attributesbits->unknownbits

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: code-segment-descriptor-attributesbits-debug

(defun code-segment-descriptor-attributesbits-debug (x)
 (declare
      (xargs :guard (code-segment-descriptor-attributesbits-p x)))
 (let ((__function__ 'code-segment-descriptor-attributesbits-debug))
  (declare (ignorable __function__))
  (b* (((code-segment-descriptor-attributesbits x)))
   (cons
    (cons 'a x.a)
    (cons
     (cons 'r x.r)
     (cons
      (cons 'c x.c)
      (cons
       (cons 'msb-of-type x.msb-of-type)
       (cons
        (cons 's x.s)
        (cons
         (cons 'dpl x.dpl)
         (cons
          (cons 'p x.p)
          (cons
           (cons 'avl x.avl)
           (cons (cons 'l x.l)
                 (cons (cons 'd x.d)
                       (cons (cons 'g x.g)
                             (cons (cons 'unknownbits x.unknownbits)
                                   nil)))))))))))))))

Subtopics

!code-segment-descriptor-attributesbits->unknownbits: Update the |X86ISA|::|UNKNOWNBITS| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->msb-of-type: Update the |X86ISA|::|MSB-OF-TYPE| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits-p: Recognizer for code-segment-descriptor-attributesbits bit structures.
!code-segment-descriptor-attributesbits->dpl: Update the |X86ISA|::|DPL| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->avl: Update the |X86ISA|::|AVL| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->s: Update the |X86ISA|::|S| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->r: Update the |ACL2|::|R| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->p: Update the |ACL2|::|P| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->l: Update the |ACL2|::|L| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->g: Update the |X86ISA|::|G| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->d: Update the |ACL2|::|D| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->c: Update the |ACL2|::|C| field of a code-segment-descriptor-attributesbits bit structure.
!code-segment-descriptor-attributesbits->a: Update the |ACL2|::|A| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits-fix: Fixing function for code-segment-descriptor-attributesbits bit structures.
Code-segment-descriptor-attributesbits->unknownbits: Access the |X86ISA|::|UNKNOWNBITS| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->msb-of-type: Access the |X86ISA|::|MSB-OF-TYPE| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->g: Access the |X86ISA|::|G| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->dpl: Access the |X86ISA|::|DPL| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->d: Access the |ACL2|::|D| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->avl: Access the |X86ISA|::|AVL| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->s: Access the |X86ISA|::|S| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->r: Access the |ACL2|::|R| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->p: Access the |ACL2|::|P| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->l: Access the |ACL2|::|L| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->c: Access the |ACL2|::|C| field of a code-segment-descriptor-attributesbits bit structure.
Code-segment-descriptor-attributesbits->a: Access the |ACL2|::|A| field of a code-segment-descriptor-attributesbits bit structure.