		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Trim-bendian+

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

Signature
(trim-bendian+ 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-bendian+

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

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

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

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

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

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

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

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

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

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

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

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

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