		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4veclist->upper-a4vecs

Signature
(a4veclist->upper-a4vecs x) → new-x
Arguments: x — Guard (a4veclist-p x).
Returns: new-x — Type (a4veclist-p new-x).

Definitions and Theorems

Function: a4veclist->upper-a4vecs

(defun a4veclist->upper-a4vecs (x)
  (declare (xargs :guard (a4veclist-p x)))
  (let ((__function__ 'a4veclist->upper-a4vecs))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (b* ((upper (a4vec->upper (car x))))
                   (a4vec upper upper))
                 (a4veclist->upper-a4vecs (cdr x))))
         :exec (a4veclist->upper-a4vecs-acc x nil))))

Theorem: a4veclist-p-of-a4veclist->upper-a4vecs

(defthm a4veclist-p-of-a4veclist->upper-a4vecs
  (b* ((new-x (a4veclist->upper-a4vecs x)))
    (a4veclist-p new-x))
  :rule-classes :rewrite)

Theorem: eval-of-a4veclist->upper-a4vecs

(defthm eval-of-a4veclist->upper-a4vecs
  (b* ((?new-x (a4veclist->upper-a4vecs x)))
    (equal (a4veclist-eval new-x env)
           (4veclist->upper-4vecs (a4veclist-eval x env)))))