		Search-engine friendly clone of the ACL2 documentation.

Bvec

Bfr-list->s

Signed interpretation of a BFR list under some environment.

Signature
(bfr-list->s x env) → *
Arguments: x — BFR list to interpret as a signed number.
Guard (true-listp x).; env — Environment to evaluate the BFRs under.

Definitions and Theorems

Function: bfr-list->s

(defun bfr-list->s (x env)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'bfr-list->s))
    (declare (ignorable __function__))
    (b* (((mv first rest end)
          (first/rest/end x)))
      (if end (bool->sign (bfr-eval first env))
        (logcons (bool->bit (bfr-eval first env))
                 (bfr-list->s rest env))))))

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

(defthm bfr-list->s-of-list-fix
  (equal (bfr-list->s (list-fix x) env)
         (bfr-list->s x env)))

Theorem: bfr-list->s-when-s-endp

(defthm bfr-list->s-when-s-endp
  (implies (s-endp x)
           (equal (bfr-list->s x env)
                  (bool->sign (bfr-eval (car x) env))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

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

(defthm bfr-list->s-of-scdr
  (equal (bfr-list->s (scdr x) env)
         (logcdr (bfr-list->s x env))))

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

(defthm logcdr-of-bfr-list->s
  (equal (logcdr (bfr-list->s x env))
         (bfr-list->s (scdr x) env)))

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

(defthm logcar-of-bfr-list->s
  (equal (logcar (bfr-list->s x env))
         (bool->bit (bfr-eval (car x) env))))

Theorem: bfr-list->s-of-set-non-dep

(defthm bfr-list->s-of-set-non-dep
  (implies
       (and (not (pbfr-list-depends-on k p x))
            (bfr-eval p env)
            (bfr-eval p (bfr-set-var k v env)))
       (equal (bfr-list->s x
                           (bfr-param-env p (bfr-set-var k v env)))
              (bfr-list->s x (bfr-param-env p env)))))