		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Dab-digit-listp

Recognize true lists of digits in the specified base.

Signature
(dab-digit-listp base x) → std::bool

The fixing function for this predicate is dab-digit-list-fix.

Definitions and Theorems

Function: dab-digit-listp

(defun dab-digit-listp (base x)
       (declare (xargs :guard (dab-basep base)))
       (let ((__function__ 'dab-digit-listp))
            (declare (ignorable __function__))
            (if (consp x)
                (and (dab-digitp base (car x))
                     (dab-digit-listp base (cdr x)))
                (null x))))

Theorem: natp-listp-when-dab-digit-listp

(defthm natp-listp-when-dab-digit-listp
        (implies (dab-digit-listp base x)
                 (nat-listp x)))

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

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

Theorem: dab-digit-listp-dab-base-equiv-congruence-on-base

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

Subtopics

Dab-digit-listp-basics: Basic theorems about dab-digit-listp, generated by std::deflist.