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