Function:
(defun a4vec-===* (a b) (declare (xargs :guard (and (a4vec-p a) (a4vec-p b)))) (let ((__function__ 'a4vec-===*)) (declare (ignorable __function__)) (b* (((a4vec a)) ((a4vec b)) ((mv true not-false) (a4vec-===*-aux a.upper a.lower b.upper b.lower))) (a4vec (aig-sterm (aig-or true not-false)) (aig-sterm true)))))
Theorem:
(defthm a4vec-p-of-a4vec-===* (b* ((ans (a4vec-===* a b))) (a4vec-p ans)) :rule-classes :rewrite)
Theorem:
(defthm a4vec-===*-correct (b* ((?ans (a4vec-===* a b))) (b* ((spec (4vec-===* (a4vec-eval a env) (a4vec-eval b env)))) (equal (a4vec-eval ans env) spec))))
Theorem:
(defthm a4vec-===*-of-a4vec-fix-a (equal (a4vec-===* (a4vec-fix a) b) (a4vec-===* a b)))
Theorem:
(defthm a4vec-===*-a4vec-equiv-congruence-on-a (implies (a4vec-equiv a a-equiv) (equal (a4vec-===* a b) (a4vec-===* a-equiv b))) :rule-classes :congruence)
Theorem:
(defthm a4vec-===*-of-a4vec-fix-b (equal (a4vec-===* a (a4vec-fix b)) (a4vec-===* a b)))
Theorem:
(defthm a4vec-===*-a4vec-equiv-congruence-on-b (implies (a4vec-equiv b b-equiv) (equal (a4vec-===* a b) (a4vec-===* a b-equiv))) :rule-classes :congruence)