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