		Search-engine friendly clone of the ACL2 documentation.

Bfr-var

Construct the nth BFR variable.

Signature
(bfr-var n) → *
Arguments: n — Guard (bfr-varname-p n).

Definitions and Theorems

Function: bfr-var

(defun bfr-var (n)
  (declare (xargs :guard (bfr-varname-p n)))
  (let ((__function__ 'bfr-var))
    (declare (ignorable __function__))
    (let ((n (bfr-varname-fix n)))
      (bfr-case :bdd (qv n) :aig n))))

Theorem: bfr-eval-bfr-var

(defthm bfr-eval-bfr-var
  (equal (bfr-eval (bfr-var n) env)
         (bfr-lookup n env)))

Theorem: bfr-varname-equiv-implies-equal-bfr-var-1

(defthm bfr-varname-equiv-implies-equal-bfr-var-1
  (implies (bfr-varname-equiv n n-equiv)
           (equal (bfr-var n) (bfr-var n-equiv)))
  :rule-classes (:congruence))