Fixing function for gdtr/idtrbits bit structures.
(gdtr/idtrbits-fix x) → fty::fixed
Function:
(defun gdtr/idtrbits-fix (x) (declare (xargs :guard (gdtr/idtrbits-p x))) (let ((__function__ 'gdtr/idtrbits-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 80 x) :exec x)))
Theorem:
(defthm gdtr/idtrbits-p-of-gdtr/idtrbits-fix (b* ((fty::fixed (gdtr/idtrbits-fix x))) (gdtr/idtrbits-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm gdtr/idtrbits-fix-when-gdtr/idtrbits-p (implies (gdtr/idtrbits-p x) (equal (gdtr/idtrbits-fix x) x)))
Function:
(defun gdtr/idtrbits-equiv$inline (x y) (declare (xargs :guard (and (gdtr/idtrbits-p x) (gdtr/idtrbits-p y)))) (equal (gdtr/idtrbits-fix x) (gdtr/idtrbits-fix y)))
Theorem:
(defthm gdtr/idtrbits-equiv-is-an-equivalence (and (booleanp (gdtr/idtrbits-equiv x y)) (gdtr/idtrbits-equiv x x) (implies (gdtr/idtrbits-equiv x y) (gdtr/idtrbits-equiv y x)) (implies (and (gdtr/idtrbits-equiv x y) (gdtr/idtrbits-equiv y z)) (gdtr/idtrbits-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm gdtr/idtrbits-equiv-implies-equal-gdtr/idtrbits-fix-1 (implies (gdtr/idtrbits-equiv x x-equiv) (equal (gdtr/idtrbits-fix x) (gdtr/idtrbits-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm gdtr/idtrbits-fix-under-gdtr/idtrbits-equiv (gdtr/idtrbits-equiv (gdtr/idtrbits-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))