Symbolic version of 4vec-===.
Function:
(defun a4vec-=== (x y) (declare (xargs :guard (and (a4vec-p x) (a4vec-p y)))) (let ((__function__ 'a4vec-===)) (declare (ignorable __function__)) (b* (((a4vec x)) ((a4vec y)) (val (aig-sterm (aig-and (aig-=-ss x.upper y.upper) (aig-=-ss x.lower y.lower))))) (a4vec val val))))
Theorem:
(defthm a4vec-p-of-a4vec-=== (b* ((res (a4vec-=== x y))) (a4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm a4vec-===-correct (equal (a4vec-eval (a4vec-=== x y) env) (4vec-=== (a4vec-eval x env) (a4vec-eval y env))))
Theorem:
(defthm a4vec-===-of-a4vec-fix-x (equal (a4vec-=== (a4vec-fix x) y) (a4vec-=== x y)))
Theorem:
(defthm a4vec-===-a4vec-equiv-congruence-on-x (implies (a4vec-equiv x x-equiv) (equal (a4vec-=== x y) (a4vec-=== x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm a4vec-===-of-a4vec-fix-y (equal (a4vec-=== x (a4vec-fix y)) (a4vec-=== x y)))
Theorem:
(defthm a4vec-===-a4vec-equiv-congruence-on-y (implies (a4vec-equiv y y-equiv) (equal (a4vec-=== x y) (a4vec-=== x y-equiv))) :rule-classes :congruence)