		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-entries->overrideconds

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

Definitions and Theorems

Function: svtv-entries->overrideconds

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

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

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

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

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

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

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

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

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