		Search-engine friendly clone of the ACL2 documentation.

In-terminal-set

Concatenation-in-termset-p

Check if all the terminal value notations in a concatenation denote values in a set.

Signature
(concatenation-in-termset-p concatenation termset) → yes/no
Arguments: concatenation — Guard (concatenationp concatenation).; termset — Guard (nat-setp termset).
Returns: yes/no — Type (booleanp yes/no).

Function: concatenation-in-termset-p

(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))))

Subtopics

Concatenation-in-termset-p-basics: Basic theorems about concatenation-in-termset-p, generated by std::deflist.