Fixer for bit-size.
(bit-size-fix x) → fixed-x
Function:
(defun bit-size-fix (x) (declare (xargs :guard (bit-size-p x))) (mbe :logic (if (bit-size-p x) x 256) :exec x))
Theorem:
(defthm bit-size-p-of-bit-size-fix (b* ((fixed-x (bit-size-fix x))) (bit-size-p fixed-x)) :rule-classes :rewrite)
Theorem:
(defthm bit-size-fix-when-bit-size-p (implies (bit-size-p x) (equal (bit-size-fix x) x)))