		Search-engine friendly clone of the ACL2 documentation.

Memory32p

Recognizer for memory32.

Function: memory32p

(defun memory32p (x)
  (declare (xargs :guard t))
  (and (ubyte8-listp x)
       (equal (len x) 4294967296)))

Theorem: booleanp-of-memory32p

(defthm booleanp-of-memory32p
  (booleanp (memory32p x)))

Theorem: ubyte8-listp-when-memory32p-rewrite

(defthm ubyte8-listp-when-memory32p-rewrite
  (implies (memory32p x)
           (ubyte8-listp x)))

Theorem: ubyte8-listp-when-memory32p-forward

(defthm ubyte8-listp-when-memory32p-forward
  (implies (memory32p x) (ubyte8-listp x))
  :rule-classes :forward-chaining)

Theorem: len-when-memory32p-tau

(defthm len-when-memory32p-tau
  (implies (memory32p x)
           (equal (len x) 4294967296))
  :rule-classes :tau-system)