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