Recognizer for ia32e-pde-pg-tablebits bit structures.
(ia32e-pde-pg-tablebits-p x) → *
Function:
(defun ia32e-pde-pg-tablebits-p (x) (declare (xargs :guard t)) (let ((__function__ 'ia32e-pde-pg-tablebits-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 64 x) :exec (and (natp x) (< x 18446744073709551616)))))
Theorem:
(defthm ia32e-pde-pg-tablebits-p-when-unsigned-byte-p (implies (unsigned-byte-p 64 x) (ia32e-pde-pg-tablebits-p x)))
Theorem:
(defthm unsigned-byte-p-when-ia32e-pde-pg-tablebits-p (implies (ia32e-pde-pg-tablebits-p x) (unsigned-byte-p 64 x)))
Theorem:
(defthm ia32e-pde-pg-tablebits-p-compound-recognizer (implies (ia32e-pde-pg-tablebits-p x) (natp x)) :rule-classes :compound-recognizer)