		Search-engine friendly clone of the ACL2 documentation.

Bit/byte/integer-conversions

I2bebsp

The function \mathsf{I2BEBSP} in [ZPS:5.1].

Signature
(i2bebsp l x) → bits
Arguments: l — Guard (natp l).; x — Guard (integer-range-p 0 (expt 2 l) x).
Returns: bits — Type (bit-listp bits).

Definitions and Theorems

Function: i2bebsp

(defun i2bebsp (l x)
  (declare (xargs :guard (and (natp l)
                              (integer-range-p 0 (expt 2 l) x))))
  (let ((__function__ 'i2bebsp))
    (declare (ignorable __function__))
    (acl2::nat=>bebits l x)))

Theorem: bit-listp-of-i2bebsp

(defthm bit-listp-of-i2bebsp
  (b* ((bits (i2bebsp l x)))
    (bit-listp bits))
  :rule-classes :rewrite)

Theorem: len-of-i2bebsp

(defthm len-of-i2bebsp
  (b* ((?bits (i2bebsp l x)))
    (equal (len bits) (nfix l))))

Theorem: i2bebsp-injectivity

(defthm i2bebsp-injectivity
  (implies (and (< (nfix x1) (expt 2 (nfix l)))
                (< (nfix x2) (expt 2 (nfix l))))
           (equal (equal (i2bebsp l x1) (i2bebsp l x2))
                  (equal (nfix x1) (nfix x2)))))