		Search-engine friendly clone of the ACL2 documentation.

Xregsp

Recognizer for xregs.

Function: xregsp

(defun xregsp (x)
  (declare (xargs :guard t))
  (and (ubyte32-listp x)
       (equal (len x) 31)))

Theorem: booleanp-of-xregsp

(defthm booleanp-of-xregsp
  (booleanp (xregsp x)))

Theorem: ubyte32-listp-when-xregsp-rewrite

(defthm ubyte32-listp-when-xregsp-rewrite
  (implies (xregsp x) (ubyte32-listp x)))

Theorem: ubyte32-listp-when-xregsp-forward

(defthm ubyte32-listp-when-xregsp-forward
  (implies (xregsp x) (ubyte32-listp x))
  :rule-classes :forward-chaining)

Theorem: len-when-xregsp-tau

(defthm len-when-xregsp-tau
  (implies (xregsp x) (equal (len x) 31))
  :rule-classes :tau-system)