		Search-engine friendly clone of the ACL2 documentation.

Ubdd-listp

Recognizer for a list of ubdds.

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