Symbolic version of a3vec-bit?.
Function:
(defun a4vec-bit?! (x y y3p z z3p) (declare (xargs :guard (and (a4vec-p x) (a4vec-p y) (a4vec-p z)))) (let ((__function__ 'a4vec-bit?!)) (declare (ignorable __function__)) (b* (((a4vec a) x) ((a4vec b) y) ((a4vec c) z) (a=1 (aig-logand-ss a.upper a.lower)) (a!=1 (aig-lognot-s a=1)) (upper (aig-logior-ss (aig-logand-ss a=1 b.upper) (aig-logand-ss a!=1 c.upper))) (lower (aig-logior-ss (aig-logand-ss a=1 b.lower) (aig-logand-ss a!=1 c.lower)))) (a4vec upper lower))))
Theorem:
(defthm a4vec-p-of-a4vec-bit?! (b* ((res (a4vec-bit?! x y y3p z z3p))) (a4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm a4vec-bit?!-correct (implies (and (case-split (implies y3p (3vec-p (a4vec-eval y env)))) (case-split (implies z3p (3vec-p (a4vec-eval z env)))) (3vec-p (a4vec-eval x env))) (equal (a4vec-eval (a4vec-bit?! x y y3p z z3p) env) (4vec-bit?! (a4vec-eval x env) (a4vec-eval y env) (a4vec-eval z env)))))
Theorem:
(defthm a4vec-bit?!-of-a4vec-fix-x (equal (a4vec-bit?! (a4vec-fix x) y y3p z z3p) (a4vec-bit?! x y y3p z z3p)))
Theorem:
(defthm a4vec-bit?!-a4vec-equiv-congruence-on-x (implies (a4vec-equiv x x-equiv) (equal (a4vec-bit?! x y y3p z z3p) (a4vec-bit?! x-equiv y y3p z z3p))) :rule-classes :congruence)
Theorem:
(defthm a4vec-bit?!-of-a4vec-fix-y (equal (a4vec-bit?! x (a4vec-fix y) y3p z z3p) (a4vec-bit?! x y y3p z z3p)))
Theorem:
(defthm a4vec-bit?!-a4vec-equiv-congruence-on-y (implies (a4vec-equiv y y-equiv) (equal (a4vec-bit?! x y y3p z z3p) (a4vec-bit?! x y-equiv y3p z z3p))) :rule-classes :congruence)
Theorem:
(defthm a4vec-bit?!-of-a4vec-fix-z (equal (a4vec-bit?! x y y3p (a4vec-fix z) z3p) (a4vec-bit?! x y y3p z z3p)))
Theorem:
(defthm a4vec-bit?!-a4vec-equiv-congruence-on-z (implies (a4vec-equiv z z-equiv) (equal (a4vec-bit?! x y y3p z z3p) (a4vec-bit?! x y y3p z-equiv z3p))) :rule-classes :congruence)