		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-expt-su

Signature
(bfr-expt-su b e) → b^e
Arguments: b — Guard (true-listp b).; e — Guard (true-listp e).
Returns: b^e — Type (true-listp b^e).

Definitions and Theorems

Function: bfr-expt-su

(defun bfr-expt-su (b e)
  (declare (xargs :guard (and (true-listp b) (true-listp e))))
  (let ((__function__ 'bfr-expt-su))
    (declare (ignorable __function__))
    (b* (((when (all-nil e)) '(t nil))
         ((when (all-nil (cdr e)))
          (bfr-ite-bss (car e) b '(t nil)))
         (rest (bfr-expt-su (bfr-*-ss b b) (cdr e))))
      (bfr-ite-bss (car e)
                   (bfr-*-ss b rest)
                   rest))))

Theorem: true-listp-of-bfr-expt-su

(defthm true-listp-of-bfr-expt-su
  (b* ((b^e (bfr-expt-su b e)))
    (true-listp b^e))
  :rule-classes :type-prescription)

Theorem: bfr-expt-su-correct

(defthm bfr-expt-su-correct
  (b* ((b^e (bfr-expt-su b e)))
    (and (equal (bfr-list->s b^e env)
                (expt (bfr-list->s b env)
                      (bfr-list->u e env))))))

Theorem: bfr-expt-su-deps

(defthm bfr-expt-su-deps
  (b* ((b^e (bfr-expt-su b e)))
    (implies (and (not (pbfr-list-depends-on varname param b))
                  (not (pbfr-list-depends-on varname param e)))
             (and (not (pbfr-list-depends-on varname param b^e))))))