Update the |X86ISA|::|RES2| field of a ia32e-pdpte-1gb-pagebits bit structure.
(!ia32e-pdpte-1gb-pagebits->res2 res2 x) → new-x
Function:
(defun !ia32e-pdpte-1gb-pagebits->res2$inline (res2 x) (declare (xargs :guard (and (17bits-p res2) (ia32e-pdpte-1gb-pagebits-p x)))) (mbe :logic (b* ((res2 (mbe :logic (17bits-fix res2) :exec res2)) (x (ia32e-pdpte-1gb-pagebits-fix x))) (part-install res2 x :width 17 :low 13)) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 64) (logand (the (unsigned-byte 64) x) (the (signed-byte 31) -1073733633))) (the (unsigned-byte 30) (ash (the (unsigned-byte 17) res2) 13))))))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits-p-of-!ia32e-pdpte-1gb-pagebits->res2 (b* ((new-x (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x))) (ia32e-pdpte-1gb-pagebits-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-of-17bits-fix-res2 (equal (!ia32e-pdpte-1gb-pagebits->res2$inline (17bits-fix res2) x) (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-17bits-equiv-congruence-on-res2 (implies (17bits-equiv res2 res2-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x) (!ia32e-pdpte-1gb-pagebits->res2$inline res2-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-of-ia32e-pdpte-1gb-pagebits-fix-x (equal (!ia32e-pdpte-1gb-pagebits->res2$inline res2 (ia32e-pdpte-1gb-pagebits-fix x)) (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x)))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2$inline-ia32e-pdpte-1gb-pagebits-equiv-congruence-on-x (implies (ia32e-pdpte-1gb-pagebits-equiv x x-equiv) (equal (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x) (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2-is-ia32e-pdpte-1gb-pagebits (equal (!ia32e-pdpte-1gb-pagebits->res2 res2 x) (change-ia32e-pdpte-1gb-pagebits x :res2 res2)))
Theorem:
(defthm ia32e-pdpte-1gb-pagebits->res2-of-!ia32e-pdpte-1gb-pagebits->res2 (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x))) (equal (ia32e-pdpte-1gb-pagebits->res2 new-x) (17bits-fix res2))))
Theorem:
(defthm !ia32e-pdpte-1gb-pagebits->res2-equiv-under-mask (b* ((?new-x (!ia32e-pdpte-1gb-pagebits->res2$inline res2 x))) (ia32e-pdpte-1gb-pagebits-equiv-under-mask new-x x -1073733633)))