		Search-engine friendly clone of the ACL2 documentation.

Bits-as-digits-in-base-2

Nat=>lebits

Convert a natural number to its little-endian list of bits, seen as digits in base 2, of specified length.

Signature
(nat=>lebits width nat) → digits
Arguments: width — Guard (natp width).; nat — Guard (natp nat).
Returns: digits — Type (bit-listp digits).

Definitions and Theorems

Function: nat=>lebits

(defun nat=>lebits (width nat)
  (declare (xargs :guard (and (natp width) (natp nat))))
  (declare (xargs :guard (< nat (expt 2 width))))
  (let ((__function__ 'nat=>lebits))
    (declare (ignorable __function__))
    (nat=>lendian 2 width nat)))

Theorem: bit-listp-of-nat=>lebits

(defthm bit-listp-of-nat=>lebits
  (b* ((digits (nat=>lebits width nat)))
    (bit-listp digits))
  :rule-classes :rewrite)

Theorem: nat=>lebits-of-nfix-width

(defthm nat=>lebits-of-nfix-width
  (equal (nat=>lebits (nfix width) nat)
         (nat=>lebits width nat)))

Theorem: nat=>lebits-nat-equiv-congruence-on-width

(defthm nat=>lebits-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (nat=>lebits width nat)
                  (nat=>lebits width-equiv nat)))
  :rule-classes :congruence)

Theorem: nat=>lebits-of-nfix-nat

(defthm nat=>lebits-of-nfix-nat
  (equal (nat=>lebits width (nfix nat))
         (nat=>lebits width nat)))

Theorem: nat=>lebits-nat-equiv-congruence-on-nat

(defthm nat=>lebits-nat-equiv-congruence-on-nat
  (implies (nat-equiv nat nat-equiv)
           (equal (nat=>lebits width nat)
                  (nat=>lebits width nat-equiv)))
  :rule-classes :congruence)

Theorem: len-of-nat=>lebits

(defthm len-of-nat=>lebits
  (equal (len (nat=>lebits width nat))
         (nfix width)))

Subtopics

Nat=>lebits-injectivity
Nat=>lebits-of-lebits=>nat
Lebits=>nat-of-nat=>lebits