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