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