Restrictions on the
This lifts the restriction
captured by tree-list-*-rule-/-*cwsp-cnl-restriction-p
from
Function:
(defun tree-rulelist-restriction-p (tree) (declare (xargs :guard (treep tree))) (declare (xargs :guard (and (tree-match-element-p tree (element-rulename *rulelist*) *grammar*) (tree-terminatedp tree)))) (b* ((subtrees (car (tree-nonleaf->branches tree)))) (or (not (consp subtrees)) (tree-list-*-rule-/-*cwsp-cnl-restriction-p (cdr subtrees)))))
Theorem:
(defthm booleanp-of-tree-rulelist-restriction-p (b* ((yes/no (tree-rulelist-restriction-p tree))) (booleanp yes/no)) :rule-classes :rewrite)