Find the rules from a list of rules that transitively define the names in a list of rule names.
(trans-rules-of-names rulenames rules) → result
Function:
(defun trans-rules-of-names (rulenames rules) (declare (xargs :guard (and (rulename-setp rulenames) (rulelistp rules)))) (calc-trans-rules-of-names rulenames nil rules))
Theorem:
(defthm rulelistp-of-trans-rules-of-names (b* ((result (trans-rules-of-names rulenames rules))) (rulelistp result)) :rule-classes :rewrite)