		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-expt-su

Signature
(aabf-expt-su b e man) → (mv b^e new-man)
Arguments: b — Guard (true-listp b).; e — Guard (true-listp e).

Definitions and Theorems

Function: aabf-expt-su

(defun aabf-expt-su (b e man)
  (declare (xargs :guard (and (true-listp b) (true-listp e))))
  (declare (xargs :guard (and (aabflist-p b man)
                              (aabflist-p e man))))
  (let ((__function__ 'aabf-expt-su))
    (declare (ignorable __function__))
    (b* (((when (aabf-syntactically-zero-p e))
          (mv (list (aabf-true) (aabf-false))
              man))
         ((when (aabf-syntactically-zero-p (cdr e)))
          (aabf-ite-bss-fn (car e)
                           b (list (aabf-true) (aabf-false))
                           man))
         (car (car e))
         (cdr (cdr e))
         ((mv rest man)
          (aabf-nest (aabf-expt-su (aabf-*-ss b b) cdr)
                     man)))
      (aabf-nest (aabf-ite-bss car (aabf-*-ss b rest)
                               rest)
                 man))))

Theorem: trivial-theorem-about-aabf-expt-su

(defthm trivial-theorem-about-aabf-expt-su
  (b* nil
    (b* ((?ignore (aabf-expt-su b e man)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-expt-su.b^e

(defthm true-listp-of-aabf-expt-su.b^e
  (b* (((mv ?b^e ?new-man)
        (aabf-expt-su b e man)))
    (true-listp b^e))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-expt-su

(defthm aabf-extension-p-of-aabf-expt-su
  (b* (((mv ?b^e ?new-man)
        (aabf-expt-su b e man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-expt-su

(defthm aabf-p-of-aabf-expt-su
  (b* (((mv b^e new-man)
        (aabf-expt-su b e man)))
    (implies (and (aabflist-p b man)
                  (aabflist-p e man))
             (and (aabflist-p b^e new-man)))))

Theorem: aabf-eval-of-aabf-expt-su

(defthm aabf-eval-of-aabf-expt-su
 (b* (((mv b^e new-man)
       (aabf-expt-su b e man)))
  (implies
     (and (aabflist-p b man)
          (aabflist-p e man))
     (and (equal (bools->int (aabflist-eval b^e env new-man))
                 (expt (bools->int (aabflist-eval b env man))
                       (bools->uint (aabflist-eval e env man))))))))

Theorem: aabf-pred-of-aabf-expt-su

(defthm aabf-pred-of-aabf-expt-su
  (b* (((mv b^e new-man)
        (aabf-expt-su b e man)))
    (implies (and (aabflist-p b man)
                  (aabflist-p e man)
                  (aabflist-pred b man)
                  (aabflist-pred e man))
             (and (aabflist-pred b^e new-man)))))