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