		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)))