		Search-engine friendly clone of the ACL2 documentation.

Bvec

Bfr-scons

Like logcons for signed bvecs.

Signature
(bfr-scons b v) → s
Arguments: v — Guard (true-listp v).
Returns: s — Type (true-listp s).

Definitions and Theorems

Function: bfr-scons

(defun bfr-scons (b v)
  (declare (xargs :guard (true-listp v)))
  (let ((__function__ 'bfr-scons))
    (declare (ignorable __function__))
    (if (atom v)
        (if b (list b nil) '(nil))
      (if (and (atom (cdr v))
               (hons-equal (car v) b))
          (llist-fix v)
        (cons b (llist-fix v))))))

Theorem: true-listp-of-bfr-scons

(defthm true-listp-of-bfr-scons
  (b* ((s (bfr-scons b v)))
    (true-listp s))
  :rule-classes :type-prescription)

Theorem: scdr-of-bfr-scons

(defthm scdr-of-bfr-scons
  (equal (scdr (bfr-scons b v))
         (bfr-snorm v)))

Theorem: s-endp-of-bfr-scons

(defthm s-endp-of-bfr-scons
  (equal (s-endp (bfr-scons b v))
         (and (s-endp v) (hqual b (car v)))))

Theorem: car-of-bfr-scons

(defthm car-of-bfr-scons
  (equal (car (bfr-scons b v)) b))

Theorem: bfr-list->s-of-bfr-scons

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

Theorem: pbfr-list-depends-on-of-scons

(defthm pbfr-list-depends-on-of-scons
  (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-scons b x)))))

Theorem: bfr-scons-of-list-fix

(defthm bfr-scons-of-list-fix
  (equal (bfr-scons b (list-fix v))
         (bfr-scons b v)))