		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Dab-digitp

Recognize valid digits for representing natural numbers as digits in the specified base.

Signature
(dab-digitp base x) → yes/no
Arguments: base — Guard (dab-basep base).
Returns: yes/no — Type (booleanp yes/no).

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

Definitions and Theorems

Function: dab-digitp

(defun dab-digitp (base x)
  (declare (xargs :guard (dab-basep base)))
  (let ((__function__ 'dab-digitp))
    (declare (ignorable __function__))
    (and (natp x)
         (< x (dab-base-fix base)))))

Theorem: booleanp-of-dab-digitp

(defthm booleanp-of-dab-digitp
  (b* ((yes/no (dab-digitp base x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: natp-when-dab-digitp

(defthm natp-when-dab-digitp
  (implies (dab-digitp base x) (natp x))
  :rule-classes :forward-chaining)

Theorem: dab-digitp-of-0

(defthm dab-digitp-of-0
  (dab-digitp base 0))

Theorem: dab-digitp-of-1

(defthm dab-digitp-of-1
  (dab-digitp base 1))

Theorem: dab-digitp-of-dab-base-fix-base

(defthm dab-digitp-of-dab-base-fix-base
  (equal (dab-digitp (dab-base-fix base) x)
         (dab-digitp base x)))

Theorem: dab-digitp-dab-base-equiv-congruence-on-base

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