		Search-engine friendly clone of the ACL2 documentation.

Bfr-fix

Signature
(bfr-fix x &optional (bfrstate 'bfrstate)) → new-x
Arguments: x — Guard (bfr-p x).; bfrstate — Guard (bfrstate-p bfrstate).
Returns: new-x — Type (bfr-p new-x).

Definitions and Theorems

Function: bfr-fix-fn

(defun bfr-fix-fn (x bfrstate)
 (declare (xargs :guard (and (bfrstate-p bfrstate) (bfr-p x))))
 (let ((__function__ 'bfr-fix))
  (declare (ignorable __function__))
  (mbe
     :logic
     (bfrstate-case :aig (aig-fix x (bfrstate->bound bfrstate))
                    :bdd (ubdd-fix x (bfrstate->bound bfrstate))
                    :aignet (if (booleanp x) x (aignet-lit->bfr x)))
     :exec x)))

Theorem: bfr-p-of-bfr-fix

(defthm bfr-p-of-bfr-fix
  (b* ((new-x (bfr-fix-fn x bfrstate)))
    (bfr-p new-x))
  :rule-classes :rewrite)

Theorem: bfr-fix-when-bfr-p

(defthm bfr-fix-when-bfr-p
  (b* ((?new-x (bfr-fix-fn x bfrstate)))
    (implies (bfr-p x) (equal new-x x))))

Theorem: bfr-fix-fn-of-bfrstate-fix-bfrstate

(defthm bfr-fix-fn-of-bfrstate-fix-bfrstate
  (equal (bfr-fix-fn x (bfrstate-fix bfrstate))
         (bfr-fix-fn x bfrstate)))

Theorem: bfr-fix-fn-bfrstate-equiv-congruence-on-bfrstate

(defthm bfr-fix-fn-bfrstate-equiv-congruence-on-bfrstate
  (implies (bfrstate-equiv bfrstate bfrstate-equiv)
           (equal (bfr-fix-fn x bfrstate)
                  (bfr-fix-fn x bfrstate-equiv)))
  :rule-classes :congruence)