		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.

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 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__))
    (cond ((endp digits) nil)
          ((zp (car digits))
           (trim-bendian* (cdr digits)))
          (t (mbe :logic (nat-list-fix digits)
                  :exec digits)))))

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) nil)))

Theorem: trim-bendian*-of-append-zeros

(defthm trim-bendian*-of-append-zeros
  (implies (zp-listp zeros)
           (equal (trim-bendian* (append zeros digits))
                  (trim-bendian* digits))))

Theorem: trim-bendian*-when-no-starting-0

(defthm trim-bendian*-when-no-starting-0
  (implies (not (zp (car digits)))
           (equal (trim-bendian* digits)
                  (nat-list-fix digits))))

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

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

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

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

Theorem: len-of-trim-bendian*-upper-bound

(defthm len-of-trim-bendian*-upper-bound
  (<= (len (trim-bendian* digits))
      (len digits))
  :rule-classes :linear)

Theorem: append-of-repeat-and-trim-bendian*

(defthm append-of-repeat-and-trim-bendian*
  (equal (append (repeat (- (len digits)
                            (len (trim-bendian* digits)))
                         0)
                 (trim-bendian* digits))
         (nat-list-fix digits)))

Theorem: trim-bendian*-of-append

(defthm trim-bendian*-of-append
  (equal (trim-bendian* (append hidigits lodigits))
         (if (zp-listp (true-list-fix hidigits))
             (trim-bendian* lodigits)
           (append (trim-bendian* hidigits)
                   (nat-list-fix lodigits)))))

Theorem: trim-bendian*-of-cons

(defthm trim-bendian*-of-cons
  (equal (trim-bendian* (cons digit digits))
         (if (zp digit)
             (trim-bendian* digits)
           (cons (nfix digit)
                 (nat-list-fix digits)))))

Theorem: trim-bendian*-iff-not-zp-listp

(defthm trim-bendian*-iff-not-zp-listp
  (implies (true-listp digits)
           (iff (trim-bendian* digits)
                (not (zp-listp 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)