		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-expt-su

Signature
(sv::aig-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: aig-expt-su

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

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

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

Theorem: aig-expt-su-correct

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