		Search-engine friendly clone of the ACL2 documentation.

Ubdds

Eval-bdd-list

Apply eval-bdd to a list of UBDDs.

The resulting list is honsed together.

BOZO why do we hons the list, I suspect it makes no sense to do so...

Definitions and Theorems

Function: eval-bdd-list

(defun eval-bdd-list (x values)
  (declare (xargs :guard t))
  (if (consp x)
      (hons (eval-bdd (car x) values)
            (eval-bdd-list (cdr x) values))
    nil))

Theorem: eval-bdd-list-when-not-consp

(defthm eval-bdd-list-when-not-consp
  (implies (not (consp x))
           (equal (eval-bdd-list x values) nil)))

Theorem: eval-bdd-list-of-cons

(defthm eval-bdd-list-of-cons
  (equal (eval-bdd-list (cons a x) values)
         (cons (eval-bdd a values)
               (eval-bdd-list x values))))

Theorem: consp-eval-bdd-list

(defthm consp-eval-bdd-list
  (equal (consp (eval-bdd-list x env))
         (consp x)))