Check if all the terminal value notations in a list of rules denote values in a set.
(rulelist-in-termset-p x termset) → std::bool
This is an ordinary std::deflist. It is
"loose" in that it does not care whether
Function:
(defun rulelist-in-termset-p (x termset) (declare (xargs :guard (and (rulelistp x) (nat-setp termset)))) (let ((__function__ 'rulelist-in-termset-p)) (declare (ignorable __function__)) (if (consp x) (and (rule-in-termset-p (car x) termset) (rulelist-in-termset-p (cdr x) termset)) t)))
Theorem:
(defthm alternation-in-termset-p-of-lookup-rulename (implies (rulelist-in-termset-p rules termset) (alternation-in-termset-p (lookup-rulename rulename rules) termset)))