A list of zero or more
(abstract-*-rule-/-*cwsp-cnl trees) → rules
Function:
(defun abstract-*-rule-/-*cwsp-cnl (trees) (declare (xargs :guard (tree-listp trees))) (b* (((fun (fail)) (abstract-fail)) ((when (endp trees)) nil) ((cons tree trees) trees) (rule? (abstract-rule-/-*cwsp-cnl tree)) (rules (abstract-*-rule-/-*cwsp-cnl trees))) (if rule? (cons rule? rules) rules)))
Theorem:
(defthm rulelistp-of-abstract-*-rule-/-*cwsp-cnl (b* ((rules (abstract-*-rule-/-*cwsp-cnl trees))) (rulelistp rules)) :rule-classes :rewrite)