		Search-engine friendly clone of the ACL2 documentation.

Pbfr-depends-on

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

Definitions and Theorems

Function: pbfr-depends-on

(defun pbfr-depends-on (k p x)
  (declare (xargs :guard t))
  (let ((__function__ 'pbfr-depends-on))
    (declare (ignorable __function__))
    (bfr-case :bdd (pbfr-semantic-depends-on k p x)
              :aig (bfr-depends-on k (bfr-from-param-space p x)))))

Theorem: pbfr-eval-of-set-non-dep

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

Theorem: non-var-implies-non-var-in-restrict-with-iterated-assigns-alist

(defthm
    non-var-implies-non-var-in-restrict-with-iterated-assigns-alist
 (implies
  (not (set::in v (acl2::aig-vars x)))
  (not
   (set::in
    v
    (acl2::aig-vars
         (acl2::aig-restrict
              x
              (acl2::aig-extract-iterated-assigns-alist y clk)))))))

Theorem: pbfr-depends-on-of-bfr-var

(defthm pbfr-depends-on-of-bfr-var
 (implies
     (and (not (bfr-depends-on m p))
          (bfr-eval p env))
     (equal (pbfr-depends-on m p (bfr-to-param-space p (bfr-var n)))
            (equal (bfr-varname-fix m)
                   (bfr-varname-fix n)))))

Theorem: pbfr-depends-on-of-constants

(defthm pbfr-depends-on-of-constants
  (and (not (pbfr-depends-on k p t))
       (not (pbfr-depends-on k p nil))))

Theorem: no-new-deps-of-pbfr-not

(defthm no-new-deps-of-pbfr-not
  (implies (not (pbfr-depends-on k p x))
           (not (pbfr-depends-on k p (bfr-not x)))))

Theorem: no-new-deps-of-pbfr-and

(defthm no-new-deps-of-pbfr-and
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-binary-and x y)))))

Theorem: no-new-deps-of-pbfr-or

(defthm no-new-deps-of-pbfr-or
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-binary-or x y)))))

Theorem: no-new-deps-of-pbfr-xor

(defthm no-new-deps-of-pbfr-xor
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-xor x y)))))

Theorem: no-new-deps-of-pbfr-iff

(defthm no-new-deps-of-pbfr-iff
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-iff x y)))))

Theorem: no-new-deps-of-pbfr-nor

(defthm no-new-deps-of-pbfr-nor
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-nor x y)))))

Theorem: no-new-deps-of-pbfr-nand

(defthm no-new-deps-of-pbfr-nand
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-nand x y)))))

Theorem: no-new-deps-of-pbfr-andc1

(defthm no-new-deps-of-pbfr-andc1
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-andc1 x y)))))

Theorem: no-new-deps-of-pbfr-andc2

(defthm no-new-deps-of-pbfr-andc2
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-andc2 x y)))))

Theorem: no-new-deps-of-pbfr-ite

(defthm no-new-deps-of-pbfr-ite
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y))
                (not (pbfr-depends-on k p z)))
           (not (pbfr-depends-on k p (bfr-ite-fn x y z)))))

Theorem: pbfr-depends-on-when-booleanp

(defthm pbfr-depends-on-when-booleanp
  (implies (booleanp y)
           (not (pbfr-depends-on k p y)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))