Function:
(defun mask-for-generic-signx$inline (outer-mask) (declare (xargs :guard (4vmask-p outer-mask))) (let ((__function__ 'mask-for-generic-signx)) (declare (ignorable __function__)) (b* ((mask (4vmask-fix outer-mask))) (if (sparseint-< mask 0) -1 (let* ((mask-upper-bound (+ 1 (sparseint-length mask)))) (sparseint-concatenate mask-upper-bound -1 0))))))
Theorem:
(defthm 4vmask-p-of-mask-for-generic-signx (b* ((arg-mask (mask-for-generic-signx$inline outer-mask))) (4vmask-p arg-mask)) :rule-classes :type-prescription)
Theorem:
(defthm mask-for-generic-signx$inline-of-4vmask-fix-outer-mask (equal (mask-for-generic-signx$inline (4vmask-fix outer-mask)) (mask-for-generic-signx$inline outer-mask)))
Theorem:
(defthm mask-for-generic-signx$inline-4vmask-equiv-congruence-on-outer-mask (implies (4vmask-equiv outer-mask outer-mask-equiv) (equal (mask-for-generic-signx$inline outer-mask) (mask-for-generic-signx$inline outer-mask-equiv))) :rule-classes :congruence)
Theorem:
(defthm mask-for-generic-signx-correct-for-signx (equal (4vec-mask mask (4vec-sign-ext n (4vec-mask (mask-for-generic-signx mask) x))) (4vec-mask mask (4vec-sign-ext n x))))
Theorem:
(defthm mask-for-generic-signx-specialized-for-signx (implies (and (equal (4vec-mask (mask-for-generic-signx mask) val1) (4vec-mask (mask-for-generic-signx mask) val2)) (syntaxp (term-order val2 val1))) (equal (4vec-mask mask (4vec-sign-ext n val2)) (4vec-mask mask (4vec-sign-ext n val1)))))
Theorem:
(defthm mask-for-generic-signx-correct-for-concat-x (equal (4vec-mask mask (4vec-concat n (4vec-mask (mask-for-generic-signx mask) x) y)) (4vec-mask mask (4vec-concat n x y))))
Theorem:
(defthm mask-for-generic-signx-correct-for-concat-y (equal (4vec-mask mask (4vec-concat n x (4vec-mask (mask-for-generic-signx mask) y))) (4vec-mask mask (4vec-concat n x y))))
Theorem:
(defthm mask-for-generic-signx-specialized-for-concat-x (implies (and (equal (4vec-mask (mask-for-generic-signx mask) xval1) (4vec-mask (mask-for-generic-signx mask) xval2)) (syntaxp (term-order xval2 xval1))) (equal (4vec-mask mask (4vec-concat n xval1 yval)) (4vec-mask mask (4vec-concat n xval2 yval)))))
Theorem:
(defthm mask-for-generic-signx-specialized-for-concat-y (implies (and (equal (4vec-mask (mask-for-generic-signx mask) yval1) (4vec-mask (mask-for-generic-signx mask) yval2)) (syntaxp (term-order yval2 yval1))) (equal (4vec-mask mask (4vec-concat n xval yval1)) (4vec-mask mask (4vec-concat n xval yval2)))))