Fixing function for cutscore bit structures.
(cutscore-fix x) → fty::fixed
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)