Fixer for ubyte16.
Function:
(defun ubyte16-fix (x) (declare (xargs :guard (ubyte16p x))) (mbe :logic (if (ubyte16p x) x 0) :exec x))
Theorem:
(defthm ubyte16p-of-ubyte16-fix (b* ((fixed-x (ubyte16-fix x))) (ubyte16p fixed-x)) :rule-classes :rewrite)
Theorem:
(defthm ubyte16-fix-when-ubyte16p (implies (ubyte16p x) (equal (ubyte16-fix x) x)))