Function:
(defun s4vec-===* (left right) (declare (xargs :guard (and (s4vec-p left) (s4vec-p right)))) (let ((__function__ 's4vec-===*)) (declare (ignorable __function__)) (b* (((s4vec left)) ((s4vec right)) (uppers-diff (sparseint-bitxor left.upper right.upper)) (lowers-diff (sparseint-bitxor left.lower right.lower)) (diff (sparseint-bitor uppers-diff lowers-diff)) (left-non-x (sparseint-bitorc1 left.upper left.lower)) (right-non-x (sparseint-bitorc1 right.upper right.lower)) (true (sparseint-equal -1 (sparseint-bitandc1 diff left-non-x))) ((when true) (mbe :logic (s4vec (int-to-sparseint -1) (int-to-sparseint -1)) :exec -1)) (not-false (sparseint-equal 0 (sparseint-bitand left-non-x (sparseint-bitorc2 diff right-non-x)))) ((when not-false) (s4vec-x))) (mbe :logic (s4vec (int-to-sparseint 0) (int-to-sparseint 0)) :exec 0))))
Theorem:
(defthm s4vec-p-of-s4vec-===* (b* ((equal (s4vec-===* left right))) (s4vec-p equal)) :rule-classes :rewrite)
Theorem:
(defthm s4vec-===*-correct (b* ((common-lisp::?equal (s4vec-===* left right))) (equal (s4vec->4vec equal) (4vec-===* (s4vec->4vec left) (s4vec->4vec right)))))
Theorem:
(defthm s4vec-===*-of-s4vec-fix-left (equal (s4vec-===* (s4vec-fix left) right) (s4vec-===* left right)))
Theorem:
(defthm s4vec-===*-s4vec-equiv-congruence-on-left (implies (s4vec-equiv left left-equiv) (equal (s4vec-===* left right) (s4vec-===* left-equiv right))) :rule-classes :congruence)
Theorem:
(defthm s4vec-===*-of-s4vec-fix-right (equal (s4vec-===* left (s4vec-fix right)) (s4vec-===* left right)))
Theorem:
(defthm s4vec-===*-s4vec-equiv-congruence-on-right (implies (s4vec-equiv right right-equiv) (equal (s4vec-===* left right) (s4vec-===* left right-equiv))) :rule-classes :congruence)