|
|
|---|
|
|
|
|---|
Recognizer for memory32i.
(memory32ip x) → *
Function:
(defun memory32ip (x) (declare (xargs :guard t)) (and (ubyte8-listp x) (equal (len x) 4294967296)))
Theorem:
(defthm booleanp-of-memory32ip (booleanp (memory32ip x)))
Theorem:
(defthm ubyte8-listp-when-memory32ip-rewrite (implies (memory32ip x) (ubyte8-listp x)))
Theorem:
(defthm ubyte8-listp-when-memory32ip-forward (implies (memory32ip x) (ubyte8-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm len-when-memory32ip-tau (implies (memory32ip x) (equal (len x) 4294967296)) :rule-classes :tau-system)