Symbolic version of 3vec-==.
Function:
(defun a3vec-== (x y) (declare (xargs :guard (and (a4vec-p x) (a4vec-p y)))) (let ((__function__ 'a3vec-==)) (declare (ignorable __function__)) (a3vec-reduction-and (a3vec-bitnot (a3vec-bitxor x y)))))
Theorem:
(defthm a4vec-p-of-a3vec-== (b* ((res (a3vec-== x y))) (a4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm a3vec-==-correct (equal (a4vec-eval (a3vec-== x y) env) (3vec-== (a4vec-eval x env) (a4vec-eval y env))))
Theorem:
(defthm a3vec-==-of-a4vec-fix-x (equal (a3vec-== (a4vec-fix x) y) (a3vec-== x y)))
Theorem:
(defthm a3vec-==-a4vec-equiv-congruence-on-x (implies (a4vec-equiv x x-equiv) (equal (a3vec-== x y) (a3vec-== x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm a3vec-==-of-a4vec-fix-y (equal (a3vec-== x (a4vec-fix y)) (a3vec-== x y)))
Theorem:
(defthm a3vec-==-a4vec-equiv-congruence-on-y (implies (a4vec-equiv y y-equiv) (equal (a3vec-== x y) (a3vec-== x y-equiv))) :rule-classes :congruence)