		Search-engine friendly clone of the ACL2 documentation.

Bfr-unparam-env

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

Definitions and Theorems

Function: bfr-unparam-env

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

Theorem: bfr-eval-to-param-space-with-unparam-env

(defthm bfr-eval-to-param-space-with-unparam-env
  (implies (and (syntaxp (not (case-match env
                                (('bfr-param-env pp &) (equal pp p))
                                (& nil))))
                (bdd-mode-or-p-true p env))
           (equal (bfr-eval (bfr-to-param-space p x) env)
                  (bfr-eval x (bfr-unparam-env p env)))))

Theorem: bfr-unparam-env-of-param-env

(defthm bfr-unparam-env-of-param-env
  (implies
       (aig-mode-or-p-true p env)
       (equal (bfr-eval x
                        (bfr-unparam-env p (bfr-param-env p env)))
              (bfr-eval x env))))

Theorem: bfr-lookup-of-unparam-bdd-env-of-param-env

(defthm bfr-lookup-of-unparam-bdd-env-of-param-env
  (implies (aig-mode-or-p-true p env)
           (bfr-env-equiv (bfr-unparam-env p (bfr-param-env p env))
                          env)))