		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-pow

Symbolic version of 4vec-pow.

Signature
(a4vec-pow base exp) → res
Arguments: base — Guard (a4vec-p base).; exp — Guard (a4vec-p exp).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: a4vec-pow

(defun a4vec-pow (base exp)
  (declare (xargs :guard (and (a4vec-p base) (a4vec-p exp))))
  (let ((__function__ 'a4vec-pow))
    (declare (ignorable __function__))
    (a4vec-ite (aig-and (a2vec-p base) (a2vec-p exp))
               (b* ((base (a4vec->lower base))
                    (exp (a4vec->lower exp)))
                 (a4vec-ite (aig-or (aig-not (aig-<-ss exp nil))
                                    (aig-or (aig-=-ss base '(t nil))
                                            (aig-=-ss base '(t))))
                            (b* ((pow (aig-expt-su base exp)))
                              (a4vec pow pow))
                            (a4vec-ite (aig-=-ss base nil)
                                       (a4vec-x)
                                       (a4vec nil nil))))
               (a4vec-x))))

Theorem: a4vec-p-of-a4vec-pow

(defthm a4vec-p-of-a4vec-pow
  (b* ((res (a4vec-pow base exp)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-pow-correct

(defthm a4vec-pow-correct
  (equal (a4vec-eval (a4vec-pow base exp) env)
         (4vec-pow (a4vec-eval base env)
                   (a4vec-eval exp env))))

Theorem: a4vec-pow-of-a4vec-fix-base

(defthm a4vec-pow-of-a4vec-fix-base
  (equal (a4vec-pow (a4vec-fix base) exp)
         (a4vec-pow base exp)))

Theorem: a4vec-pow-a4vec-equiv-congruence-on-base

(defthm a4vec-pow-a4vec-equiv-congruence-on-base
  (implies (a4vec-equiv base base-equiv)
           (equal (a4vec-pow base exp)
                  (a4vec-pow base-equiv exp)))
  :rule-classes :congruence)

Theorem: a4vec-pow-of-a4vec-fix-exp

(defthm a4vec-pow-of-a4vec-fix-exp
  (equal (a4vec-pow base (a4vec-fix exp))
         (a4vec-pow base exp)))

Theorem: a4vec-pow-a4vec-equiv-congruence-on-exp

(defthm a4vec-pow-a4vec-equiv-congruence-on-exp
  (implies (a4vec-equiv exp exp-equiv)
           (equal (a4vec-pow base exp)
                  (a4vec-pow base exp-equiv)))
  :rule-classes :congruence)