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