		Search-engine friendly clone of the ACL2 documentation.

Bit/byte/integer-conversions

Lebs2ip

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

Signature
(lebs2ip s) → x
Arguments: s — Guard (bit-listp s).
Returns: x — Type (natp x).

The $\ell$ argument can be determined from the S argument: it is the length of S. Thus, in our formalization we just have one argument.

Definitions and Theorems

Function: lebs2ip

(defun lebs2ip (s)
  (declare (xargs :guard (bit-listp s)))
  (let ((__function__ 'lebs2ip))
    (declare (ignorable __function__))
    (acl2::lebits=>nat s)))

Theorem: natp-of-lebs2ip

(defthm natp-of-lebs2ip
  (b* ((x (lebs2ip s))) (natp x))
  :rule-classes :type-prescription)

Theorem: lebs2ip-upper-bound

(defthm lebs2ip-upper-bound
  (b* ((?x (lebs2ip s)))
    (< x (expt 2 (len s))))
  :rule-classes :linear)

Theorem: lebs2ip-injectivity

(defthm lebs2ip-injectivity
  (implies (equal (len s1) (len s2))
           (equal (equal (lebs2ip s1) (lebs2ip s2))
                  (equal (bit-list-fix s1)
                         (bit-list-fix s2)))))