Function:
(defun s4vec-concat (width low high) (declare (xargs :guard (and (s4vec-p width) (s4vec-p low) (s4vec-p high)))) (let ((__function__ 's4vec-concat)) (declare (ignorable __function__)) (b* (((unless (s4vec-index-p width)) (s4vec-x)) (widthval (s4vec-sparseint-val (s4vec->upper width)))) (if-s2vec-p (low high) (s2vec (sparseint-concatenate widthval (s2vec->val low) (s2vec->val high))) (b* (((s4vec low)) ((s4vec high))) (s4vec (sparseint-concatenate widthval low.upper high.upper) (sparseint-concatenate widthval low.lower high.lower)))))))
Theorem:
(defthm s4vec-p-of-s4vec-concat (b* ((res (s4vec-concat width low high))) (s4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm s4vec-concat-correct (b* ((?res (s4vec-concat width low high))) (equal (s4vec->4vec res) (4vec-concat (s4vec->4vec width) (s4vec->4vec low) (s4vec->4vec high)))))
Theorem:
(defthm s4vec-concat-of-s4vec-fix-width (equal (s4vec-concat (s4vec-fix width) low high) (s4vec-concat width low high)))
Theorem:
(defthm s4vec-concat-s4vec-equiv-congruence-on-width (implies (s4vec-equiv width width-equiv) (equal (s4vec-concat width low high) (s4vec-concat width-equiv low high))) :rule-classes :congruence)
Theorem:
(defthm s4vec-concat-of-s4vec-fix-low (equal (s4vec-concat width (s4vec-fix low) high) (s4vec-concat width low high)))
Theorem:
(defthm s4vec-concat-s4vec-equiv-congruence-on-low (implies (s4vec-equiv low low-equiv) (equal (s4vec-concat width low high) (s4vec-concat width low-equiv high))) :rule-classes :congruence)
Theorem:
(defthm s4vec-concat-of-s4vec-fix-high (equal (s4vec-concat width low (s4vec-fix high)) (s4vec-concat width low high)))
Theorem:
(defthm s4vec-concat-s4vec-equiv-congruence-on-high (implies (s4vec-equiv high high-equiv) (equal (s4vec-concat width low high) (s4vec-concat width low high-equiv))) :rule-classes :congruence)