		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Dab-digit-fix

Fixing function for dab-digitp.

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

Definitions and Theorems

Function: dab-digit-fix

(defun dab-digit-fix (base x)
  (declare (xargs :guard (and (dab-basep base)
                              (dab-digitp base x))))
  (let ((__function__ 'dab-digit-fix))
    (declare (ignorable __function__))
    (mbe :logic (if (dab-digitp base x) x 0)
         :exec x)))

Theorem: return-type-of-dab-digit-fix

(defthm return-type-of-dab-digit-fix
  (b* ((fixed-x (dab-digit-fix base x)))
    (dab-digitp base fixed-x))
  :rule-classes :rewrite)

Theorem: natp-of-dab-digit-fix

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

Theorem: dab-digit-fix-upper-bound

(defthm dab-digit-fix-upper-bound
  (b* ((fixed-x (dab-digit-fix base x)))
    (< fixed-x (dab-base-fix base)))
  :rule-classes :linear)

Theorem: dab-digit-fix-when-dab-digitp

(defthm dab-digit-fix-when-dab-digitp
  (implies (dab-digitp base x)
           (equal (dab-digit-fix base x) x)))

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

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

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

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