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