		Search-engine friendly clone of the ACL2 documentation.

Memory32i

Memory32i-fix

Fixer for memory32i.

Signature
(memory32i-fix x) → *
Arguments: x — Guard (memory32ip x).

Definitions and Theorems

Function: memory32i-fix

(defun memory32i-fix (x)
  (declare (xargs :guard (memory32ip x)))
  (mbe :logic
       (if (memory32ip x)
           x
         (acl2::ubyte8-list-fix (take 4294967296 x)))
       :exec x))

Theorem: memory32ip-of-memory32i-fix

(defthm memory32ip-of-memory32i-fix
  (memory32ip (memory32i-fix x)))

Theorem: memory32i-fix-when-memory32ip

(defthm memory32i-fix-when-memory32ip
  (implies (memory32ip x)
           (equal (memory32i-fix x) x)))