An 12-bit unsigned bitstruct type.
This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 12-bit integer.
This is an atomic/empty structure; it has no fields.
Function:
(defun cutscore-p (x) (declare (xargs :guard t)) (let ((__function__ 'cutscore-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 12 x) :exec (and (natp x) (< x 4096)))))
Theorem:
(defthm cutscore-p-when-unsigned-byte-p (implies (unsigned-byte-p 12 x) (cutscore-p x)))
Theorem:
(defthm unsigned-byte-p-when-cutscore-p (implies (cutscore-p x) (unsigned-byte-p 12 x)))
Theorem:
(defthm cutscore-p-compound-recognizer (implies (cutscore-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun cutscore-fix (x) (declare (xargs :guard (cutscore-p x))) (let ((__function__ 'cutscore-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 12 x) :exec x)))
Theorem:
(defthm cutscore-p-of-cutscore-fix (b* ((fty::fixed (cutscore-fix x))) (cutscore-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm cutscore-fix-when-cutscore-p (implies (cutscore-p x) (equal (cutscore-fix x) x)))
Function:
(defun cutscore-equiv$inline (x acl2::y) (declare (xargs :guard (and (cutscore-p x) (cutscore-p acl2::y)))) (equal (cutscore-fix x) (cutscore-fix acl2::y)))
Theorem:
(defthm cutscore-equiv-is-an-equivalence (and (booleanp (cutscore-equiv x y)) (cutscore-equiv x x) (implies (cutscore-equiv x y) (cutscore-equiv y x)) (implies (and (cutscore-equiv x y) (cutscore-equiv y z)) (cutscore-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm cutscore-equiv-implies-equal-cutscore-fix-1 (implies (cutscore-equiv x x-equiv) (equal (cutscore-fix x) (cutscore-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm cutscore-fix-under-cutscore-equiv (cutscore-equiv (cutscore-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm cutscore-fix-of-cutscore-fix-x (equal (cutscore-fix (cutscore-fix x)) (cutscore-fix x)))
Theorem:
(defthm cutscore-fix-cutscore-equiv-congruence-on-x (implies (cutscore-equiv x x-equiv) (equal (cutscore-fix x) (cutscore-fix x-equiv))) :rule-classes :congruence)