		Search-engine friendly clone of the ACL2 documentation.

Ubdd-constructors

Q-and-is-nil

(q-and-is-nil x y) determines whether (q-and x y) is always false.

You could ask the same question in other ways, say for instance

(not (q-and x y))

But q-and-is-nil is especially efficient and doesn't need to construct an intermediate UBDD.

Definitions and Theorems

Function: q-and-is-nil

(defun q-and-is-nil (x y)
       (declare (xargs :guard t))
       (cond ((eq x t) (eq y nil))
             ((atom x) t)
             ((eq y t) nil)
             ((atom y) t)
             (t (and (q-and-is-nil (qcar x) (qcar y))
                     (q-and-is-nil (qcdr x) (qcdr y))))))

Function: q-and-is-nil-memoize-condition

(defun q-and-is-nil-memoize-condition (x y)
       (declare (ignorable x y)
                (xargs :guard 't))
       (and (consp x) (consp y)))

Theorem: q-and-is-nil-removal

(defthm q-and-is-nil-removal
        (implies (and (force (ubddp x))
                      (force (ubddp y)))
                 (equal (q-and-is-nil x y)
                        (not (q-and x y)))))