		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Eval-ubddarr

Signature
(eval-ubddarr x env) → bits
Arguments: x — Guard (ubdd-arr$ap x).
Returns: bits — Type (bit-listp bits).

Definitions and Theorems

Function: eval-ubddarr

(defun eval-ubddarr (x env)
  (declare (xargs :guard (ubdd-arr$ap x)))
  (let ((__function__ 'eval-ubddarr))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (bool->bit (acl2::eval-bdd (car x) env))
            (eval-ubddarr (cdr x) env)))))

Theorem: bit-listp-of-eval-ubddarr

(defthm bit-listp-of-eval-ubddarr
  (b* ((bits (eval-ubddarr x env)))
    (bit-listp bits))
  :rule-classes :rewrite)

Theorem: nth-of-eval-ubddarr

(defthm nth-of-eval-ubddarr
  (b* ((?bits (eval-ubddarr x env)))
    (bit-equiv (nth n bits)
               (bool->bit (acl2::eval-bdd (nth n x) env)))))