		Search-engine friendly clone of the ACL2 documentation.

Semantics-shallowly-embedded

Sesem-gen-fep-terms

Generate a list of terms (fep x1 p), ..., (fep xn p) from a list of variables x1, ..., xn.

Signature
(sesem-gen-fep-terms vars prime) → terms
Arguments: vars — Guard (symbol-listp vars).; prime — Guard (symbolp prime).
Returns: terms — Type (pseudo-term-listp terms), given the guard.

Definitions and Theorems

Function: sesem-gen-fep-terms

(defun sesem-gen-fep-terms (vars prime)
  (declare (xargs :guard (and (symbol-listp vars)
                              (symbolp prime))))
  (let ((__function__ 'sesem-gen-fep-terms))
    (declare (ignorable __function__))
    (cond ((endp vars) nil)
          (t (cons (cons 'fep
                         (cons (car vars) (cons prime 'nil)))
                   (sesem-gen-fep-terms (cdr vars)
                                        prime))))))

Theorem: pseudo-term-listp-of-sesem-gen-fep-terms

(defthm pseudo-term-listp-of-sesem-gen-fep-terms
  (implies (and (symbol-listp vars)
                (symbolp prime))
           (b* ((terms (sesem-gen-fep-terms vars prime)))
             (pseudo-term-listp terms)))
  :rule-classes :rewrite)