		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.

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 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__))
    (rev (trim-bendian* (rev digits)))))

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

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

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

Theorem: trim-lendian*-when-no-ending-0

(defthm trim-lendian*-when-no-ending-0
  (implies (not (zp (car (last digits))))
           (equal (trim-lendian* digits)
                  (nat-list-fix digits))))

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

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

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

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

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

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

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

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

Theorem: trim-lendian*-of-append

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

Theorem: trim-lendian*-of-cons

(defthm trim-lendian*-of-cons
  (implies (and (natp digit) (nat-listp digits))
           (equal (trim-lendian* (cons digit digits))
                  (if (zp-listp digits)
                      (if (zp digit) nil (list digit))
                    (cons digit (trim-lendian* digits))))))

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

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