		Search-engine friendly clone of the ACL2 documentation.

Bvec

Bfr-ucons

Like logcons for unsigned bvecs.

Signature
(bfr-ucons b x) → new-x
Arguments: x — Guard (true-listp x).
Returns: new-x — Type (true-listp new-x).

Definitions and Theorems

Function: bfr-ucons

(defun bfr-ucons (b x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'bfr-ucons))
    (declare (ignorable __function__))
    (if (and (atom x) (not b))
        nil
      (cons b (llist-fix x)))))

Theorem: true-listp-of-bfr-ucons

(defthm true-listp-of-bfr-ucons
  (b* ((new-x (bfr-ucons b x)))
    (true-listp new-x))
  :rule-classes :type-prescription)

Theorem: bfr-list->u-of-bfr-ucons

(defthm bfr-list->u-of-bfr-ucons
  (equal (bfr-list->u (bfr-ucons b x) env)
         (logcons (bool->bit (bfr-eval b env))
                  (bfr-list->u x env))))

Theorem: pbfr-list-depends-on-of-bfr-ucons

(defthm pbfr-list-depends-on-of-bfr-ucons
  (implies (and (not (pbfr-depends-on k p b))
                (not (pbfr-list-depends-on k p x)))
           (not (pbfr-list-depends-on k p (bfr-ucons b x)))))

Theorem: bfr-ucons-of-list-fix

(defthm bfr-ucons-of-list-fix
  (equal (bfr-ucons b (list-fix x))
         (bfr-ucons b x)))