		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec->4vec

Signature
(s4vec->4vec x) → val
Arguments: x — Guard (s4vec-p x).
Returns: val — Type (4vec-p val).

Definitions and Theorems

Function: s4vec->4vec

(defun s4vec->4vec (x)
  (declare (xargs :guard (s4vec-p x)))
  (let ((__function__ 's4vec->4vec))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((s4vec x)))
           (4vec (sparseint-val x.upper)
                 (sparseint-val x.lower)))
         :exec
         (if (atom x)
             (2vec x)
           (if (cdr x)
               (4vec (sparseint-val (car x))
                     (sparseint-val (cdr x)))
             (2vec (sparseint-val (car x))))))))

Theorem: 4vec-p-of-s4vec->4vec

(defthm 4vec-p-of-s4vec->4vec
  (b* ((val (s4vec->4vec x)))
    (4vec-p val))
  :rule-classes :rewrite)

Theorem: s4vec->4vec-of-make-s4vec

(defthm s4vec->4vec-of-make-s4vec
  (equal (s4vec->4vec (make-s4vec :upper upper :lower lower))
         (4vec (sparseint-val upper)
               (sparseint-val lower))))

Theorem: 4vec->lower-of-s4vec->4vec

(defthm 4vec->lower-of-s4vec->4vec
  (b* ((?val (s4vec->4vec x)))
    (equal (4vec->lower val)
           (sparseint-val (s4vec->lower x)))))

Theorem: 4vec->upper-of-s4vec->4vec

(defthm 4vec->upper-of-s4vec->4vec
  (b* ((?val (s4vec->4vec x)))
    (equal (4vec->upper val)
           (sparseint-val (s4vec->upper x)))))

Theorem: s4vec->4vec-of-s4vec-fix-x

(defthm s4vec->4vec-of-s4vec-fix-x
  (equal (s4vec->4vec (s4vec-fix x))
         (s4vec->4vec x)))

Theorem: s4vec->4vec-s4vec-equiv-congruence-on-x

(defthm s4vec->4vec-s4vec-equiv-congruence-on-x
  (implies (s4vec-equiv x x-equiv)
           (equal (s4vec->4vec x)
                  (s4vec->4vec x-equiv)))
  :rule-classes :congruence)