Check if all the terminal value notations in a concatenation denote values in a set.
(concatenation-in-termset-p concatenation termset) → yes/no
Function:
(defun concatenation-in-termset-p (concatenation termset) (declare (xargs :guard (and (concatenationp concatenation) (nat-setp termset)))) (or (endp concatenation) (and (repetition-in-termset-p (car concatenation) termset) (concatenation-in-termset-p (cdr concatenation) termset))))