		Search-engine friendly clone of the ACL2 documentation.

Bvec

Pbfr-list-depends-on

Signature
(pbfr-list-depends-on k p x) → *

Definitions and Theorems

Function: pbfr-list-depends-on

(defun pbfr-list-depends-on (k p x)
  (declare (xargs :guard t))
  (let ((__function__ 'pbfr-list-depends-on))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (or (pbfr-depends-on k p (car x))
          (pbfr-list-depends-on k p (cdr x))))))

Theorem: pbfr-list-depends-on-of-list-fix

(defthm pbfr-list-depends-on-of-list-fix
  (equal (pbfr-list-depends-on k p (list-fix x))
         (pbfr-list-depends-on k p x)))

Theorem: bfr-eval-list-of-set-non-dep

(defthm bfr-eval-list-of-set-non-dep
 (implies
      (and (not (pbfr-list-depends-on k p x))
           (bfr-eval p env)
           (bfr-eval p (bfr-set-var k v env)))
      (equal (bfr-eval-list x
                            (bfr-param-env p (bfr-set-var k v env)))
             (bfr-eval-list x (bfr-param-env p env)))))

Theorem: pbfr-depends-on-car

(defthm pbfr-depends-on-car
  (implies (not (pbfr-list-depends-on k p x))
           (not (pbfr-depends-on k p (car x)))))

Theorem: pbfr-depends-on-cdr

(defthm pbfr-depends-on-cdr
  (implies (not (pbfr-list-depends-on k p x))
           (not (pbfr-list-depends-on k p (cdr x)))))