Symbolic version of 3vec-?*.
Function:
(defun a4vec-?! (x y z) (declare (xargs :guard (and (a4vec-p x) (a4vec-p y) (a4vec-p z)))) (let ((__function__ 'a4vec-?!)) (declare (ignorable __function__)) (b* (((a4vec a) x) ((a4vec b) y) ((a4vec c) z) (pick-c (aig-iszero-s (aig-logand-ss a.upper a.lower))) (upper (aig-ite-bss pick-c c.upper b.upper)) (lower (aig-ite-bss pick-c c.lower b.lower))) (a4vec upper lower))))
Theorem:
(defthm a4vec-p-of-a4vec-?! (b* ((res (a4vec-?! x y z))) (a4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm a4vec-?!-correct (equal (a4vec-eval (a4vec-?! x y z) env) (4vec-?! (a4vec-eval x env) (a4vec-eval y env) (a4vec-eval z env))))
Theorem:
(defthm a4vec-?!-of-a4vec-fix-x (equal (a4vec-?! (a4vec-fix x) y z) (a4vec-?! x y z)))
Theorem:
(defthm a4vec-?!-a4vec-equiv-congruence-on-x (implies (a4vec-equiv x x-equiv) (equal (a4vec-?! x y z) (a4vec-?! x-equiv y z))) :rule-classes :congruence)
Theorem:
(defthm a4vec-?!-of-a4vec-fix-y (equal (a4vec-?! x (a4vec-fix y) z) (a4vec-?! x y z)))
Theorem:
(defthm a4vec-?!-a4vec-equiv-congruence-on-y (implies (a4vec-equiv y y-equiv) (equal (a4vec-?! x y z) (a4vec-?! x y-equiv z))) :rule-classes :congruence)
Theorem:
(defthm a4vec-?!-of-a4vec-fix-z (equal (a4vec-?! x y (a4vec-fix z)) (a4vec-?! x y z)))
Theorem:
(defthm a4vec-?!-a4vec-equiv-congruence-on-z (implies (a4vec-equiv z z-equiv) (equal (a4vec-?! x y z) (a4vec-?! x y z-equiv))) :rule-classes :congruence)