		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-entries->vars

Signature
(svtv-entries->vars x) → vars
Arguments: x — Guard (svtv-entrylist-p x).
Returns: vars — Type (symbol-listp vars).

Definitions and Theorems

Function: svtv-entries->vars

(defun svtv-entries->vars (x)
  (declare (xargs :guard (svtv-entrylist-p x)))
  (let ((__function__ 'svtv-entries->vars))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (let ((xf (svtv-entry-fix (car x))))
        (cond ((and (symbolp xf)
                    (not (svtv-dontcare-p xf))
                    (not (equal (symbol-name xf) "~"))
                    (not (eq xf :ones)))
               (cons xf (svtv-entries->vars (cdr x))))
              ((and (svtv-condoverride-p xf)
                    (let ((xf (svtv-condoverride->value xf)))
                      (and (symbolp xf)
                           (not (svtv-dontcare-p xf))
                           (not (equal (symbol-name xf) "~"))
                           (not (eq xf :ones)))))
               (cons (svtv-condoverride->value xf)
                     (svtv-entries->vars (cdr x))))
              (t (svtv-entries->vars (cdr x))))))))

Theorem: symbol-listp-of-svtv-entries->vars

(defthm symbol-listp-of-svtv-entries->vars
  (b* ((vars (svtv-entries->vars x)))
    (symbol-listp vars))
  :rule-classes :rewrite)

Theorem: svarlist-p-of-svtv-entries->vars

(defthm svarlist-p-of-svtv-entries->vars
  (svarlist-p (svtv-entries->vars x)))

Theorem: svtv-entries->vars-of-svtv-entrylist-fix-x

(defthm svtv-entries->vars-of-svtv-entrylist-fix-x
  (equal (svtv-entries->vars (svtv-entrylist-fix x))
         (svtv-entries->vars x)))

Theorem: svtv-entries->vars-svtv-entrylist-equiv-congruence-on-x

(defthm svtv-entries->vars-svtv-entrylist-equiv-congruence-on-x
  (implies (svtv-entrylist-equiv x x-equiv)
           (equal (svtv-entries->vars x)
                  (svtv-entries->vars x-equiv)))
  :rule-classes :congruence)