Subset of data-segment-descriptorBits.
This is a bitstruct type introduced by defbitstruct, represented as a unsigned 16-bit integer.
Function:
(defun data-segment-descriptor-attributesbits-p (x) (declare (xargs :guard t)) (let ((__function__ 'data-segment-descriptor-attributesbits-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 16 x) :exec (and (natp x) (< x 65536)))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-when-unsigned-byte-p (implies (unsigned-byte-p 16 x) (data-segment-descriptor-attributesbits-p x)))
Theorem:
(defthm unsigned-byte-p-when-data-segment-descriptor-attributesbits-p (implies (data-segment-descriptor-attributesbits-p x) (unsigned-byte-p 16 x)))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-compound-recognizer (implies (data-segment-descriptor-attributesbits-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun data-segment-descriptor-attributesbits-fix (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (let ((__function__ 'data-segment-descriptor-attributesbits-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 16 x) :exec x)))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-data-segment-descriptor-attributesbits-fix (b* ((fty::fixed (data-segment-descriptor-attributesbits-fix x))) (data-segment-descriptor-attributesbits-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits-fix-when-data-segment-descriptor-attributesbits-p (implies (data-segment-descriptor-attributesbits-p x) (equal (data-segment-descriptor-attributesbits-fix x) x)))
Function:
(defun data-segment-descriptor-attributesbits-equiv$inline (x y) (declare (xargs :guard (and (data-segment-descriptor-attributesbits-p x) (data-segment-descriptor-attributesbits-p y)))) (equal (data-segment-descriptor-attributesbits-fix x) (data-segment-descriptor-attributesbits-fix y)))
Theorem:
(defthm data-segment-descriptor-attributesbits-equiv-is-an-equivalence (and (booleanp (data-segment-descriptor-attributesbits-equiv x y)) (data-segment-descriptor-attributesbits-equiv x x) (implies (data-segment-descriptor-attributesbits-equiv x y) (data-segment-descriptor-attributesbits-equiv y x)) (implies (and (data-segment-descriptor-attributesbits-equiv x y) (data-segment-descriptor-attributesbits-equiv y z)) (data-segment-descriptor-attributesbits-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm data-segment-descriptor-attributesbits-equiv-implies-equal-data-segment-descriptor-attributesbits-fix-1 (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits-fix x) (data-segment-descriptor-attributesbits-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm data-segment-descriptor-attributesbits-fix-under-data-segment-descriptor-attributesbits-equiv (data-segment-descriptor-attributesbits-equiv (data-segment-descriptor-attributesbits-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(defun data-segment-descriptor-attributesbits (a w e msb-of-type s dpl p avl l d/b g unknownbits) (declare (xargs :guard (and (bitp a) (bitp w) (bitp e) (bitp msb-of-type) (bitp s) (2bits-p dpl) (bitp p) (bitp avl) (bitp l) (bitp d/b) (bitp g) (4bits-p unknownbits)))) (let ((__function__ 'data-segment-descriptor-attributesbits)) (declare (ignorable __function__)) (b* ((a (mbe :logic (bfix a) :exec a)) (w (mbe :logic (bfix w) :exec w)) (e (mbe :logic (bfix e) :exec e)) (msb-of-type (mbe :logic (bfix msb-of-type) :exec msb-of-type)) (s (mbe :logic (bfix s) :exec s)) (dpl (mbe :logic (2bits-fix dpl) :exec dpl)) (p (mbe :logic (bfix p) :exec p)) (avl (mbe :logic (bfix avl) :exec avl)) (l (mbe :logic (bfix l) :exec l)) (d/b (mbe :logic (bfix d/b) :exec d/b)) (g (mbe :logic (bfix g) :exec g)) (unknownbits (mbe :logic (4bits-fix unknownbits) :exec unknownbits))) (logapp 1 a (logapp 1 w (logapp 1 e (logapp 1 msb-of-type (logapp 1 s (logapp 2 dpl (logapp 1 p (logapp 1 avl (logapp 1 l (logapp 1 d/b (logapp 1 g unknownbits))))))))))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-data-segment-descriptor-attributesbits (b* ((data-segment-descriptor-attributesbits (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits))) (data-segment-descriptor-attributesbits-p data-segment-descriptor-attributesbits)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-a (equal (data-segment-descriptor-attributesbits (bfix a) w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-a (implies (bit-equiv a a-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a-equiv w e msb-of-type s dpl p avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-w (equal (data-segment-descriptor-attributesbits a (bfix w) e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-w (implies (bit-equiv w w-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w-equiv e msb-of-type s dpl p avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-e (equal (data-segment-descriptor-attributesbits a w (bfix e) msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-e (implies (bit-equiv e e-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e-equiv msb-of-type s dpl p avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-msb-of-type (equal (data-segment-descriptor-attributesbits a w e (bfix msb-of-type) s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-msb-of-type (implies (bit-equiv msb-of-type msb-of-type-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type-equiv s dpl p avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-s (equal (data-segment-descriptor-attributesbits a w e msb-of-type (bfix s) dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-s (implies (bit-equiv s s-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s-equiv dpl p avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-2bits-fix-dpl (equal (data-segment-descriptor-attributesbits a w e msb-of-type s (2bits-fix dpl) p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-2bits-equiv-congruence-on-dpl (implies (2bits-equiv dpl dpl-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl-equiv p avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-p (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl (bfix p) avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-p (implies (bit-equiv p p-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p-equiv avl l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-avl (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p (bfix avl) l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-avl (implies (bit-equiv avl avl-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl-equiv l d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-l (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl (bfix l) d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-l (implies (bit-equiv l l-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l-equiv d/b g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-d/b (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l (bfix d/b) g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-d/b (implies (bit-equiv d/b d/b-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b-equiv g unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-bfix-g (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b (bfix g) unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-bit-equiv-congruence-on-g (implies (bit-equiv g g-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g-equiv unknownbits))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits-of-4bits-fix-unknownbits (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g (4bits-fix unknownbits)) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits-4bits-equiv-congruence-on-unknownbits (implies (4bits-equiv unknownbits unknownbits-equiv) (equal (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits) (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits-equiv))) :rule-classes :congruence)
Function:
(defun data-segment-descriptor-attributesbits-equiv-under-mask (x x1 mask) (declare (xargs :guard (and (data-segment-descriptor-attributesbits-p x) (data-segment-descriptor-attributesbits-p x1) (integerp mask)))) (let ((__function__ 'data-segment-descriptor-attributesbits-equiv-under-mask)) (declare (ignorable __function__)) (fty::int-equiv-under-mask (data-segment-descriptor-attributesbits-fix x) (data-segment-descriptor-attributesbits-fix x1) mask)))
Function:
(defun data-segment-descriptor-attributesbits->a$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 0 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 16) x)))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->a (b* ((a (data-segment-descriptor-attributesbits->a$inline x))) (bitp a)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->a$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->a$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->a$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->a$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->a$inline x) (data-segment-descriptor-attributesbits->a$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->a-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->a (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix a)))
Theorem:
(defthm data-segment-descriptor-attributesbits->a-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 1) 0)) (equal (data-segment-descriptor-attributesbits->a x) (data-segment-descriptor-attributesbits->a y))))
Function:
(defun data-segment-descriptor-attributesbits->w$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 1 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 15) (ash (the (unsigned-byte 16) x) -1))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->w (b* ((w (data-segment-descriptor-attributesbits->w$inline x))) (bitp w)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->w$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->w$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->w$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->w$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->w$inline x) (data-segment-descriptor-attributesbits->w$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->w-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->w (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix w)))
Theorem:
(defthm data-segment-descriptor-attributesbits->w-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 2) 0)) (equal (data-segment-descriptor-attributesbits->w x) (data-segment-descriptor-attributesbits->w y))))
Function:
(defun data-segment-descriptor-attributesbits->e$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 2 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 14) (ash (the (unsigned-byte 16) x) -2))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->e (b* ((e (data-segment-descriptor-attributesbits->e$inline x))) (bitp e)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->e$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->e$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->e$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->e$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->e$inline x) (data-segment-descriptor-attributesbits->e$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->e-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->e (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix e)))
Theorem:
(defthm data-segment-descriptor-attributesbits->e-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 4) 0)) (equal (data-segment-descriptor-attributesbits->e x) (data-segment-descriptor-attributesbits->e y))))
Function:
(defun data-segment-descriptor-attributesbits->msb-of-type$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 3 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 13) (ash (the (unsigned-byte 16) x) -3))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->msb-of-type (b* ((msb-of-type (data-segment-descriptor-attributesbits->msb-of-type$inline x))) (bitp msb-of-type)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->msb-of-type$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->msb-of-type$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->msb-of-type$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->msb-of-type$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->msb-of-type$inline x) (data-segment-descriptor-attributesbits->msb-of-type$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->msb-of-type-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->msb-of-type (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix msb-of-type)))
Theorem:
(defthm data-segment-descriptor-attributesbits->msb-of-type-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 8) 0)) (equal (data-segment-descriptor-attributesbits->msb-of-type x) (data-segment-descriptor-attributesbits->msb-of-type y))))
Function:
(defun data-segment-descriptor-attributesbits->s$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 4 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 12) (ash (the (unsigned-byte 16) x) -4))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->s (b* ((s (data-segment-descriptor-attributesbits->s$inline x))) (bitp s)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->s$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->s$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->s$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->s$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->s$inline x) (data-segment-descriptor-attributesbits->s$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->s-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->s (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix s)))
Theorem:
(defthm data-segment-descriptor-attributesbits->s-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 16) 0)) (equal (data-segment-descriptor-attributesbits->s x) (data-segment-descriptor-attributesbits->s y))))
Function:
(defun data-segment-descriptor-attributesbits->dpl$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 5 :width 2)) :exec (the (unsigned-byte 2) (logand (the (unsigned-byte 2) 3) (the (unsigned-byte 11) (ash (the (unsigned-byte 16) x) -5))))))
Theorem:
(defthm 2bits-p-of-data-segment-descriptor-attributesbits->dpl (b* ((dpl (data-segment-descriptor-attributesbits->dpl$inline x))) (2bits-p dpl)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->dpl$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->dpl$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->dpl$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->dpl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->dpl$inline x) (data-segment-descriptor-attributesbits->dpl$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->dpl-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->dpl (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (2bits-fix dpl)))
Theorem:
(defthm data-segment-descriptor-attributesbits->dpl-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 96) 0)) (equal (data-segment-descriptor-attributesbits->dpl x) (data-segment-descriptor-attributesbits->dpl y))))
Function:
(defun data-segment-descriptor-attributesbits->p$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 7 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 9) (ash (the (unsigned-byte 16) x) -7))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->p (b* ((p (data-segment-descriptor-attributesbits->p$inline x))) (bitp p)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->p$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->p$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->p$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->p$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->p$inline x) (data-segment-descriptor-attributesbits->p$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->p-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->p (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix p)))
Theorem:
(defthm data-segment-descriptor-attributesbits->p-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 128) 0)) (equal (data-segment-descriptor-attributesbits->p x) (data-segment-descriptor-attributesbits->p y))))
Function:
(defun data-segment-descriptor-attributesbits->avl$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 8 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 8) (ash (the (unsigned-byte 16) x) -8))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->avl (b* ((avl (data-segment-descriptor-attributesbits->avl$inline x))) (bitp avl)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->avl$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->avl$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->avl$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->avl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->avl$inline x) (data-segment-descriptor-attributesbits->avl$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->avl-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->avl (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix avl)))
Theorem:
(defthm data-segment-descriptor-attributesbits->avl-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 256) 0)) (equal (data-segment-descriptor-attributesbits->avl x) (data-segment-descriptor-attributesbits->avl y))))
Function:
(defun data-segment-descriptor-attributesbits->l$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 9 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 7) (ash (the (unsigned-byte 16) x) -9))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->l (b* ((l (data-segment-descriptor-attributesbits->l$inline x))) (bitp l)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->l$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->l$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->l$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->l$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->l$inline x) (data-segment-descriptor-attributesbits->l$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->l-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->l (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix l)))
Theorem:
(defthm data-segment-descriptor-attributesbits->l-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 512) 0)) (equal (data-segment-descriptor-attributesbits->l x) (data-segment-descriptor-attributesbits->l y))))
Function:
(defun data-segment-descriptor-attributesbits->d/b$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 10 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 6) (ash (the (unsigned-byte 16) x) -10))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->d/b (b* ((d/b (data-segment-descriptor-attributesbits->d/b$inline x))) (bitp d/b)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->d/b$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->d/b$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->d/b$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->d/b$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->d/b$inline x) (data-segment-descriptor-attributesbits->d/b$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->d/b-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->d/b (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix d/b)))
Theorem:
(defthm data-segment-descriptor-attributesbits->d/b-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 1024) 0)) (equal (data-segment-descriptor-attributesbits->d/b x) (data-segment-descriptor-attributesbits->d/b y))))
Function:
(defun data-segment-descriptor-attributesbits->g$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 11 :width 1)) :exec (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 5) (ash (the (unsigned-byte 16) x) -11))))))
Theorem:
(defthm bitp-of-data-segment-descriptor-attributesbits->g (b* ((g (data-segment-descriptor-attributesbits->g$inline x))) (bitp g)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->g$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->g$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->g$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->g$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->g$inline x) (data-segment-descriptor-attributesbits->g$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->g-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->g (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (bfix g)))
Theorem:
(defthm data-segment-descriptor-attributesbits->g-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 2048) 0)) (equal (data-segment-descriptor-attributesbits->g x) (data-segment-descriptor-attributesbits->g y))))
Function:
(defun data-segment-descriptor-attributesbits->unknownbits$inline (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (mbe :logic (let ((x (data-segment-descriptor-attributesbits-fix x))) (part-select x :low 12 :width 4)) :exec (the (unsigned-byte 4) (logand (the (unsigned-byte 4) 15) (the (unsigned-byte 4) (ash (the (unsigned-byte 16) x) -12))))))
Theorem:
(defthm 4bits-p-of-data-segment-descriptor-attributesbits->unknownbits (b* ((unknownbits (data-segment-descriptor-attributesbits->unknownbits$inline x))) (4bits-p unknownbits)) :rule-classes :rewrite)
Theorem:
(defthm data-segment-descriptor-attributesbits->unknownbits$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (data-segment-descriptor-attributesbits->unknownbits$inline (data-segment-descriptor-attributesbits-fix x)) (data-segment-descriptor-attributesbits->unknownbits$inline x)))
Theorem:
(defthm data-segment-descriptor-attributesbits->unknownbits$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (data-segment-descriptor-attributesbits->unknownbits$inline x) (data-segment-descriptor-attributesbits->unknownbits$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm data-segment-descriptor-attributesbits->unknownbits-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits->unknownbits (data-segment-descriptor-attributesbits a w e msb-of-type s dpl p avl l d/b g unknownbits)) (4bits-fix unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits->unknownbits-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x data-segment-descriptor-attributesbits-equiv-under-mask) (data-segment-descriptor-attributesbits-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 61440) 0)) (equal (data-segment-descriptor-attributesbits->unknownbits x) (data-segment-descriptor-attributesbits->unknownbits y))))
Theorem:
(defthm data-segment-descriptor-attributesbits-fix-in-terms-of-data-segment-descriptor-attributesbits (equal (data-segment-descriptor-attributesbits-fix x) (change-data-segment-descriptor-attributesbits x)))
Function:
(defun !data-segment-descriptor-attributesbits->a$inline (a x) (declare (xargs :guard (and (bitp a) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((a (mbe :logic (bfix a) :exec a)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install a x :width 1 :low 0)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 2) -2))) (the (unsigned-byte 1) a)))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->a (b* ((new-x (!data-segment-descriptor-attributesbits->a$inline a x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->a$inline-of-bfix-a (equal (!data-segment-descriptor-attributesbits->a$inline (bfix a) x) (!data-segment-descriptor-attributesbits->a$inline a x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->a$inline-bit-equiv-congruence-on-a (implies (bit-equiv a a-equiv) (equal (!data-segment-descriptor-attributesbits->a$inline a x) (!data-segment-descriptor-attributesbits->a$inline a-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->a$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->a$inline a (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->a$inline a x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->a$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->a$inline a x) (!data-segment-descriptor-attributesbits->a$inline a x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->a-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->a a x) (change-data-segment-descriptor-attributesbits x :a a)))
Theorem:
(defthm data-segment-descriptor-attributesbits->a-of-!data-segment-descriptor-attributesbits->a (b* ((?new-x (!data-segment-descriptor-attributesbits->a$inline a x))) (equal (data-segment-descriptor-attributesbits->a new-x) (bfix a))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->a-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->a$inline a x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -2)))
Function:
(defun !data-segment-descriptor-attributesbits->w$inline (w x) (declare (xargs :guard (and (bitp w) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((w (mbe :logic (bfix w) :exec w)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install w x :width 1 :low 1)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 3) -3))) (the (unsigned-byte 2) (ash (the (unsigned-byte 1) w) 1))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->w (b* ((new-x (!data-segment-descriptor-attributesbits->w$inline w x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->w$inline-of-bfix-w (equal (!data-segment-descriptor-attributesbits->w$inline (bfix w) x) (!data-segment-descriptor-attributesbits->w$inline w x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->w$inline-bit-equiv-congruence-on-w (implies (bit-equiv w w-equiv) (equal (!data-segment-descriptor-attributesbits->w$inline w x) (!data-segment-descriptor-attributesbits->w$inline w-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->w$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->w$inline w (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->w$inline w x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->w$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->w$inline w x) (!data-segment-descriptor-attributesbits->w$inline w x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->w-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->w w x) (change-data-segment-descriptor-attributesbits x :w w)))
Theorem:
(defthm data-segment-descriptor-attributesbits->w-of-!data-segment-descriptor-attributesbits->w (b* ((?new-x (!data-segment-descriptor-attributesbits->w$inline w x))) (equal (data-segment-descriptor-attributesbits->w new-x) (bfix w))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->w-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->w$inline w x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -3)))
Function:
(defun !data-segment-descriptor-attributesbits->e$inline (e x) (declare (xargs :guard (and (bitp e) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((e (mbe :logic (bfix e) :exec e)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install e x :width 1 :low 2)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 4) -5))) (the (unsigned-byte 3) (ash (the (unsigned-byte 1) e) 2))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->e (b* ((new-x (!data-segment-descriptor-attributesbits->e$inline e x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->e$inline-of-bfix-e (equal (!data-segment-descriptor-attributesbits->e$inline (bfix e) x) (!data-segment-descriptor-attributesbits->e$inline e x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->e$inline-bit-equiv-congruence-on-e (implies (bit-equiv e e-equiv) (equal (!data-segment-descriptor-attributesbits->e$inline e x) (!data-segment-descriptor-attributesbits->e$inline e-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->e$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->e$inline e (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->e$inline e x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->e$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->e$inline e x) (!data-segment-descriptor-attributesbits->e$inline e x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->e-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->e e x) (change-data-segment-descriptor-attributesbits x :e e)))
Theorem:
(defthm data-segment-descriptor-attributesbits->e-of-!data-segment-descriptor-attributesbits->e (b* ((?new-x (!data-segment-descriptor-attributesbits->e$inline e x))) (equal (data-segment-descriptor-attributesbits->e new-x) (bfix e))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->e-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->e$inline e x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -5)))
Function:
(defun !data-segment-descriptor-attributesbits->msb-of-type$inline (msb-of-type x) (declare (xargs :guard (and (bitp msb-of-type) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((msb-of-type (mbe :logic (bfix msb-of-type) :exec msb-of-type)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install msb-of-type x :width 1 :low 3)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 5) -9))) (the (unsigned-byte 4) (ash (the (unsigned-byte 1) msb-of-type) 3))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->msb-of-type (b* ((new-x (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->msb-of-type$inline-of-bfix-msb-of-type (equal (!data-segment-descriptor-attributesbits->msb-of-type$inline (bfix msb-of-type) x) (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->msb-of-type$inline-bit-equiv-congruence-on-msb-of-type (implies (bit-equiv msb-of-type msb-of-type-equiv) (equal (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x) (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->msb-of-type$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->msb-of-type$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x) (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->msb-of-type-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->msb-of-type msb-of-type x) (change-data-segment-descriptor-attributesbits x :msb-of-type msb-of-type)))
Theorem:
(defthm data-segment-descriptor-attributesbits->msb-of-type-of-!data-segment-descriptor-attributesbits->msb-of-type (b* ((?new-x (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x))) (equal (data-segment-descriptor-attributesbits->msb-of-type new-x) (bfix msb-of-type))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->msb-of-type-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->msb-of-type$inline msb-of-type x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -9)))
Function:
(defun !data-segment-descriptor-attributesbits->s$inline (s x) (declare (xargs :guard (and (bitp s) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((s (mbe :logic (bfix s) :exec s)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install s x :width 1 :low 4)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) s) 4))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->s (b* ((new-x (!data-segment-descriptor-attributesbits->s$inline s x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->s$inline-of-bfix-s (equal (!data-segment-descriptor-attributesbits->s$inline (bfix s) x) (!data-segment-descriptor-attributesbits->s$inline s x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->s$inline-bit-equiv-congruence-on-s (implies (bit-equiv s s-equiv) (equal (!data-segment-descriptor-attributesbits->s$inline s x) (!data-segment-descriptor-attributesbits->s$inline s-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->s$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->s$inline s (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->s$inline s x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->s$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->s$inline s x) (!data-segment-descriptor-attributesbits->s$inline s x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->s-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->s s x) (change-data-segment-descriptor-attributesbits x :s s)))
Theorem:
(defthm data-segment-descriptor-attributesbits->s-of-!data-segment-descriptor-attributesbits->s (b* ((?new-x (!data-segment-descriptor-attributesbits->s$inline s x))) (equal (data-segment-descriptor-attributesbits->s new-x) (bfix s))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->s-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->s$inline s x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -17)))
Function:
(defun !data-segment-descriptor-attributesbits->dpl$inline (dpl x) (declare (xargs :guard (and (2bits-p dpl) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((dpl (mbe :logic (2bits-fix dpl) :exec dpl)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install dpl x :width 2 :low 5)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 8) -97))) (the (unsigned-byte 7) (ash (the (unsigned-byte 2) dpl) 5))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->dpl (b* ((new-x (!data-segment-descriptor-attributesbits->dpl$inline dpl x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->dpl$inline-of-2bits-fix-dpl (equal (!data-segment-descriptor-attributesbits->dpl$inline (2bits-fix dpl) x) (!data-segment-descriptor-attributesbits->dpl$inline dpl x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->dpl$inline-2bits-equiv-congruence-on-dpl (implies (2bits-equiv dpl dpl-equiv) (equal (!data-segment-descriptor-attributesbits->dpl$inline dpl x) (!data-segment-descriptor-attributesbits->dpl$inline dpl-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->dpl$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->dpl$inline dpl (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->dpl$inline dpl x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->dpl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->dpl$inline dpl x) (!data-segment-descriptor-attributesbits->dpl$inline dpl x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->dpl-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->dpl dpl x) (change-data-segment-descriptor-attributesbits x :dpl dpl)))
Theorem:
(defthm data-segment-descriptor-attributesbits->dpl-of-!data-segment-descriptor-attributesbits->dpl (b* ((?new-x (!data-segment-descriptor-attributesbits->dpl$inline dpl x))) (equal (data-segment-descriptor-attributesbits->dpl new-x) (2bits-fix dpl))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->dpl-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->dpl$inline dpl x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -97)))
Function:
(defun !data-segment-descriptor-attributesbits->p$inline (p x) (declare (xargs :guard (and (bitp p) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((p (mbe :logic (bfix p) :exec p)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install p x :width 1 :low 7)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 9) -129))) (the (unsigned-byte 8) (ash (the (unsigned-byte 1) p) 7))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->p (b* ((new-x (!data-segment-descriptor-attributesbits->p$inline p x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->p$inline-of-bfix-p (equal (!data-segment-descriptor-attributesbits->p$inline (bfix p) x) (!data-segment-descriptor-attributesbits->p$inline p x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->p$inline-bit-equiv-congruence-on-p (implies (bit-equiv p p-equiv) (equal (!data-segment-descriptor-attributesbits->p$inline p x) (!data-segment-descriptor-attributesbits->p$inline p-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->p$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->p$inline p (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->p$inline p x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->p$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->p$inline p x) (!data-segment-descriptor-attributesbits->p$inline p x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->p-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->p p x) (change-data-segment-descriptor-attributesbits x :p p)))
Theorem:
(defthm data-segment-descriptor-attributesbits->p-of-!data-segment-descriptor-attributesbits->p (b* ((?new-x (!data-segment-descriptor-attributesbits->p$inline p x))) (equal (data-segment-descriptor-attributesbits->p new-x) (bfix p))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->p-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->p$inline p x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -129)))
Function:
(defun !data-segment-descriptor-attributesbits->avl$inline (avl x) (declare (xargs :guard (and (bitp avl) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((avl (mbe :logic (bfix avl) :exec avl)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install avl x :width 1 :low 8)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 10) -257))) (the (unsigned-byte 9) (ash (the (unsigned-byte 1) avl) 8))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->avl (b* ((new-x (!data-segment-descriptor-attributesbits->avl$inline avl x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->avl$inline-of-bfix-avl (equal (!data-segment-descriptor-attributesbits->avl$inline (bfix avl) x) (!data-segment-descriptor-attributesbits->avl$inline avl x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->avl$inline-bit-equiv-congruence-on-avl (implies (bit-equiv avl avl-equiv) (equal (!data-segment-descriptor-attributesbits->avl$inline avl x) (!data-segment-descriptor-attributesbits->avl$inline avl-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->avl$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->avl$inline avl (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->avl$inline avl x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->avl$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->avl$inline avl x) (!data-segment-descriptor-attributesbits->avl$inline avl x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->avl-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->avl avl x) (change-data-segment-descriptor-attributesbits x :avl avl)))
Theorem:
(defthm data-segment-descriptor-attributesbits->avl-of-!data-segment-descriptor-attributesbits->avl (b* ((?new-x (!data-segment-descriptor-attributesbits->avl$inline avl x))) (equal (data-segment-descriptor-attributesbits->avl new-x) (bfix avl))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->avl-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->avl$inline avl x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -257)))
Function:
(defun !data-segment-descriptor-attributesbits->l$inline (l x) (declare (xargs :guard (and (bitp l) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((l (mbe :logic (bfix l) :exec l)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install l x :width 1 :low 9)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 11) -513))) (the (unsigned-byte 10) (ash (the (unsigned-byte 1) l) 9))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->l (b* ((new-x (!data-segment-descriptor-attributesbits->l$inline l x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->l$inline-of-bfix-l (equal (!data-segment-descriptor-attributesbits->l$inline (bfix l) x) (!data-segment-descriptor-attributesbits->l$inline l x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->l$inline-bit-equiv-congruence-on-l (implies (bit-equiv l l-equiv) (equal (!data-segment-descriptor-attributesbits->l$inline l x) (!data-segment-descriptor-attributesbits->l$inline l-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->l$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->l$inline l (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->l$inline l x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->l$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->l$inline l x) (!data-segment-descriptor-attributesbits->l$inline l x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->l-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->l l x) (change-data-segment-descriptor-attributesbits x :l l)))
Theorem:
(defthm data-segment-descriptor-attributesbits->l-of-!data-segment-descriptor-attributesbits->l (b* ((?new-x (!data-segment-descriptor-attributesbits->l$inline l x))) (equal (data-segment-descriptor-attributesbits->l new-x) (bfix l))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->l-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->l$inline l x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -513)))
Function:
(defun !data-segment-descriptor-attributesbits->d/b$inline (d/b x) (declare (xargs :guard (and (bitp d/b) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((d/b (mbe :logic (bfix d/b) :exec d/b)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install d/b x :width 1 :low 10)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 12) -1025))) (the (unsigned-byte 11) (ash (the (unsigned-byte 1) d/b) 10))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->d/b (b* ((new-x (!data-segment-descriptor-attributesbits->d/b$inline d/b x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->d/b$inline-of-bfix-d/b (equal (!data-segment-descriptor-attributesbits->d/b$inline (bfix d/b) x) (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->d/b$inline-bit-equiv-congruence-on-d/b (implies (bit-equiv d/b d/b-equiv) (equal (!data-segment-descriptor-attributesbits->d/b$inline d/b x) (!data-segment-descriptor-attributesbits->d/b$inline d/b-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->d/b$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->d/b$inline d/b (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->d/b$inline d/b x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->d/b$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->d/b$inline d/b x) (!data-segment-descriptor-attributesbits->d/b$inline d/b x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->d/b-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->d/b d/b x) (change-data-segment-descriptor-attributesbits x :d/b d/b)))
Theorem:
(defthm data-segment-descriptor-attributesbits->d/b-of-!data-segment-descriptor-attributesbits->d/b (b* ((?new-x (!data-segment-descriptor-attributesbits->d/b$inline d/b x))) (equal (data-segment-descriptor-attributesbits->d/b new-x) (bfix d/b))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->d/b-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->d/b$inline d/b x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -1025)))
Function:
(defun !data-segment-descriptor-attributesbits->g$inline (g x) (declare (xargs :guard (and (bitp g) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((g (mbe :logic (bfix g) :exec g)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install g x :width 1 :low 11)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 13) -2049))) (the (unsigned-byte 12) (ash (the (unsigned-byte 1) g) 11))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->g (b* ((new-x (!data-segment-descriptor-attributesbits->g$inline g x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->g$inline-of-bfix-g (equal (!data-segment-descriptor-attributesbits->g$inline (bfix g) x) (!data-segment-descriptor-attributesbits->g$inline g x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->g$inline-bit-equiv-congruence-on-g (implies (bit-equiv g g-equiv) (equal (!data-segment-descriptor-attributesbits->g$inline g x) (!data-segment-descriptor-attributesbits->g$inline g-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->g$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->g$inline g (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->g$inline g x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->g$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->g$inline g x) (!data-segment-descriptor-attributesbits->g$inline g x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->g-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->g g x) (change-data-segment-descriptor-attributesbits x :g g)))
Theorem:
(defthm data-segment-descriptor-attributesbits->g-of-!data-segment-descriptor-attributesbits->g (b* ((?new-x (!data-segment-descriptor-attributesbits->g$inline g x))) (equal (data-segment-descriptor-attributesbits->g new-x) (bfix g))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->g-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->g$inline g x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x -2049)))
Function:
(defun !data-segment-descriptor-attributesbits->unknownbits$inline (unknownbits x) (declare (xargs :guard (and (4bits-p unknownbits) (data-segment-descriptor-attributesbits-p x)))) (mbe :logic (b* ((unknownbits (mbe :logic (4bits-fix unknownbits) :exec unknownbits)) (x (data-segment-descriptor-attributesbits-fix x))) (part-install unknownbits x :width 4 :low 12)) :exec (the (unsigned-byte 16) (logior (the (unsigned-byte 16) (logand (the (unsigned-byte 16) x) (the (signed-byte 17) -61441))) (the (unsigned-byte 16) (ash (the (unsigned-byte 4) unknownbits) 12))))))
Theorem:
(defthm data-segment-descriptor-attributesbits-p-of-!data-segment-descriptor-attributesbits->unknownbits (b* ((new-x (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x))) (data-segment-descriptor-attributesbits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !data-segment-descriptor-attributesbits->unknownbits$inline-of-4bits-fix-unknownbits (equal (!data-segment-descriptor-attributesbits->unknownbits$inline (4bits-fix unknownbits) x) (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->unknownbits$inline-4bits-equiv-congruence-on-unknownbits (implies (4bits-equiv unknownbits unknownbits-equiv) (equal (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x) (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->unknownbits$inline-of-data-segment-descriptor-attributesbits-fix-x (equal (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits (data-segment-descriptor-attributesbits-fix x)) (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x)))
Theorem:
(defthm !data-segment-descriptor-attributesbits->unknownbits$inline-data-segment-descriptor-attributesbits-equiv-congruence-on-x (implies (data-segment-descriptor-attributesbits-equiv x x-equiv) (equal (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x) (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !data-segment-descriptor-attributesbits->unknownbits-is-data-segment-descriptor-attributesbits (equal (!data-segment-descriptor-attributesbits->unknownbits unknownbits x) (change-data-segment-descriptor-attributesbits x :unknownbits unknownbits)))
Theorem:
(defthm data-segment-descriptor-attributesbits->unknownbits-of-!data-segment-descriptor-attributesbits->unknownbits (b* ((?new-x (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x))) (equal (data-segment-descriptor-attributesbits->unknownbits new-x) (4bits-fix unknownbits))))
Theorem:
(defthm !data-segment-descriptor-attributesbits->unknownbits-equiv-under-mask (b* ((?new-x (!data-segment-descriptor-attributesbits->unknownbits$inline unknownbits x))) (data-segment-descriptor-attributesbits-equiv-under-mask new-x x 4095)))
Function:
(defun data-segment-descriptor-attributesbits-debug (x) (declare (xargs :guard (data-segment-descriptor-attributesbits-p x))) (let ((__function__ 'data-segment-descriptor-attributesbits-debug)) (declare (ignorable __function__)) (b* (((data-segment-descriptor-attributesbits x))) (cons (cons 'a x.a) (cons (cons 'w x.w) (cons (cons 'e x.e) (cons (cons 'msb-of-type x.msb-of-type) (cons (cons 's x.s) (cons (cons 'dpl x.dpl) (cons (cons 'p x.p) (cons (cons 'avl x.avl) (cons (cons 'l x.l) (cons (cons 'd/b x.d/b) (cons (cons 'g x.g) (cons (cons 'unknownbits x.unknownbits) nil)))))))))))))))