A rule list is closed iff it defines all the rules that it calls.
Function:
(defun rulelist-closedp (rules) (declare (xargs :guard (rulelistp rules))) (subset (rulelist-called-rules rules) (rulelist-defined-rules rules)))
Theorem:
(defthm booleanp-of-rulelist-closedp (b* ((yes/no (rulelist-closedp rules))) (booleanp yes/no)) :rule-classes :rewrite)