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