		Search-engine friendly clone of the ACL2 documentation.

Ubdds

Ubdd-listp

Recognizer for a list of ubdds.

Definitions and Theorems

Function: ubdd-listp

(defun ubdd-listp (l)
       (declare (xargs :guard t))
       (if (atom l)
           (null l)
           (and (ubddp (car l))
                (ubdd-listp (cdr l)))))

Theorem: ubdd-listp-when-atom

(defthm ubdd-listp-when-atom
        (implies (atom x)
                 (equal (ubdd-listp x) (not x))))

Theorem: ubdd-listp-of-cons

(defthm ubdd-listp-of-cons
        (equal (ubdd-listp (cons a x))
               (and (ubddp a) (ubdd-listp x))))