		Search-engine friendly clone of the ACL2 documentation.

Bit/byte/integer-conversions

I2lebsp

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

Signature
(i2lebsp 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: i2lebsp

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

Theorem: bit-listp-of-i2lebsp

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

Theorem: len-of-i2lebsp

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

Theorem: i2lebsp-injectivity

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