		Search-engine friendly clone of the ACL2 documentation.

Defdigit-grouping-implementation

Defdigit-grouping-find-exp

Find the exponent exp that relates the smaller and larger bases.

Signature
(defdigit-grouping-find-exp smaller larger) → exp?
Arguments: smaller — Guard (dab-basep smaller).; larger — Guard (dab-basep larger).
Returns: exp? — Type (maybe-posp exp?).

This is the logarithm to base smaller of larger, i.e. the exponent exp such that larger is smaller^exp. If exp is not a positive integer, we return nil. If the two bases are the same, we return 1.

Definitions and Theorems

Function: defdigit-grouping-find-exp

(defun defdigit-grouping-find-exp (smaller larger)
  (declare (xargs :guard (and (dab-basep smaller)
                              (dab-basep larger))))
  (let ((__function__ 'defdigit-grouping-find-exp))
    (declare (ignorable __function__))
    (b* (((unless (mbt (and (dab-basep smaller)
                            (dab-basep larger))))
          nil)
         (larger2 (/ larger smaller))
         ((unless (posp larger2)) nil)
         ((when (= larger2 1)) 1)
         (exp2? (defdigit-grouping-find-exp smaller larger2))
         ((unless exp2?) nil))
      (1+ exp2?))))

Theorem: maybe-posp-of-defdigit-grouping-find-exp

(defthm maybe-posp-of-defdigit-grouping-find-exp
  (b* ((exp? (defdigit-grouping-find-exp smaller larger)))
    (maybe-posp exp?))
  :rule-classes :rewrite)