Restrictions on the (non-starting)
This lifts the restriction captured by tree-*cwsp-cnl-restriction-p
from
Function:
(defun tree-rule-/-*cwsp-cnl-restriction-p (tree) (declare (xargs :guard (treep tree))) (declare (xargs :guard (and (tree-match-element-p tree (!_ (/_ *rule*) (/_ (!_ (/_ (*_ *c-wsp*) *c-nl*)))) *grammar*) (tree-terminatedp tree)))) (or (tree-match-element-p (car (car (tree-nonleaf->branches tree))) (element-rulename *rule*) *grammar*) (tree-*cwsp-cnl-restriction-p (car (car (tree-nonleaf->branches tree))))))
Theorem:
(defthm booleanp-of-tree-rule-/-*cwsp-cnl-restriction-p (b* ((yes/no (tree-rule-/-*cwsp-cnl-restriction-p tree))) (booleanp yes/no)) :rule-classes :rewrite)