		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec

Signature
(s4vec upper lower) → result
Arguments: upper — Guard (sparseint-p upper).; lower — Guard (sparseint-p lower).
Returns: result — Type (s4vec-p result).

Definitions and Theorems

Function: s4vec

(defun s4vec (upper lower)
  (declare (xargs :guard (and (sparseint-p upper)
                              (sparseint-p lower))))
  (let ((__function__ 's4vec))
    (declare (ignorable __function__))
    (b* ((upper (sparseint-fix upper))
         (lower (sparseint-fix lower)))
      (if (equal upper lower)
          (if (integerp upper) upper (list upper))
        (cons upper lower)))))

Theorem: s4vec-p-of-s4vec

(defthm s4vec-p-of-s4vec
  (b* ((result (s4vec upper lower)))
    (s4vec-p result))
  :rule-classes :rewrite)

Theorem: s4vec->upper-of-s4vec

(defthm s4vec->upper-of-s4vec
  (b* ((?result (s4vec upper lower)))
    (equal (s4vec->upper result)
           (sparseint-fix upper))))

Theorem: s4vec->lower-of-s4vec

(defthm s4vec->lower-of-s4vec
  (b* ((?result (s4vec upper lower)))
    (equal (s4vec->lower result)
           (sparseint-fix lower))))

Theorem: s4vec-of-sparseint-fix-upper

(defthm s4vec-of-sparseint-fix-upper
  (equal (s4vec (sparseint-fix upper) lower)
         (s4vec upper lower)))

Theorem: s4vec-sparseint-equiv-congruence-on-upper

(defthm s4vec-sparseint-equiv-congruence-on-upper
  (implies (sparseint-equiv upper upper-equiv)
           (equal (s4vec upper lower)
                  (s4vec upper-equiv lower)))
  :rule-classes :congruence)

Theorem: s4vec-of-sparseint-fix-lower

(defthm s4vec-of-sparseint-fix-lower
  (equal (s4vec upper (sparseint-fix lower))
         (s4vec upper lower)))

Theorem: s4vec-sparseint-equiv-congruence-on-lower

(defthm s4vec-sparseint-equiv-congruence-on-lower
  (implies (sparseint-equiv lower lower-equiv)
           (equal (s4vec upper lower)
                  (s4vec upper lower-equiv)))
  :rule-classes :congruence)