		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Ubdd-negate-cond

Signature
(ubdd-negate-cond neg x) → new-x
Arguments: neg — Guard (bitp neg).; x — Guard (acl2::ubddp x).
Returns: new-x — Type (acl2::ubddp new-x).

Definitions and Theorems

Function: ubdd-negate-cond

(defun ubdd-negate-cond (neg x)
  (declare (xargs :guard (and (bitp neg) (acl2::ubddp x))))
  (let ((__function__ 'ubdd-negate-cond))
    (declare (ignorable __function__))
    (let ((x (lubdd-fix x)))
      (if (eql neg 1) (acl2::q-not x) x))))

Theorem: ubddp-of-ubdd-negate-cond

(defthm ubddp-of-ubdd-negate-cond
  (b* ((new-x (ubdd-negate-cond neg x)))
    (acl2::ubddp new-x))
  :rule-classes :rewrite)

Theorem: eval-of-ubdd-negate-cond

(defthm eval-of-ubdd-negate-cond
  (b* ((?new-x (ubdd-negate-cond neg x)))
    (equal (acl2::eval-bdd new-x env)
           (bit->bool (b-xor (bool->bit (acl2::eval-bdd x env))
                             neg)))))

Theorem: ubdd-negate-cond-of-bfix-neg

(defthm ubdd-negate-cond-of-bfix-neg
  (equal (ubdd-negate-cond (bfix neg) x)
         (ubdd-negate-cond neg x)))

Theorem: ubdd-negate-cond-bit-equiv-congruence-on-neg

(defthm ubdd-negate-cond-bit-equiv-congruence-on-neg
  (implies (bit-equiv neg neg-equiv)
           (equal (ubdd-negate-cond neg x)
                  (ubdd-negate-cond neg-equiv x)))
  :rule-classes :congruence)