		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

4veclist->upper-4vecs

Signature
(4veclist->upper-4vecs x) → new-x
Arguments: x — Guard (4veclist-p x).
Returns: new-x — Type (4veclist-p new-x).

Definitions and Theorems

Function: 4veclist->upper-4vecs

(defun 4veclist->upper-4vecs (x)
  (declare (xargs :guard (4veclist-p x)))
  (let ((__function__ '4veclist->upper-4vecs))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (2vec (4vec->upper (car x)))
            (4veclist->upper-4vecs (cdr x))))))

Theorem: 4veclist-p-of-4veclist->upper-4vecs

(defthm 4veclist-p-of-4veclist->upper-4vecs
  (b* ((new-x (4veclist->upper-4vecs x)))
    (4veclist-p new-x))
  :rule-classes :rewrite)

Theorem: 4veclist->upper-4vecs-when-integer-listp

(defthm 4veclist->upper-4vecs-when-integer-listp
  (b* nil
    (implies (integer-listp x)
             (equal (4veclist->upper-4vecs x) x))))