		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-vars

4v-sexpr-vars-alists

Extension of 4v-sexpr-vars-alists to a list of sexpr alists.

Definitions and Theorems

Function: 4v-sexpr-vars-alists

(defun 4v-sexpr-vars-alists (x)
 (declare (xargs :guard t))
 (if (atom x)
     nil
  (mbe
      :logic (set::union (4v-sexpr-vars-alist (car x))
                         (4v-sexpr-vars-alists (cdr x)))
      :exec (hons-alphorder-merge (4v-sexpr-vars-alist (car x))
                                  (4v-sexpr-vars-alists (cdr x))))))

Theorem: atom-listp-of-4v-sexpr-vars-alists

(defthm atom-listp-of-4v-sexpr-vars-alists
  (atom-listp (4v-sexpr-vars-alists x)))

Theorem: setp-of-4v-sexpr-vars-alists

(defthm setp-of-4v-sexpr-vars-alists
  (set::setp (4v-sexpr-vars-alists x)))