		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-gen-fep-terms

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

Signature
(lift-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: lift-gen-fep-terms

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

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

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