		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-x-z1...zm-aux

Signature
(schemalg-gen-x-z1...zm-aux terms-to-do vars-done x-a1...am x-x1...xn x y) → vars
Arguments: terms-to-do — Guard (pseudo-term-listp terms-to-do).; vars-done — Guard (symbol-listp vars-done).; x-a1...am — Guard (pseudo-term-listp x-a1...am).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x — Guard (symbolp x).; y — Guard (symbolp y).
Returns: vars — A symbol-listp.

Definitions and Theorems

Function: schemalg-gen-x-z1...zm-aux

(defun schemalg-gen-x-z1...zm-aux
       (terms-to-do vars-done x-a1...am x-x1...xn x y)
 (declare (xargs :guard (and (pseudo-term-listp terms-to-do)
                             (symbol-listp vars-done)
                             (pseudo-term-listp x-a1...am)
                             (symbol-listp x-x1...xn)
                             (symbolp x)
                             (symbolp y))))
 (let ((__function__ 'schemalg-gen-x-z1...zm-aux))
  (declare (ignorable __function__))
  (b*
   (((when (endp terms-to-do)) nil)
    (term (car terms-to-do))
    (var
        (if (and (symbolp term)
                 (not (member-eq term (remove1-eq term x-a1...am))))
            term
          (genvar x "VAR$" nil
                  (append vars-done x-x1...xn (list y))))))
   (cons var
         (schemalg-gen-x-z1...zm-aux (cdr terms-to-do)
                                     (cons var vars-done)
                                     x-a1...am x-x1...xn x y)))))