		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Data-segment-descriptorbits

AMD manual, Jun'23, Vol. 2, Figures 4-21 and 4-15.

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

Fields

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

Definitions and Theorems

Function: data-segment-descriptorbits-p

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

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

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

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

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

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

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

Function: data-segment-descriptorbits-fix

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

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

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

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

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

Function: data-segment-descriptorbits-equiv$inline

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

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

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

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

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

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

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

Function: data-segment-descriptorbits

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

Theorem: data-segment-descriptorbits-p-of-data-segment-descriptorbits

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

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

(defthm data-segment-descriptorbits-of-16bits-fix-limit15-0
 (equal
  (data-segment-descriptorbits
       (16bits-fix limit15-0)
       base15-0 base23-16 a w e msb-of-type s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-16bits-fix-base15-0
 (equal
  (data-segment-descriptorbits
       limit15-0 (16bits-fix base15-0)
       base23-16 a w e msb-of-type s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-8bits-fix-base23-16
 (equal
  (data-segment-descriptorbits
       limit15-0 base15-0 (8bits-fix base23-16)
       a w e msb-of-type s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-bfix-a
 (equal
  (data-segment-descriptorbits
       limit15-0 base15-0 base23-16 (bfix a)
       w e msb-of-type s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

Theorem: data-segment-descriptorbits-of-bfix-w

(defthm data-segment-descriptorbits-of-bfix-w
 (equal
  (data-segment-descriptorbits
       limit15-0 base15-0 base23-16 a (bfix w)
       e msb-of-type s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

Theorem: data-segment-descriptorbits-bit-equiv-congruence-on-w

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

Theorem: data-segment-descriptorbits-of-bfix-e

(defthm data-segment-descriptorbits-of-bfix-e
 (equal
  (data-segment-descriptorbits
       limit15-0
       base15-0 base23-16 a w (bfix e)
       msb-of-type s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

Theorem: data-segment-descriptorbits-bit-equiv-congruence-on-e

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

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

(defthm data-segment-descriptorbits-of-bfix-msb-of-type
 (equal
  (data-segment-descriptorbits
       limit15-0 base15-0
       base23-16 a w e (bfix msb-of-type)
       s
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-bfix-s
 (equal
  (data-segment-descriptorbits
       limit15-0 base15-0
       base23-16 a w e msb-of-type (bfix s)
       dpl p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-2bits-fix-dpl
 (equal
  (data-segment-descriptorbits limit15-0 base15-0 base23-16
                               a w e msb-of-type s (2bits-fix dpl)
                               p limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-bfix-p
 (equal
  (data-segment-descriptorbits limit15-0 base15-0 base23-16
                               a w e msb-of-type s dpl (bfix p)
                               limit19-16 avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-4bits-fix-limit19-16
 (equal
  (data-segment-descriptorbits limit15-0
                               base15-0 base23-16 a w e msb-of-type
                               s dpl p (4bits-fix limit19-16)
                               avl l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-bfix-avl
 (equal
  (data-segment-descriptorbits limit15-0
                               base15-0 base23-16 a w e msb-of-type
                               s dpl p limit19-16 (bfix avl)
                               l d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-bfix-l
 (equal
  (data-segment-descriptorbits limit15-0
                               base15-0 base23-16 a w e msb-of-type
                               s dpl p limit19-16 avl (bfix l)
                               d/b g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

Theorem: data-segment-descriptorbits-of-bfix-d/b

(defthm data-segment-descriptorbits-of-bfix-d/b
 (equal
  (data-segment-descriptorbits limit15-0
                               base15-0 base23-16 a w e msb-of-type
                               s dpl p limit19-16 avl l (bfix d/b)
                               g base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-bfix-g
 (equal
  (data-segment-descriptorbits limit15-0
                               base15-0 base23-16 a w e msb-of-type
                               s dpl p limit19-16 avl l d/b (bfix g)
                               base31-24)
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

(defthm data-segment-descriptorbits-of-8bits-fix-base31-24
 (equal
  (data-segment-descriptorbits limit15-0 base15-0 base23-16
                               a w e msb-of-type s dpl p limit19-16
                               avl l d/b g (8bits-fix base31-24))
  (data-segment-descriptorbits limit15-0 base15-0
                               base23-16 a w e msb-of-type s dpl
                               p limit19-16 avl l d/b g base31-24)))

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

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

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

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

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

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

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

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

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

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

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

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

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

(defthm
 data-segment-descriptorbits->limit15-0-of-data-segment-descriptorbits
 (equal (data-segment-descriptorbits->limit15-0
             (data-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a w e msb-of-type s
                  dpl p limit19-16 avl l d/b g base31-24))
        (16bits-fix limit15-0)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
 data-segment-descriptorbits->base15-0-of-data-segment-descriptorbits
 (equal (data-segment-descriptorbits->base15-0
             (data-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a w e msb-of-type s
                  dpl p limit19-16 avl l d/b g base31-24))
        (16bits-fix base15-0)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
 data-segment-descriptorbits->base23-16-of-data-segment-descriptorbits
 (equal (data-segment-descriptorbits->base23-16
             (data-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a w e msb-of-type s
                  dpl p limit19-16 avl l d/b g base31-24))
        (8bits-fix base23-16)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
      data-segment-descriptorbits->a-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->a
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix a)))

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

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

Function: data-segment-descriptorbits->w$inline

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

Theorem: bitp-of-data-segment-descriptorbits->w

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

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

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

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

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

Theorem: data-segment-descriptorbits->w-of-data-segment-descriptorbits

(defthm
      data-segment-descriptorbits->w-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->w
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix w)))

Theorem: data-segment-descriptorbits->w-of-write-with-mask

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

Function: data-segment-descriptorbits->e$inline

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

Theorem: bitp-of-data-segment-descriptorbits->e

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

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

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

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

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

Theorem: data-segment-descriptorbits->e-of-data-segment-descriptorbits

(defthm
      data-segment-descriptorbits->e-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->e
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix e)))

Theorem: data-segment-descriptorbits->e-of-write-with-mask

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

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

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

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

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

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

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

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

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

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

(defthm
 data-segment-descriptorbits->msb-of-type-of-data-segment-descriptorbits
 (equal (data-segment-descriptorbits->msb-of-type
             (data-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a w e msb-of-type s
                  dpl p limit19-16 avl l d/b g base31-24))
        (bfix msb-of-type)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
      data-segment-descriptorbits->s-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->s
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix s)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
    data-segment-descriptorbits->dpl-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->dpl
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (2bits-fix dpl)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
      data-segment-descriptorbits->p-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->p
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix p)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
 data-segment-descriptorbits->limit19-16-of-data-segment-descriptorbits
 (equal (data-segment-descriptorbits->limit19-16
             (data-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a w e msb-of-type s
                  dpl p limit19-16 avl l d/b g base31-24))
        (4bits-fix limit19-16)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
    data-segment-descriptorbits->avl-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->avl
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix avl)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
      data-segment-descriptorbits->l-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->l
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix l)))

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

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

Function: data-segment-descriptorbits->d/b$inline

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

Theorem: bitp-of-data-segment-descriptorbits->d/b

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

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

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

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

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

Theorem: data-segment-descriptorbits->d/b-of-data-segment-descriptorbits

(defthm
    data-segment-descriptorbits->d/b-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->d/b
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix d/b)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
      data-segment-descriptorbits->g-of-data-segment-descriptorbits
  (equal (data-segment-descriptorbits->g
              (data-segment-descriptorbits
                   limit15-0
                   base15-0 base23-16 a w e msb-of-type s
                   dpl p limit19-16 avl l d/b g base31-24))
         (bfix g)))

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

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

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

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

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

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

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

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

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

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

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

(defthm
 data-segment-descriptorbits->base31-24-of-data-segment-descriptorbits
 (equal (data-segment-descriptorbits->base31-24
             (data-segment-descriptorbits
                  limit15-0
                  base15-0 base23-16 a w e msb-of-type s
                  dpl p limit19-16 avl l d/b g base31-24))
        (8bits-fix base31-24)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: !data-segment-descriptorbits->w$inline

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

Theorem: data-segment-descriptorbits-p-of-!data-segment-descriptorbits->w

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

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

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

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

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

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

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

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

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

Theorem: !data-segment-descriptorbits->w-is-data-segment-descriptorbits

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

Theorem: data-segment-descriptorbits->w-of-!data-segment-descriptorbits->w

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

Theorem: !data-segment-descriptorbits->w-equiv-under-mask

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

Function: !data-segment-descriptorbits->e$inline

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

Theorem: data-segment-descriptorbits-p-of-!data-segment-descriptorbits->e

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

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

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

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

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

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

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

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

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

Theorem: !data-segment-descriptorbits->e-is-data-segment-descriptorbits

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

Theorem: data-segment-descriptorbits->e-of-!data-segment-descriptorbits->e

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

Theorem: !data-segment-descriptorbits->e-equiv-under-mask

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: !data-segment-descriptorbits->d/b-is-data-segment-descriptorbits

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

Theorem: data-segment-descriptorbits->d/b-of-!data-segment-descriptorbits->d/b

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: data-segment-descriptorbits-debug

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

Subtopics

Data-segment-descriptorbits-p: Recognizer for data-segment-descriptorbits bit structures.
!data-segment-descriptorbits->msb-of-type: Update the |X86ISA|::|MSB-OF-TYPE| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->limit19-16: Update the |X86ISA|::|LIMIT19-16| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->base31-24: Update the |X86ISA|::|BASE31-24| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->limit15-0: Update the |X86ISA|::|LIMIT15-0| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->base23-16: Update the |X86ISA|::|BASE23-16| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->base15-0: Update the |X86ISA|::|BASE15-0| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->dpl: Update the |X86ISA|::|DPL| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->d/b: Update the |X86ISA|::|D/B| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->avl: Update the |X86ISA|::|AVL| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->w: Update the |ACL2|::|W| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->s: Update the |X86ISA|::|S| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->p: Update the |ACL2|::|P| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->l: Update the |ACL2|::|L| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->g: Update the |X86ISA|::|G| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->e: Update the |ACL2|::|E| field of a data-segment-descriptorbits bit structure.
!data-segment-descriptorbits->a: Update the |ACL2|::|A| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->msb-of-type: Access the |X86ISA|::|MSB-OF-TYPE| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->limit19-16: Access the |X86ISA|::|LIMIT19-16| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits-fix: Fixing function for data-segment-descriptorbits bit structures.
Data-segment-descriptorbits->limit15-0: Access the |X86ISA|::|LIMIT15-0| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->base31-24: Access the |X86ISA|::|BASE31-24| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->base23-16: Access the |X86ISA|::|BASE23-16| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->base15-0: Access the |X86ISA|::|BASE15-0| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->dpl: Access the |X86ISA|::|DPL| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->w: Access the |ACL2|::|W| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->s: Access the |X86ISA|::|S| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->p: Access the |ACL2|::|P| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->l: Access the |ACL2|::|L| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->g: Access the |X86ISA|::|G| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->e: Access the |ACL2|::|E| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->d/b: Access the |X86ISA|::|D/B| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->avl: Access the |X86ISA|::|AVL| field of a data-segment-descriptorbits bit structure.
Data-segment-descriptorbits->a: Access the |ACL2|::|A| field of a data-segment-descriptorbits bit structure.