		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Dab-basep

Recognize valid bases for representing natural numbers as digits.

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

The fixing function for this predicate is dab-base-fix and the fixtype for this predicate is dab-base.

Any integer above 1 raised to a positive power is a valid base, e.g. binary, octal, and hexadecimal bases.

Definitions and Theorems

Function: dab-basep

(defun dab-basep (x)
  (declare (xargs :guard t))
  (let ((__function__ 'dab-basep))
    (declare (ignorable __function__))
    (and (integerp x) (>= x 2))))

Theorem: booleanp-of-dab-basep

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

Theorem: posp-when-dab-basep

(defthm posp-when-dab-basep
  (implies (dab-basep x) (posp x))
  :rule-classes :compound-recognizer)

Theorem: dab-basep-of-expt

(defthm dab-basep-of-expt
  (implies (and (integerp x) (> x 1) (posp n))
           (dab-basep (expt x n))))