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.
(bfr-sterm b) → *
Function:
(defun bfr-sterm (b) (declare (xargs :guard t)) (let ((__function__ 'bfr-sterm)) (declare (ignorable __function__)) (list b)))
Theorem:
(defthm s-endp-of-bfr-sterm (equal (s-endp (bfr-sterm b)) t))
Theorem:
(defthm scdr-of-bfr-sterm (equal (scdr (bfr-sterm b)) (bfr-sterm b)))
Theorem:
(defthm car-of-bfr-sterm (equal (car (bfr-sterm b)) b))
Theorem:
(defthm bfr-list->s-of-bfr-sterm (equal (bfr-list->s (bfr-sterm b) env) (bool->sign (bfr-eval b env))))
Theorem:
(defthm pbfr-list-depends-on-of-bfr-sterm (equal (pbfr-list-depends-on k p (bfr-sterm b)) (pbfr-depends-on k p b)))