Check if a string consists of terminals in a set and rule names.
(string-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 string-in-termset-p (x termset) (declare (xargs :guard (and (stringp x) (nat-setp termset)))) (let ((__function__ 'string-in-termset-p)) (declare (ignorable __function__)) (if (consp x) (and (symbol-in-termset-p (car x) termset) (string-in-termset-p (cdr x) termset)) t)))
Theorem:
(defthm string-in-termset-p-when-nat-listp (implies (nat-listp nats) (equal (string-in-termset-p nats termset) (list-in nats termset))))