Check if a numeric value notation denotes values in a set.
Function:
(defun num-val-in-termset-p (num-val termset) (declare (xargs :guard (and (num-val-p num-val) (nat-setp termset)))) (num-val-case num-val :direct (list-in num-val.get termset) :range (list-in (integers-from-to num-val.min num-val.max) termset)))
Theorem:
(defthm booleanp-of-num-val-in-termset-p (b* ((yes/no (num-val-in-termset-p num-val termset))) (booleanp yes/no)) :rule-classes :rewrite)