		Search-engine friendly clone of the ACL2 documentation.

Xregfile64p

Recognizer for xregfile64.

Function: xregfile64p

(defun xregfile64p (x)
  (declare (xargs :guard t))
  (and (ubyte64-listp x)
       (equal (len x) 32)))

Theorem: booleanp-of-xregfile64p

(defthm booleanp-of-xregfile64p
  (booleanp (xregfile64p x)))

Theorem: ubyte64-listp-when-xregfile64p-rewrite

(defthm ubyte64-listp-when-xregfile64p-rewrite
  (implies (xregfile64p x)
           (ubyte64-listp x)))

Theorem: ubyte64-listp-when-xregfile64p-forward

(defthm ubyte64-listp-when-xregfile64p-forward
  (implies (xregfile64p x)
           (ubyte64-listp x))
  :rule-classes :forward-chaining)

Theorem: len-when-xregfile64p-tau

(defthm len-when-xregfile64p-tau
  (implies (xregfile64p x)
           (equal (len x) 32))
  :rule-classes :tau-system)