Recognizer for `rulename-set`.

- Signature
(rulename-setp x) → *

**Function: **

(defun rulename-setp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (rulenamep (car x)) (or (null (cdr x)) (and (consp (cdr x)) (acl2::fast-<< (car x) (cadr x)) (rulename-setp (cdr x)))))))

**Theorem: **

(defthm booleanp-ofrulename-setp (booleanp (rulename-setp x)))

**Theorem: **

(defthm setp-when-rulename-setp (implies (rulename-setp x) (setp x)) :rule-classes (:rewrite))

**Theorem: **

(defthm rulenamep-of-head-when-rulename-setp (implies (rulename-setp x) (equal (rulenamep (head x)) (not (emptyp x)))))

**Theorem: **

(defthm rulename-setp-of-tail-when-rulename-setp (implies (rulename-setp x) (rulename-setp (tail x))))

**Theorem: **

(defthm rulename-setp-of-insert (equal (rulename-setp (insert a x)) (and (rulenamep a) (rulename-setp (sfix x)))))

**Theorem: **

(defthm rulenamep-when-in-rulename-setp-binds-free-x (implies (and (in a x) (rulename-setp x)) (rulenamep a)))

**Theorem: **

(defthm rulename-setp-of-union (equal (rulename-setp (union x y)) (and (rulename-setp (sfix x)) (rulename-setp (sfix y)))))

**Theorem: **

(defthm rulename-setp-of-difference (implies (rulename-setp x) (rulename-setp (difference x y))))

**Theorem: **

(defthm rulename-setp-of-delete (implies (rulename-setp x) (rulename-setp (delete a x))))