		Search-engine friendly clone of the ACL2 documentation.

Byte-list64p

Recognizer for byte-list64.

Function: byte-list64p

(defun byte-list64p (x)
  (declare (xargs :guard t))
  (and (byte-listp x) (equal (len x) 64)))

Theorem: booleanp-of-byte-list64p

(defthm booleanp-of-byte-list64p
  (booleanp (byte-list64p x)))

Theorem: byte-listp-when-byte-list64p-rewrite

(defthm byte-listp-when-byte-list64p-rewrite
  (implies (byte-list64p x)
           (byte-listp x)))

Theorem: byte-listp-when-byte-list64p-forward

(defthm byte-listp-when-byte-list64p-forward
  (implies (byte-list64p x)
           (byte-listp x))
  :rule-classes :forward-chaining)

Theorem: len-when-byte-list64p-tau

(defthm len-when-byte-list64p-tau
  (implies (byte-list64p x)
           (equal (len x) 64))
  :rule-classes :tau-system)