		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Dab-digit-list-fix

Fixing function for dab-digit-listp.

Signature
(dab-digit-list-fix base x) → fixed-x
Arguments: base — Guard (dab-basep base).; x — Guard (dab-digit-listp base x).
Returns: fixed-x — Type (dab-digit-listp base fixed-x).

Definitions and Theorems

Function: dab-digit-list-fix

(defun dab-digit-list-fix (base x)
  (declare (xargs :guard (and (dab-basep base)
                              (dab-digit-listp base x))))
  (let ((__function__ 'dab-digit-list-fix))
    (declare (ignorable __function__))
    (mbe :logic (cond ((atom x) nil)
                      (t (cons (dab-digit-fix base (car x))
                               (dab-digit-list-fix base (cdr x)))))
         :exec x)))

Theorem: return-type-of-dab-digit-list-fix

(defthm return-type-of-dab-digit-list-fix
  (b* ((fixed-x (dab-digit-list-fix base x)))
    (dab-digit-listp base fixed-x))
  :rule-classes :rewrite)

Theorem: nat-listp-of-dab-digit-list-fix

(defthm nat-listp-of-dab-digit-list-fix
  (b* ((fixed-x (dab-digit-list-fix base x)))
    (nat-listp fixed-x))
  :rule-classes :rewrite)

Theorem: dab-digit-list-fix-of-true-list-fix

(defthm dab-digit-list-fix-of-true-list-fix
  (equal (dab-digit-list-fix base (true-list-fix digits))
         (dab-digit-list-fix base digits)))

Theorem: dab-digit-list-fix-when-dab-digit-listp

(defthm dab-digit-list-fix-when-dab-digit-listp
  (implies (dab-digit-listp base x)
           (equal (dab-digit-list-fix base x) x)))

Theorem: dab-digit-list-fix-of-nil

(defthm dab-digit-list-fix-of-nil
  (equal (dab-digit-list-fix base nil)
         nil))

Theorem: dab-digit-list-fix-of-cons

(defthm dab-digit-list-fix-of-cons
  (equal (dab-digit-list-fix base (cons x y))
         (cons (dab-digit-fix base x)
               (dab-digit-list-fix base y))))

Theorem: dab-digit-list-fix-of-append

(defthm dab-digit-list-fix-of-append
  (equal (dab-digit-list-fix base (append x y))
         (append (dab-digit-list-fix base x)
                 (dab-digit-list-fix base y))))

Theorem: len-of-dab-digit-list-fix

(defthm len-of-dab-digit-list-fix
  (equal (len (dab-digit-list-fix base x))
         (len x)))

Theorem: consp-of-dab-digit-list-fix

(defthm consp-of-dab-digit-list-fix
  (equal (consp (dab-digit-list-fix base x))
         (consp x)))

Theorem: car-of-dab-digit-list-fix

(defthm car-of-dab-digit-list-fix
  (implies (consp x)
           (equal (car (dab-digit-list-fix base x))
                  (dab-digit-fix base (car x)))))

Theorem: cdr-of-dab-digit-list-fix

(defthm cdr-of-dab-digit-list-fix
  (implies (consp x)
           (equal (cdr (dab-digit-list-fix base x))
                  (dab-digit-list-fix base (cdr x)))))

Theorem: rev-of-dab-digit-list-fix

(defthm rev-of-dab-digit-list-fix
  (equal (rev (dab-digit-list-fix base x))
         (dab-digit-list-fix base (rev x))))

Theorem: nat-list-fix-of-dab-digit-list-fix

(defthm nat-list-fix-of-dab-digit-list-fix
  (equal (nat-list-fix (dab-digit-list-fix base x))
         (dab-digit-list-fix base x)))

Theorem: dab-digit-list-fix-of-dab-base-fix-base

(defthm dab-digit-list-fix-of-dab-base-fix-base
  (equal (dab-digit-list-fix (dab-base-fix base)
                             x)
         (dab-digit-list-fix base x)))

Theorem: dab-digit-list-fix-dab-base-equiv-congruence-on-base

(defthm dab-digit-list-fix-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (dab-digit-list-fix base x)
                  (dab-digit-list-fix base-equiv x)))
  :rule-classes :congruence)