		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.