A
(abstract-rule-/-*cwsp-cnl tree) → rule?
Function:
(defun abstract-rule-/-*cwsp-cnl (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (abstract-fail)) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (consp treess)) (fail)) (trees (car treess)) ((unless (consp trees)) (fail)) (subtree (car trees)) ((unless (tree-case subtree :nonleaf)) (fail))) (if (equal (tree-nonleaf->rulename? subtree) (rulename "rule")) (abstract-rule subtree) nil)))
Theorem:
(defthm rule-optionp-of-abstract-rule-/-*cwsp-cnl (b* ((rule? (abstract-rule-/-*cwsp-cnl tree))) (rule-optionp rule?)) :rule-classes :rewrite)