Function:
(defun s3vec-== (x y) (declare (xargs :guard (and (s4vec-p x) (s4vec-p y)))) (let ((__function__ 's3vec-==)) (declare (ignorable __function__)) (s3vec-reduction-and (s3vec-bitnot (s3vec-bitxor x y)))))
Theorem:
(defthm s4vec-p-of-s3vec-== (b* ((res (s3vec-== x y))) (s4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm s3vec-==-correct (b* ((?res (s3vec-== x y))) (equal (s4vec->4vec res) (3vec-== (s4vec->4vec x) (s4vec->4vec y)))))
Theorem:
(defthm s3vec-==-of-s4vec-fix-x (equal (s3vec-== (s4vec-fix x) y) (s3vec-== x y)))
Theorem:
(defthm s3vec-==-s4vec-equiv-congruence-on-x (implies (s4vec-equiv x x-equiv) (equal (s3vec-== x y) (s3vec-== x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm s3vec-==-of-s4vec-fix-y (equal (s3vec-== x (s4vec-fix y)) (s3vec-== x y)))
Theorem:
(defthm s3vec-==-s4vec-equiv-congruence-on-y (implies (s4vec-equiv y y-equiv) (equal (s3vec-== x y) (s3vec-== x y-equiv))) :rule-classes :congruence)