Rule names that are defined in a list of rules.
(rulelist-defined-rules rules) → rulenames
Function:
(defun rulelist-defined-rules (rules) (declare (xargs :guard (rulelistp rules))) (cond ((endp rules) nil) (t (insert (rule->name (car rules)) (rulelist-defined-rules (cdr rules))))))
Theorem:
(defthm rulename-setp-of-rulelist-defined-rules (b* ((rulenames (rulelist-defined-rules rules))) (rulename-setp rulenames)) :rule-classes :rewrite)