		Search-engine friendly clone of the ACL2 documentation.

Ubyte6-fix

Fixer for ubyte6.

Function: ubyte6-fix

(defun ubyte6-fix (x)
  (declare (xargs :guard (ubyte6p x)))
  (mbe :logic (if (ubyte6p x) x 0)
       :exec x))

Theorem: ubyte6p-of-ubyte6-fix

(defthm ubyte6p-of-ubyte6-fix
  (b* ((fixed-x (ubyte6-fix x)))
    (ubyte6p fixed-x))
  :rule-classes :rewrite)

Theorem: ubyte6-fix-when-ubyte6p

(defthm ubyte6-fix-when-ubyte6p
  (implies (ubyte6p x)
           (equal (ubyte6-fix x) x)))