(page-present entry) → bit
Function:
(defun page-present (entry) (declare (type (unsigned-byte 64) entry)) (let ((__function__ 'page-present)) (declare (ignorable __function__)) (ia32e-page-tablesbits->p entry)))
Theorem:
(defthm return-type-of-page-present (b* ((bit (page-present entry))) (unsigned-byte-p 1 bit)) :rule-classes :rewrite)
Theorem:
(defthm n01p-page-present (unsigned-byte-p 1 (page-present val)) :rule-classes (:rewrite (:type-prescription :corollary (bitp (page-present val)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp bitp (:e expt))))) (:linear :corollary (and (<= 0 (page-present val)) (< (page-present val) 2)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))