		Search-engine friendly clone of the ACL2 documentation.

Qv

(qv i) constructs a UBDD which evaluates to true exactly when the ith BDD variable is true.

Function: qv

(defun qv (i)
  (declare (xargs :guard t))
  (if (posp i)
      (let ((prev (qv (1- i))))
        (hons prev prev))
    (hons t nil)))

Theorem: ubddp-qv

(defthm ubddp-qv (ubddp (qv i)))

Theorem: eval-bdd-of-qv-and-nil

(defthm eval-bdd-of-qv-and-nil
  (not (eval-bdd (qv i) nil)))

Theorem: eval-bdd-of-qv

(defthm eval-bdd-of-qv
  (equal (eval-bdd (qv i) lst)
         (if (nth i lst) t nil)))

Theorem: qvs-equal

(defthm qvs-equal
  (equal (equal (qv i) (qv j))
         (equal (nfix i) (nfix j))))