		Search-engine friendly clone of the ACL2 documentation.

Bfr-param-env

Signature
(bfr-param-env p env) → *

Definitions and Theorems

Function: bfr-param-env

(defun bfr-param-env (p env)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-param-env))
    (declare (ignorable __function__))
    (bfr-case :bdd (acl2::param-env p env)
              :aig env)))

Theorem: bfr-eval-to-param-space

(defthm bfr-eval-to-param-space
  (implies (bfr-eval p env)
           (equal (bfr-eval (bfr-to-param-space p x)
                            (bfr-param-env p env))
                  (bfr-eval x env))))

Theorem: bfr-eval-to-param-space-weak

(defthm bfr-eval-to-param-space-weak
  (implies (bfr-eval p env)
           (equal (bfr-eval (bfr-to-param-space-weak p x)
                            (bfr-param-env p env))
                  (bfr-eval x env))))

Theorem: bfr-eval-from-param-space

(defthm bfr-eval-from-param-space
  (implies (bfr-eval p env)
           (equal (bfr-eval (bfr-from-param-space p x)
                            env)
                  (bfr-eval x (bfr-param-env p env)))))