		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-pow

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

Definitions and Theorems

Function: s4vec-pow

(defun s4vec-pow (base exp)
 (declare (xargs :guard (and (s4vec-p base) (s4vec-p exp))))
 (let ((__function__ 's4vec-pow))
  (declare (ignorable __function__))
  (b*
   (((unless (and (s4vec-2vec-p base)
                  (s4vec-2vec-p exp)))
     (s4vec-x))
    (expint (s4vec->upper exp))
    (baseint (s4vec->upper base))
    ((when (sparseint-equal expint 0))
     (s2vec 1))
    ((when (sparseint-< expint 0))
     (b*
      (((when (sparseint-equal baseint 0))
        (s4vec-x))
       ((when (sparseint-equal baseint 1))
        (s2vec 1))
       ((when (sparseint-equal baseint -1))
        (s2vec
          (int-to-sparseint (- 1 (* 2 (sparseint-bit 0 expint)))))))
      (s2vec 0)))
    ((when (or (sparseint-equal expint 1)
               (sparseint-equal baseint 0)
               (sparseint-equal baseint 1)))
     (s2vec baseint))
    ((when (sparseint-equal baseint -1))
     (s2vec
          (int-to-sparseint (- 1 (* 2 (sparseint-bit 0 expint))))))
    (expval (s4vec-sparseint-val expint))
    (baseval (s4vec-sparseint-val baseint)))
   (s2vec (int-to-sparseint (expt baseval expval))))))

Theorem: s4vec-p-of-s4vec-pow

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

Theorem: s4vec-pow-correct

(defthm s4vec-pow-correct
  (b* ((?res (s4vec-pow base exp)))
    (equal (s4vec->4vec res)
           (4vec-pow (s4vec->4vec base)
                     (s4vec->4vec exp)))))

Theorem: s4vec-pow-of-s4vec-fix-base

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

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

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

Theorem: s4vec-pow-of-s4vec-fix-exp

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

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

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