		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Dab-base-fix

Fixing function for dab-basep.

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

Definitions and Theorems

Function: dab-base-fix

(defun dab-base-fix (x)
  (declare (xargs :guard (dab-basep x)))
  (let ((__function__ 'dab-base-fix))
    (declare (ignorable __function__))
    (mbe :logic (max (nfix x) 2) :exec x)))

Theorem: dab-basep-of-dab-base-fix

(defthm dab-basep-of-dab-base-fix
  (b* ((fixed-x (dab-base-fix x)))
    (dab-basep fixed-x))
  :rule-classes :rewrite)

Theorem: posp-of-dab-base-fix

(defthm posp-of-dab-base-fix
  (b* ((fixed-x (dab-base-fix x)))
    (posp fixed-x))
  :rule-classes :type-prescription)

Theorem: dab-base-fix-when-dab-basep

(defthm dab-base-fix-when-dab-basep
  (implies (dab-basep x)
           (equal (dab-base-fix x) x)))