		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Trim-lendian+

Remove all the most significant zero digits from a little-endian representation, but leave one zero if all the digits are zero.

Signature
(trim-lendian+ digits) → trimmed-digits
Arguments: digits — Guard (nat-listp digits).
Returns: trimmed-digits — Type (nat-listp trimmed-digits).

This produces a minimal-length non-empty representation with the same value.

This operation does not depend on a base. It maps lists of natural numbers to lists of natural numbers, where the natural numbers may be digit in any suitable base.

Definitions and Theorems

Function: trim-lendian+

(defun trim-lendian+ (digits)
  (declare (xargs :guard (nat-listp digits)))
  (let ((__function__ 'trim-lendian+))
    (declare (ignorable __function__))
    (b* ((digits (trim-lendian* digits)))
      (or digits (list 0)))))

Theorem: nat-listp-of-trim-lendian+

(defthm nat-listp-of-trim-lendian+
  (b* ((trimmed-digits (trim-lendian+ digits)))
    (nat-listp trimmed-digits))
  :rule-classes :rewrite)

Theorem: trim-lendian+-of-true-list-fix

(defthm trim-lendian+-of-true-list-fix
  (equal (trim-lendian+ (true-list-fix digits))
         (trim-lendian+ digits)))

Theorem: trim-lendian+-when-zp-listp

(defthm trim-lendian+-when-zp-listp
  (implies (zp-listp digits)
           (equal (trim-lendian+ digits)
                  (list 0))))

Theorem: lendian=>nat-of-trim-lendian+

(defthm lendian=>nat-of-trim-lendian+
  (equal (lendian=>nat base (trim-lendian+ digits))
         (lendian=>nat base digits)))

Theorem: trim-lendian+-of-nat-list-fix-digits

(defthm trim-lendian+-of-nat-list-fix-digits
  (equal (trim-lendian+ (nat-list-fix digits))
         (trim-lendian+ digits)))

Theorem: trim-lendian+-nat-list-equiv-congruence-on-digits

(defthm trim-lendian+-nat-list-equiv-congruence-on-digits
  (implies (nat-list-equiv digits digits-equiv)
           (equal (trim-lendian+ digits)
                  (trim-lendian+ digits-equiv)))
  :rule-classes :congruence)