|
|
|---|
|
|
|
|---|
Fixer for xregfile32.
(xregfile32-fix x) → *
Function:
(defun xregfile32-fix (x) (declare (xargs :guard (xregfile32p x))) (mbe :logic (if (xregfile32p x) x (acl2::ubyte32-list-fix (take 32 x))) :exec x))
Theorem:
(defthm xregfile32p-of-xregfile32-fix (xregfile32p (xregfile32-fix x)))
Theorem:
(defthm xregfile32-fix-when-xregfile32p (implies (xregfile32p x) (equal (xregfile32-fix x) x)))