		Search-engine friendly clone of the ACL2 documentation.

Bfr-sterm

Promote a single BFR into a signed, one-bit bvec, i.e., the resulting value under bfr-list->s is either 0 or -1, depending on the environment.

Function: bfr-sterm

(defun bfr-sterm (b)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-sterm))
    (declare (ignorable __function__))
    (list b)))

Theorem: s-endp-of-bfr-sterm

(defthm s-endp-of-bfr-sterm
  (equal (s-endp (bfr-sterm b)) t))

Theorem: scdr-of-bfr-sterm

(defthm scdr-of-bfr-sterm
  (equal (scdr (bfr-sterm b))
         (bfr-sterm b)))

Theorem: car-of-bfr-sterm

(defthm car-of-bfr-sterm
  (equal (car (bfr-sterm b)) b))

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

(defthm bfr-list->s-of-bfr-sterm
  (equal (bfr-list->s (bfr-sterm b) env)
         (bool->sign (bfr-eval b env))))

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

(defthm pbfr-list-depends-on-of-bfr-sterm
  (equal (pbfr-list-depends-on k p (bfr-sterm b))
         (pbfr-depends-on k p b)))