		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

System-segment-descriptorbits

AMD manual, Jun'23, Vol. 2, Figure 4-22.

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

Fields

limit15-0 — 16bits
base15-0 — 16bits
base23-16 — 8bits
type — 4bits
s — bit
dpl — 2bits
p — bit
limit19-16 — 4bits
avl — bit
res1 — 2bits
g — bit
base31-24 — 8bits
base63-32 — 32bits
res2 — 8bits
all-zeroes? — 5bits
res3 — 19bits

Definitions and Theorems

Function: system-segment-descriptorbits-p

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

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

(defthm system-segment-descriptorbits-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 128 x)
           (system-segment-descriptorbits-p x)))

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

(defthm unsigned-byte-p-when-system-segment-descriptorbits-p
  (implies (system-segment-descriptorbits-p x)
           (unsigned-byte-p 128 x)))

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

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

Function: system-segment-descriptorbits-fix

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

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

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

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

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

Function: system-segment-descriptorbits-equiv$inline

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

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

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

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

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

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

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

Function: system-segment-descriptorbits

(defun system-segment-descriptorbits
       (limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3)
 (declare (xargs :guard (and (16bits-p limit15-0)
                             (16bits-p base15-0)
                             (8bits-p base23-16)
                             (4bits-p type)
                             (bitp s)
                             (2bits-p dpl)
                             (bitp p)
                             (4bits-p limit19-16)
                             (bitp avl)
                             (2bits-p res1)
                             (bitp g)
                             (8bits-p base31-24)
                             (32bits-p base63-32)
                             (8bits-p res2)
                             (5bits-p all-zeroes?)
                             (19bits-p res3))))
 (let ((__function__ 'system-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))
       (type (mbe :logic (4bits-fix type)
                  :exec 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))
       (res1 (mbe :logic (2bits-fix res1)
                  :exec res1))
       (g (mbe :logic (bfix g) :exec g))
       (base31-24 (mbe :logic (8bits-fix base31-24)
                       :exec base31-24))
       (base63-32 (mbe :logic (32bits-fix base63-32)
                       :exec base63-32))
       (res2 (mbe :logic (8bits-fix res2)
                  :exec res2))
       (all-zeroes? (mbe :logic (5bits-fix all-zeroes?)
                         :exec all-zeroes?))
       (res3 (mbe :logic (19bits-fix res3)
                  :exec res3)))
   (logapp
    16 limit15-0
    (logapp
     16 base15-0
     (logapp
      8 base23-16
      (logapp
       4 type
       (logapp
        1 s
        (logapp
         2 dpl
         (logapp
          1 p
          (logapp
           4 limit19-16
           (logapp
            1 avl
            (logapp
             2 res1
             (logapp
              1 g
              (logapp
               8 base31-24
               (logapp
                32 base63-32
                (logapp 8 res2
                        (logapp 5 all-zeroes? res3))))))))))))))))))

Theorem: system-segment-descriptorbits-p-of-system-segment-descriptorbits

(defthm
   system-segment-descriptorbits-p-of-system-segment-descriptorbits
  (b* ((system-segment-descriptorbits
            (system-segment-descriptorbits
                 limit15-0 base15-0 base23-16 type
                 s dpl p limit19-16 avl res1 g base31-24
                 base63-32 res2 all-zeroes? res3)))
    (system-segment-descriptorbits-p system-segment-descriptorbits))
  :rule-classes :rewrite)

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

(defthm system-segment-descriptorbits-of-16bits-fix-limit15-0
  (equal (system-segment-descriptorbits
              (16bits-fix limit15-0)
              base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

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

(defthm
 system-segment-descriptorbits-16bits-equiv-congruence-on-limit15-0
 (implies (16bits-equiv limit15-0 limit15-0-equiv)
          (equal (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32 res2 all-zeroes? res3)
                 (system-segment-descriptorbits
                      limit15-0-equiv base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-16bits-fix-base15-0
  (equal (system-segment-descriptorbits
              limit15-0 (16bits-fix base15-0)
              base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

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

(defthm
  system-segment-descriptorbits-16bits-equiv-congruence-on-base15-0
  (implies (16bits-equiv base15-0 base15-0-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0-equiv base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-8bits-fix-base23-16
  (equal (system-segment-descriptorbits
              limit15-0 base15-0 (8bits-fix base23-16)
              type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

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

(defthm
  system-segment-descriptorbits-8bits-equiv-congruence-on-base23-16
  (implies (8bits-equiv base23-16 base23-16-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16-equiv type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

Theorem: system-segment-descriptorbits-of-4bits-fix-type

(defthm system-segment-descriptorbits-of-4bits-fix-type
  (equal (system-segment-descriptorbits
              limit15-0
              base15-0 base23-16 (4bits-fix type)
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

Theorem: system-segment-descriptorbits-4bits-equiv-congruence-on-type

(defthm system-segment-descriptorbits-4bits-equiv-congruence-on-type
  (implies (4bits-equiv type type-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type-equiv
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-bfix-s
  (equal (system-segment-descriptorbits
              limit15-0
              base15-0 base23-16 type (bfix s)
              dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

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

(defthm system-segment-descriptorbits-bit-equiv-congruence-on-s
  (implies (bit-equiv s s-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 type s-equiv
                       dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-2bits-fix-dpl
 (equal
    (system-segment-descriptorbits limit15-0 base15-0
                                   base23-16 type s (2bits-fix dpl)
                                   p limit19-16 avl res1 g base31-24
                                   base63-32 res2 all-zeroes? res3)
    (system-segment-descriptorbits
         limit15-0 base15-0 base23-16 type
         s dpl p limit19-16 avl res1 g base31-24
         base63-32 res2 all-zeroes? res3)))

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

(defthm system-segment-descriptorbits-2bits-equiv-congruence-on-dpl
  (implies (2bits-equiv dpl dpl-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0
                       base15-0 base23-16 type s dpl-equiv
                       p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-bfix-p
  (equal (system-segment-descriptorbits
              limit15-0
              base15-0 base23-16 type s dpl (bfix p)
              limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

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

(defthm system-segment-descriptorbits-bit-equiv-congruence-on-p
  (implies (bit-equiv p p-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type s dpl
                       p-equiv limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-4bits-fix-limit19-16
 (equal
  (system-segment-descriptorbits limit15-0 base15-0 base23-16
                                 type s dpl p (4bits-fix limit19-16)
                                 avl res1 g base31-24
                                 base63-32 res2 all-zeroes? res3)
  (system-segment-descriptorbits
       limit15-0 base15-0 base23-16 type
       s dpl p limit19-16 avl res1 g base31-24
       base63-32 res2 all-zeroes? res3)))

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

(defthm
 system-segment-descriptorbits-4bits-equiv-congruence-on-limit19-16
 (implies (4bits-equiv limit19-16 limit19-16-equiv)
          (equal (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32 res2 all-zeroes? res3)
                 (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type s dpl
                      p limit19-16-equiv avl res1 g base31-24
                      base63-32 res2 all-zeroes? res3)))
 :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-bfix-avl
 (equal
   (system-segment-descriptorbits limit15-0 base15-0 base23-16
                                  type s dpl p limit19-16 (bfix avl)
                                  res1 g base31-24
                                  base63-32 res2 all-zeroes? res3)
   (system-segment-descriptorbits
        limit15-0 base15-0 base23-16 type
        s dpl p limit19-16 avl res1 g base31-24
        base63-32 res2 all-zeroes? res3)))

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

(defthm system-segment-descriptorbits-bit-equiv-congruence-on-avl
  (implies (bit-equiv avl avl-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type s dpl
                       p limit19-16 avl-equiv res1 g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

Theorem: system-segment-descriptorbits-of-2bits-fix-res1

(defthm system-segment-descriptorbits-of-2bits-fix-res1
  (equal (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl (2bits-fix res1)
              g base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

Theorem: system-segment-descriptorbits-2bits-equiv-congruence-on-res1

(defthm system-segment-descriptorbits-2bits-equiv-congruence-on-res1
  (implies (2bits-equiv res1 res1-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type s dpl
                       p limit19-16 avl res1-equiv g base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-bfix-g
  (equal (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 (bfix g)
              base31-24
              base63-32 res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

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

(defthm system-segment-descriptorbits-bit-equiv-congruence-on-g
  (implies (bit-equiv g g-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type s dpl
                       p limit19-16 avl res1 g-equiv base31-24
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

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

(defthm system-segment-descriptorbits-of-8bits-fix-base31-24
 (equal
    (system-segment-descriptorbits limit15-0 base15-0
                                   base23-16 type s dpl p limit19-16
                                   avl res1 g (8bits-fix base31-24)
                                   base63-32 res2 all-zeroes? res3)
    (system-segment-descriptorbits
         limit15-0 base15-0 base23-16 type
         s dpl p limit19-16 avl res1 g base31-24
         base63-32 res2 all-zeroes? res3)))

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

(defthm
  system-segment-descriptorbits-8bits-equiv-congruence-on-base31-24
  (implies (8bits-equiv base31-24 base31-24-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type s dpl
                       p limit19-16 avl res1 g base31-24-equiv
                       base63-32 res2 all-zeroes? res3)))
  :rule-classes :congruence)

Theorem: system-segment-descriptorbits-of-32bits-fix-base63-32

(defthm system-segment-descriptorbits-of-32bits-fix-base63-32
  (equal (system-segment-descriptorbits
              limit15-0 base15-0
              base23-16 type s dpl p limit19-16 avl
              res1 g base31-24 (32bits-fix base63-32)
              res2 all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

Theorem: system-segment-descriptorbits-32bits-equiv-congruence-on-base63-32

(defthm
 system-segment-descriptorbits-32bits-equiv-congruence-on-base63-32
 (implies (32bits-equiv base63-32 base63-32-equiv)
          (equal (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32 res2 all-zeroes? res3)
                 (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32-equiv res2 all-zeroes? res3)))
 :rule-classes :congruence)

Theorem: system-segment-descriptorbits-of-8bits-fix-res2

(defthm system-segment-descriptorbits-of-8bits-fix-res2
  (equal (system-segment-descriptorbits
              limit15-0 base15-0 base23-16
              type s dpl p limit19-16 avl res1
              g base31-24 base63-32 (8bits-fix res2)
              all-zeroes? res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

Theorem: system-segment-descriptorbits-8bits-equiv-congruence-on-res2

(defthm system-segment-descriptorbits-8bits-equiv-congruence-on-res2
  (implies (8bits-equiv res2 res2-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2-equiv all-zeroes? res3)))
  :rule-classes :congruence)

Theorem: system-segment-descriptorbits-of-5bits-fix-all-zeroes?

(defthm system-segment-descriptorbits-of-5bits-fix-all-zeroes?
  (equal (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 (5bits-fix all-zeroes?)
              res3)
         (system-segment-descriptorbits
              limit15-0 base15-0 base23-16 type
              s dpl p limit19-16 avl res1 g base31-24
              base63-32 res2 all-zeroes? res3)))

Theorem: system-segment-descriptorbits-5bits-equiv-congruence-on-all-zeroes?

(defthm
 system-segment-descriptorbits-5bits-equiv-congruence-on-all-zeroes?
 (implies (5bits-equiv all-zeroes? all-zeroes?-equiv)
          (equal (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32 res2 all-zeroes? res3)
                 (system-segment-descriptorbits
                      limit15-0 base15-0 base23-16 type
                      s dpl p limit19-16 avl res1 g base31-24
                      base63-32 res2 all-zeroes?-equiv res3)))
 :rule-classes :congruence)

Theorem: system-segment-descriptorbits-of-19bits-fix-res3

(defthm system-segment-descriptorbits-of-19bits-fix-res3
 (equal
  (system-segment-descriptorbits limit15-0 base15-0
                                 base23-16 type s dpl p limit19-16
                                 avl res1 g base31-24 base63-32
                                 res2 all-zeroes? (19bits-fix res3))
  (system-segment-descriptorbits
       limit15-0 base15-0 base23-16 type
       s dpl p limit19-16 avl res1 g base31-24
       base63-32 res2 all-zeroes? res3)))

Theorem: system-segment-descriptorbits-19bits-equiv-congruence-on-res3

(defthm
      system-segment-descriptorbits-19bits-equiv-congruence-on-res3
  (implies (19bits-equiv res3 res3-equiv)
           (equal (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3)
                  (system-segment-descriptorbits
                       limit15-0 base15-0 base23-16 type
                       s dpl p limit19-16 avl res1 g base31-24
                       base63-32 res2 all-zeroes? res3-equiv)))
  :rule-classes :congruence)

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

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

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

(defun system-segment-descriptorbits->limit15-0$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 128) x)))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->limit15-0-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->limit15-0
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (16bits-fix limit15-0)))

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

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

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

(defun system-segment-descriptorbits->base15-0$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 112)
                               (ash (the (unsigned-byte 128) x)
                                    -16))))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->base15-0-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->base15-0
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (16bits-fix base15-0)))

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

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

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

(defun system-segment-descriptorbits->base23-16$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 96)
                               (ash (the (unsigned-byte 128) x)
                                    -32))))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->base23-16-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->base23-16
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (8bits-fix base23-16)))

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

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

Function: system-segment-descriptorbits->type$inline

(defun system-segment-descriptorbits->type$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-segment-descriptorbits-fix x)))
         (part-select x :low 40 :width 4))
       :exec (the (unsigned-byte 4)
                  (logand (the (unsigned-byte 4) 15)
                          (the (unsigned-byte 88)
                               (ash (the (unsigned-byte 128) x)
                                    -40))))))

Theorem: 4bits-p-of-system-segment-descriptorbits->type

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

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

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

Theorem: system-segment-descriptorbits->type$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: system-segment-descriptorbits->type-of-system-segment-descriptorbits

(defthm
 system-segment-descriptorbits->type-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->type
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (4bits-fix type)))

Theorem: system-segment-descriptorbits->type-of-write-with-mask

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

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

(defun system-segment-descriptorbits->s$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 84)
                               (ash (the (unsigned-byte 128) x)
                                    -44))))))

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

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

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

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

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

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

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

(defthm
  system-segment-descriptorbits->s-of-system-segment-descriptorbits
  (equal (system-segment-descriptorbits->s
              (system-segment-descriptorbits
                   limit15-0 base15-0 base23-16 type
                   s dpl p limit19-16 avl res1 g base31-24
                   base63-32 res2 all-zeroes? res3))
         (bfix s)))

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

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

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

(defun system-segment-descriptorbits->dpl$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 83)
                               (ash (the (unsigned-byte 128) x)
                                    -45))))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->dpl-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->dpl
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (2bits-fix dpl)))

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

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

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

(defun system-segment-descriptorbits->p$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 81)
                               (ash (the (unsigned-byte 128) x)
                                    -47))))))

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

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

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

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

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

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

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

(defthm
  system-segment-descriptorbits->p-of-system-segment-descriptorbits
  (equal (system-segment-descriptorbits->p
              (system-segment-descriptorbits
                   limit15-0 base15-0 base23-16 type
                   s dpl p limit19-16 avl res1 g base31-24
                   base63-32 res2 all-zeroes? res3))
         (bfix p)))

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

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

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

(defun system-segment-descriptorbits->limit19-16$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 80)
                               (ash (the (unsigned-byte 128) x)
                                    -48))))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->limit19-16-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->limit19-16
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (4bits-fix limit19-16)))

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

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

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

(defun system-segment-descriptorbits->avl$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 76)
                               (ash (the (unsigned-byte 128) x)
                                    -52))))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->avl-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->avl
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (bfix avl)))

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

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

Function: system-segment-descriptorbits->res1$inline

(defun system-segment-descriptorbits->res1$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-segment-descriptorbits-fix x)))
         (part-select x :low 53 :width 2))
       :exec (the (unsigned-byte 2)
                  (logand (the (unsigned-byte 2) 3)
                          (the (unsigned-byte 75)
                               (ash (the (unsigned-byte 128) x)
                                    -53))))))

Theorem: 2bits-p-of-system-segment-descriptorbits->res1

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

Theorem: system-segment-descriptorbits->res1$inline-of-system-segment-descriptorbits-fix-x

(defthm
 system-segment-descriptorbits->res1$inline-of-system-segment-descriptorbits-fix-x
 (equal (system-segment-descriptorbits->res1$inline
             (system-segment-descriptorbits-fix x))
        (system-segment-descriptorbits->res1$inline x)))

Theorem: system-segment-descriptorbits->res1$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: system-segment-descriptorbits->res1-of-system-segment-descriptorbits

(defthm
 system-segment-descriptorbits->res1-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->res1
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (2bits-fix res1)))

Theorem: system-segment-descriptorbits->res1-of-write-with-mask

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

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

(defun system-segment-descriptorbits->g$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 73)
                               (ash (the (unsigned-byte 128) x)
                                    -55))))))

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

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

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

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

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

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

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

(defthm
  system-segment-descriptorbits->g-of-system-segment-descriptorbits
  (equal (system-segment-descriptorbits->g
              (system-segment-descriptorbits
                   limit15-0 base15-0 base23-16 type
                   s dpl p limit19-16 avl res1 g base31-24
                   base63-32 res2 all-zeroes? res3))
         (bfix g)))

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

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

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

(defun system-segment-descriptorbits->base31-24$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-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 72)
                               (ash (the (unsigned-byte 128) x)
                                    -56))))))

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

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

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

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

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

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

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

(defthm
 system-segment-descriptorbits->base31-24-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->base31-24
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (8bits-fix base31-24)))

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

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

Function: system-segment-descriptorbits->base63-32$inline

(defun system-segment-descriptorbits->base63-32$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-segment-descriptorbits-fix x)))
         (part-select x :low 64 :width 32))
       :exec (the (unsigned-byte 32)
                  (logand (the (unsigned-byte 32) 4294967295)
                          (the (unsigned-byte 64)
                               (ash (the (unsigned-byte 128) x)
                                    -64))))))

Theorem: 32bits-p-of-system-segment-descriptorbits->base63-32

(defthm 32bits-p-of-system-segment-descriptorbits->base63-32
  (b*
   ((base63-32 (system-segment-descriptorbits->base63-32$inline x)))
   (32bits-p base63-32))
  :rule-classes :rewrite)

Theorem: system-segment-descriptorbits->base63-32$inline-of-system-segment-descriptorbits-fix-x

(defthm
 system-segment-descriptorbits->base63-32$inline-of-system-segment-descriptorbits-fix-x
 (equal (system-segment-descriptorbits->base63-32$inline
             (system-segment-descriptorbits-fix x))
        (system-segment-descriptorbits->base63-32$inline x)))

Theorem: system-segment-descriptorbits->base63-32$inline-system-segment-descriptorbits-equiv-congruence-on-x

(defthm
 system-segment-descriptorbits->base63-32$inline-system-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (system-segment-descriptorbits-equiv x x-equiv)
  (equal (system-segment-descriptorbits->base63-32$inline x)
         (system-segment-descriptorbits->base63-32$inline x-equiv)))
 :rule-classes :congruence)

Theorem: system-segment-descriptorbits->base63-32-of-system-segment-descriptorbits

(defthm
 system-segment-descriptorbits->base63-32-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->base63-32
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (32bits-fix base63-32)))

Theorem: system-segment-descriptorbits->base63-32-of-write-with-mask

(defthm system-segment-descriptorbits->base63-32-of-write-with-mask
 (implies
  (and
      (fty::bitstruct-read-over-write-hyps
           x
           system-segment-descriptorbits-equiv-under-mask)
      (system-segment-descriptorbits-equiv-under-mask x y fty::mask)
      (equal (logand (lognot fty::mask)
                     79228162495817593519834398720)
             0))
  (equal (system-segment-descriptorbits->base63-32 x)
         (system-segment-descriptorbits->base63-32 y))))

Function: system-segment-descriptorbits->res2$inline

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

Theorem: 8bits-p-of-system-segment-descriptorbits->res2

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

Theorem: system-segment-descriptorbits->res2$inline-of-system-segment-descriptorbits-fix-x

(defthm
 system-segment-descriptorbits->res2$inline-of-system-segment-descriptorbits-fix-x
 (equal (system-segment-descriptorbits->res2$inline
             (system-segment-descriptorbits-fix x))
        (system-segment-descriptorbits->res2$inline x)))

Theorem: system-segment-descriptorbits->res2$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: system-segment-descriptorbits->res2-of-system-segment-descriptorbits

(defthm
 system-segment-descriptorbits->res2-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->res2
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (8bits-fix res2)))

Theorem: system-segment-descriptorbits->res2-of-write-with-mask

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

Function: system-segment-descriptorbits->all-zeroes?$inline

(defun system-segment-descriptorbits->all-zeroes?$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-segment-descriptorbits-fix x)))
         (part-select x :low 104 :width 5))
       :exec (the (unsigned-byte 5)
                  (logand (the (unsigned-byte 5) 31)
                          (the (unsigned-byte 24)
                               (ash (the (unsigned-byte 128) x)
                                    -104))))))

Theorem: 5bits-p-of-system-segment-descriptorbits->all-zeroes?

(defthm 5bits-p-of-system-segment-descriptorbits->all-zeroes?
  (b* ((all-zeroes?
            (system-segment-descriptorbits->all-zeroes?$inline x)))
    (5bits-p all-zeroes?))
  :rule-classes :rewrite)

Theorem: system-segment-descriptorbits->all-zeroes?$inline-of-system-segment-descriptorbits-fix-x

(defthm
 system-segment-descriptorbits->all-zeroes?$inline-of-system-segment-descriptorbits-fix-x
 (equal (system-segment-descriptorbits->all-zeroes?$inline
             (system-segment-descriptorbits-fix x))
        (system-segment-descriptorbits->all-zeroes?$inline x)))

Theorem: system-segment-descriptorbits->all-zeroes?$inline-system-segment-descriptorbits-equiv-congruence-on-x

(defthm
 system-segment-descriptorbits->all-zeroes?$inline-system-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (system-segment-descriptorbits-equiv x x-equiv)
  (equal
       (system-segment-descriptorbits->all-zeroes?$inline x)
       (system-segment-descriptorbits->all-zeroes?$inline x-equiv)))
 :rule-classes :congruence)

Theorem: system-segment-descriptorbits->all-zeroes?-of-system-segment-descriptorbits

(defthm
 system-segment-descriptorbits->all-zeroes?-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->all-zeroes?
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (5bits-fix all-zeroes?)))

Theorem: system-segment-descriptorbits->all-zeroes?-of-write-with-mask

(defthm
      system-segment-descriptorbits->all-zeroes?-of-write-with-mask
 (implies
  (and
      (fty::bitstruct-read-over-write-hyps
           x
           system-segment-descriptorbits-equiv-under-mask)
      (system-segment-descriptorbits-equiv-under-mask x y fty::mask)
      (equal (logand (lognot fty::mask)
                     628754697713201783142364789866496)
             0))
  (equal (system-segment-descriptorbits->all-zeroes? x)
         (system-segment-descriptorbits->all-zeroes? y))))

Function: system-segment-descriptorbits->res3$inline

(defun system-segment-descriptorbits->res3$inline (x)
  (declare (xargs :guard (system-segment-descriptorbits-p x)))
  (mbe :logic
       (let ((x (system-segment-descriptorbits-fix x)))
         (part-select x :low 109 :width 19))
       :exec (the (unsigned-byte 19)
                  (logand (the (unsigned-byte 19) 524287)
                          (the (unsigned-byte 19)
                               (ash (the (unsigned-byte 128) x)
                                    -109))))))

Theorem: 19bits-p-of-system-segment-descriptorbits->res3

(defthm 19bits-p-of-system-segment-descriptorbits->res3
  (b* ((res3 (system-segment-descriptorbits->res3$inline x)))
    (19bits-p res3))
  :rule-classes :rewrite)

Theorem: system-segment-descriptorbits->res3$inline-of-system-segment-descriptorbits-fix-x

(defthm
 system-segment-descriptorbits->res3$inline-of-system-segment-descriptorbits-fix-x
 (equal (system-segment-descriptorbits->res3$inline
             (system-segment-descriptorbits-fix x))
        (system-segment-descriptorbits->res3$inline x)))

Theorem: system-segment-descriptorbits->res3$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: system-segment-descriptorbits->res3-of-system-segment-descriptorbits

(defthm
 system-segment-descriptorbits->res3-of-system-segment-descriptorbits
 (equal (system-segment-descriptorbits->res3
             (system-segment-descriptorbits
                  limit15-0 base15-0 base23-16 type
                  s dpl p limit19-16 avl res1 g base31-24
                  base63-32 res2 all-zeroes? res3))
        (19bits-fix res3)))

Theorem: system-segment-descriptorbits->res3-of-write-with-mask

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: !system-segment-descriptorbits->type$inline

(defun !system-segment-descriptorbits->type$inline (type x)
 (declare (xargs :guard (and (4bits-p type)
                             (system-segment-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((type (mbe :logic (4bits-fix type)
                  :exec type))
       (x (system-segment-descriptorbits-fix x)))
    (part-install type x :width 4 :low 40))
  :exec
  (the (unsigned-byte 128)
       (logior (the (unsigned-byte 128)
                    (logand (the (unsigned-byte 128) x)
                            (the (signed-byte 45) -16492674416641)))
               (the (unsigned-byte 44)
                    (ash (the (unsigned-byte 4) type)
                         40))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->type

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

Theorem: !system-segment-descriptorbits->type$inline-of-4bits-fix-type

(defthm
      !system-segment-descriptorbits->type$inline-of-4bits-fix-type
  (equal
       (!system-segment-descriptorbits->type$inline (4bits-fix type)
                                                    x)
       (!system-segment-descriptorbits->type$inline type x)))

Theorem: !system-segment-descriptorbits->type$inline-4bits-equiv-congruence-on-type

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

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

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

Theorem: !system-segment-descriptorbits->type$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: !system-segment-descriptorbits->type-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->type-is-system-segment-descriptorbits
 (equal (!system-segment-descriptorbits->type type x)
        (change-system-segment-descriptorbits x
                                              :type type)))

Theorem: system-segment-descriptorbits->type-of-!system-segment-descriptorbits->type

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

Theorem: !system-segment-descriptorbits->type-equiv-under-mask

(defthm !system-segment-descriptorbits->type-equiv-under-mask
 (b* ((?new-x (!system-segment-descriptorbits->type$inline type x)))
   (system-segment-descriptorbits-equiv-under-mask
        new-x x -16492674416641)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: !system-segment-descriptorbits->res1$inline

(defun !system-segment-descriptorbits->res1$inline (res1 x)
  (declare (xargs :guard (and (2bits-p res1)
                              (system-segment-descriptorbits-p x))))
  (mbe :logic
       (b* ((res1 (mbe :logic (2bits-fix res1)
                       :exec res1))
            (x (system-segment-descriptorbits-fix x)))
         (part-install res1 x :width 2 :low 53))
       :exec (the (unsigned-byte 128)
                  (logior (the (unsigned-byte 128)
                               (logand (the (unsigned-byte 128) x)
                                       (the (signed-byte 56)
                                            -27021597764222977)))
                          (the (unsigned-byte 55)
                               (ash (the (unsigned-byte 2) res1)
                                    53))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->res1

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

Theorem: !system-segment-descriptorbits->res1$inline-of-2bits-fix-res1

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

Theorem: !system-segment-descriptorbits->res1$inline-2bits-equiv-congruence-on-res1

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

Theorem: !system-segment-descriptorbits->res1$inline-of-system-segment-descriptorbits-fix-x

(defthm
 !system-segment-descriptorbits->res1$inline-of-system-segment-descriptorbits-fix-x
 (equal (!system-segment-descriptorbits->res1$inline
             res1
             (system-segment-descriptorbits-fix x))
        (!system-segment-descriptorbits->res1$inline res1 x)))

Theorem: !system-segment-descriptorbits->res1$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: !system-segment-descriptorbits->res1-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->res1-is-system-segment-descriptorbits
 (equal (!system-segment-descriptorbits->res1 res1 x)
        (change-system-segment-descriptorbits x
                                              :res1 res1)))

Theorem: system-segment-descriptorbits->res1-of-!system-segment-descriptorbits->res1

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

Theorem: !system-segment-descriptorbits->res1-equiv-under-mask

(defthm !system-segment-descriptorbits->res1-equiv-under-mask
 (b* ((?new-x (!system-segment-descriptorbits->res1$inline res1 x)))
   (system-segment-descriptorbits-equiv-under-mask
        new-x x -27021597764222977)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Function: !system-segment-descriptorbits->base63-32$inline

(defun !system-segment-descriptorbits->base63-32$inline
       (base63-32 x)
 (declare (xargs :guard (and (32bits-p base63-32)
                             (system-segment-descriptorbits-p x))))
 (mbe
    :logic
    (b* ((base63-32 (mbe :logic (32bits-fix base63-32)
                         :exec base63-32))
         (x (system-segment-descriptorbits-fix x)))
      (part-install base63-32 x
                    :width 32
                    :low 64))
    :exec
    (the (unsigned-byte 128)
         (logior (the (unsigned-byte 128)
                      (logand (the (unsigned-byte 128) x)
                              (the (signed-byte 97)
                                   -79228162495817593519834398721)))
                 (the (unsigned-byte 96)
                      (ash (the (unsigned-byte 32) base63-32)
                           64))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->base63-32

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

Theorem: !system-segment-descriptorbits->base63-32$inline-of-32bits-fix-base63-32

(defthm
 !system-segment-descriptorbits->base63-32$inline-of-32bits-fix-base63-32
 (equal
    (!system-segment-descriptorbits->base63-32$inline
         (32bits-fix base63-32)
         x)
    (!system-segment-descriptorbits->base63-32$inline base63-32 x)))

Theorem: !system-segment-descriptorbits->base63-32$inline-32bits-equiv-congruence-on-base63-32

(defthm
 !system-segment-descriptorbits->base63-32$inline-32bits-equiv-congruence-on-base63-32
 (implies
  (32bits-equiv base63-32 base63-32-equiv)
  (equal
      (!system-segment-descriptorbits->base63-32$inline base63-32 x)
      (!system-segment-descriptorbits->base63-32$inline
           base63-32-equiv x)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->base63-32$inline-of-system-segment-descriptorbits-fix-x

(defthm
 !system-segment-descriptorbits->base63-32$inline-of-system-segment-descriptorbits-fix-x
 (equal
    (!system-segment-descriptorbits->base63-32$inline
         base63-32
         (system-segment-descriptorbits-fix x))
    (!system-segment-descriptorbits->base63-32$inline base63-32 x)))

Theorem: !system-segment-descriptorbits->base63-32$inline-system-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !system-segment-descriptorbits->base63-32$inline-system-segment-descriptorbits-equiv-congruence-on-x
 (implies
  (system-segment-descriptorbits-equiv x x-equiv)
  (equal
      (!system-segment-descriptorbits->base63-32$inline base63-32 x)
      (!system-segment-descriptorbits->base63-32$inline
           base63-32 x-equiv)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->base63-32-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->base63-32-is-system-segment-descriptorbits
 (equal
      (!system-segment-descriptorbits->base63-32 base63-32 x)
      (change-system-segment-descriptorbits x
                                            :base63-32 base63-32)))

Theorem: system-segment-descriptorbits->base63-32-of-!system-segment-descriptorbits->base63-32

(defthm
 system-segment-descriptorbits->base63-32-of-!system-segment-descriptorbits->base63-32
 (b*
  ((?new-x
    (!system-segment-descriptorbits->base63-32$inline base63-32 x)))
  (equal (system-segment-descriptorbits->base63-32 new-x)
         (32bits-fix base63-32))))

Theorem: !system-segment-descriptorbits->base63-32-equiv-under-mask

(defthm !system-segment-descriptorbits->base63-32-equiv-under-mask
 (b*
  ((?new-x
    (!system-segment-descriptorbits->base63-32$inline base63-32 x)))
  (system-segment-descriptorbits-equiv-under-mask
       new-x
       x -79228162495817593519834398721)))

Function: !system-segment-descriptorbits->res2$inline

(defun !system-segment-descriptorbits->res2$inline (res2 x)
 (declare (xargs :guard (and (8bits-p res2)
                             (system-segment-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((res2 (mbe :logic (8bits-fix res2)
                  :exec res2))
       (x (system-segment-descriptorbits-fix x)))
    (part-install res2 x :width 8 :low 96))
  :exec
  (the
      (unsigned-byte 128)
      (logior (the (unsigned-byte 128)
                   (logand (the (unsigned-byte 128) x)
                           (the (signed-byte 105)
                                -20203181441137406086353707335681)))
              (the (unsigned-byte 104)
                   (ash (the (unsigned-byte 8) res2)
                        96))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->res2

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

Theorem: !system-segment-descriptorbits->res2$inline-of-8bits-fix-res2

(defthm
      !system-segment-descriptorbits->res2$inline-of-8bits-fix-res2
  (equal
       (!system-segment-descriptorbits->res2$inline (8bits-fix res2)
                                                    x)
       (!system-segment-descriptorbits->res2$inline res2 x)))

Theorem: !system-segment-descriptorbits->res2$inline-8bits-equiv-congruence-on-res2

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

Theorem: !system-segment-descriptorbits->res2$inline-of-system-segment-descriptorbits-fix-x

(defthm
 !system-segment-descriptorbits->res2$inline-of-system-segment-descriptorbits-fix-x
 (equal (!system-segment-descriptorbits->res2$inline
             res2
             (system-segment-descriptorbits-fix x))
        (!system-segment-descriptorbits->res2$inline res2 x)))

Theorem: !system-segment-descriptorbits->res2$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: !system-segment-descriptorbits->res2-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->res2-is-system-segment-descriptorbits
 (equal (!system-segment-descriptorbits->res2 res2 x)
        (change-system-segment-descriptorbits x
                                              :res2 res2)))

Theorem: system-segment-descriptorbits->res2-of-!system-segment-descriptorbits->res2

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

Theorem: !system-segment-descriptorbits->res2-equiv-under-mask

(defthm !system-segment-descriptorbits->res2-equiv-under-mask
 (b* ((?new-x (!system-segment-descriptorbits->res2$inline res2 x)))
   (system-segment-descriptorbits-equiv-under-mask
        new-x
        x -20203181441137406086353707335681)))

Function: !system-segment-descriptorbits->all-zeroes?$inline

(defun !system-segment-descriptorbits->all-zeroes?$inline
       (all-zeroes? x)
 (declare (xargs :guard (and (5bits-p all-zeroes?)
                             (system-segment-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((all-zeroes? (mbe :logic (5bits-fix all-zeroes?)
                         :exec all-zeroes?))
       (x (system-segment-descriptorbits-fix x)))
    (part-install all-zeroes? x
                  :width 5
                  :low 104))
  :exec
  (the
     (unsigned-byte 128)
     (logior (the (unsigned-byte 128)
                  (logand (the (unsigned-byte 128) x)
                          (the (signed-byte 110)
                               -628754697713201783142364789866497)))
             (the (unsigned-byte 109)
                  (ash (the (unsigned-byte 5) all-zeroes?)
                       104))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->all-zeroes?

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

Theorem: !system-segment-descriptorbits->all-zeroes?$inline-of-5bits-fix-all-zeroes?

(defthm
 !system-segment-descriptorbits->all-zeroes?$inline-of-5bits-fix-all-zeroes?
 (equal (!system-segment-descriptorbits->all-zeroes?$inline
             (5bits-fix all-zeroes?)
             x)
        (!system-segment-descriptorbits->all-zeroes?$inline
             all-zeroes? x)))

Theorem: !system-segment-descriptorbits->all-zeroes?$inline-5bits-equiv-congruence-on-all-zeroes?

(defthm
 !system-segment-descriptorbits->all-zeroes?$inline-5bits-equiv-congruence-on-all-zeroes?
 (implies (5bits-equiv all-zeroes? all-zeroes?-equiv)
          (equal (!system-segment-descriptorbits->all-zeroes?$inline
                      all-zeroes? x)
                 (!system-segment-descriptorbits->all-zeroes?$inline
                      all-zeroes?-equiv x)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->all-zeroes?$inline-of-system-segment-descriptorbits-fix-x

(defthm
 !system-segment-descriptorbits->all-zeroes?$inline-of-system-segment-descriptorbits-fix-x
 (equal (!system-segment-descriptorbits->all-zeroes?$inline
             all-zeroes?
             (system-segment-descriptorbits-fix x))
        (!system-segment-descriptorbits->all-zeroes?$inline
             all-zeroes? x)))

Theorem: !system-segment-descriptorbits->all-zeroes?$inline-system-segment-descriptorbits-equiv-congruence-on-x

(defthm
 !system-segment-descriptorbits->all-zeroes?$inline-system-segment-descriptorbits-equiv-congruence-on-x
 (implies (system-segment-descriptorbits-equiv x x-equiv)
          (equal (!system-segment-descriptorbits->all-zeroes?$inline
                      all-zeroes? x)
                 (!system-segment-descriptorbits->all-zeroes?$inline
                      all-zeroes? x-equiv)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->all-zeroes?-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->all-zeroes?-is-system-segment-descriptorbits
 (equal
   (!system-segment-descriptorbits->all-zeroes? all-zeroes? x)
   (change-system-segment-descriptorbits x
                                         :all-zeroes? all-zeroes?)))

Theorem: system-segment-descriptorbits->all-zeroes?-of-!system-segment-descriptorbits->all-zeroes?

(defthm
 system-segment-descriptorbits->all-zeroes?-of-!system-segment-descriptorbits->all-zeroes?
 (b* ((?new-x (!system-segment-descriptorbits->all-zeroes?$inline
                   all-zeroes? x)))
   (equal (system-segment-descriptorbits->all-zeroes? new-x)
          (5bits-fix all-zeroes?))))

Theorem: !system-segment-descriptorbits->all-zeroes?-equiv-under-mask

(defthm !system-segment-descriptorbits->all-zeroes?-equiv-under-mask
  (b* ((?new-x (!system-segment-descriptorbits->all-zeroes?$inline
                    all-zeroes? x)))
    (system-segment-descriptorbits-equiv-under-mask
         new-x
         x -628754697713201783142364789866497)))

Function: !system-segment-descriptorbits->res3$inline

(defun !system-segment-descriptorbits->res3$inline (res3 x)
 (declare (xargs :guard (and (19bits-p res3)
                             (system-segment-descriptorbits-p x))))
 (mbe
  :logic
  (b* ((res3 (mbe :logic (19bits-fix res3)
                  :exec res3))
       (x (system-segment-descriptorbits-fix x)))
    (part-install res3 x
                  :width 19
                  :low 109))
  :exec
  (the
   (unsigned-byte 128)
   (logior
       (the (unsigned-byte 128)
            (logand (the (unsigned-byte 128) x)
                    (the (signed-byte 129)
                         -340281717883831146609921041119727058945)))
       (the (unsigned-byte 128)
            (ash (the (unsigned-byte 19) res3)
                 109))))))

Theorem: system-segment-descriptorbits-p-of-!system-segment-descriptorbits->res3

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

Theorem: !system-segment-descriptorbits->res3$inline-of-19bits-fix-res3

(defthm
     !system-segment-descriptorbits->res3$inline-of-19bits-fix-res3
 (equal
      (!system-segment-descriptorbits->res3$inline (19bits-fix res3)
                                                   x)
      (!system-segment-descriptorbits->res3$inline res3 x)))

Theorem: !system-segment-descriptorbits->res3$inline-19bits-equiv-congruence-on-res3

(defthm
 !system-segment-descriptorbits->res3$inline-19bits-equiv-congruence-on-res3
 (implies
   (19bits-equiv res3 res3-equiv)
   (equal
        (!system-segment-descriptorbits->res3$inline res3 x)
        (!system-segment-descriptorbits->res3$inline res3-equiv x)))
 :rule-classes :congruence)

Theorem: !system-segment-descriptorbits->res3$inline-of-system-segment-descriptorbits-fix-x

(defthm
 !system-segment-descriptorbits->res3$inline-of-system-segment-descriptorbits-fix-x
 (equal (!system-segment-descriptorbits->res3$inline
             res3
             (system-segment-descriptorbits-fix x))
        (!system-segment-descriptorbits->res3$inline res3 x)))

Theorem: !system-segment-descriptorbits->res3$inline-system-segment-descriptorbits-equiv-congruence-on-x

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

Theorem: !system-segment-descriptorbits->res3-is-system-segment-descriptorbits

(defthm
 !system-segment-descriptorbits->res3-is-system-segment-descriptorbits
 (equal (!system-segment-descriptorbits->res3 res3 x)
        (change-system-segment-descriptorbits x
                                              :res3 res3)))

Theorem: system-segment-descriptorbits->res3-of-!system-segment-descriptorbits->res3

(defthm
 system-segment-descriptorbits->res3-of-!system-segment-descriptorbits->res3
 (b* ((?new-x (!system-segment-descriptorbits->res3$inline res3 x)))
   (equal (system-segment-descriptorbits->res3 new-x)
          (19bits-fix res3))))

Theorem: !system-segment-descriptorbits->res3-equiv-under-mask

(defthm !system-segment-descriptorbits->res3-equiv-under-mask
 (b* ((?new-x (!system-segment-descriptorbits->res3$inline res3 x)))
   (system-segment-descriptorbits-equiv-under-mask
        new-x
        x 649037107316853453566312041152511)))

Function: system-segment-descriptorbits-debug

(defun system-segment-descriptorbits-debug (x)
 (declare (xargs :guard (system-segment-descriptorbits-p x)))
 (let ((__function__ 'system-segment-descriptorbits-debug))
  (declare (ignorable __function__))
  (b* (((system-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 'type x.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 'res1 x.res1)
             (cons
              (cons 'g x.g)
              (cons
                 (cons 'base31-24 x.base31-24)
                 (cons (cons 'base63-32 x.base63-32)
                       (cons (cons 'res2 x.res2)
                             (cons (cons 'all-zeroes? x.all-zeroes?)
                                   (cons (cons 'res3 x.res3)
                                         nil)))))))))))))))))))

Subtopics

System-segment-descriptorbits-p: Recognizer for system-segment-descriptorbits bit structures.
!system-segment-descriptorbits->all-zeroes?: Update the |X86ISA|::|ALL-ZEROES?| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->limit19-16: Update the |X86ISA|::|LIMIT19-16| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->base63-32: Update the |X86ISA|::|BASE63-32| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->base31-24: Update the |X86ISA|::|BASE31-24| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->limit15-0: Update the |X86ISA|::|LIMIT15-0| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->base23-16: Update the |X86ISA|::|BASE23-16| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->base15-0: Update the |X86ISA|::|BASE15-0| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->res3: Update the |X86ISA|::|RES3| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->res2: Update the |X86ISA|::|RES2| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->res1: Update the |X86ISA|::|RES1| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->type: Update the |COMMON-LISP|::|TYPE| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->dpl: Update the |X86ISA|::|DPL| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->avl: Update the |X86ISA|::|AVL| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->s: Update the |X86ISA|::|S| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->p: Update the |ACL2|::|P| field of a system-segment-descriptorbits bit structure.
!system-segment-descriptorbits->g: Update the |X86ISA|::|G| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->limit19-16: Access the |X86ISA|::|LIMIT19-16| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->all-zeroes?: Access the |X86ISA|::|ALL-ZEROES?| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits-fix: Fixing function for system-segment-descriptorbits bit structures.
System-segment-descriptorbits->limit15-0: Access the |X86ISA|::|LIMIT15-0| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->base63-32: Access the |X86ISA|::|BASE63-32| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->base31-24: Access the |X86ISA|::|BASE31-24| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->base23-16: Access the |X86ISA|::|BASE23-16| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->base15-0: Access the |X86ISA|::|BASE15-0| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->type: Access the |COMMON-LISP|::|TYPE| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->res3: Access the |X86ISA|::|RES3| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->res2: Access the |X86ISA|::|RES2| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->res1: Access the |X86ISA|::|RES1| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->s: Access the |X86ISA|::|S| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->g: Access the |X86ISA|::|G| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->dpl: Access the |X86ISA|::|DPL| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->avl: Access the |X86ISA|::|AVL| field of a system-segment-descriptorbits bit structure.
System-segment-descriptorbits->p: Access the |ACL2|::|P| field of a system-segment-descriptorbits bit structure.