(a4vec-===*-bit a.upper a.lower b.upper b.lower) → (mv true not-false)
Function:
(defun a4vec-===*-bit (a.upper a.lower b.upper b.lower) (declare (xargs :guard t)) (let ((__function__ 'a4vec-===*-bit)) (declare (ignorable __function__)) (b* ((diff (aig-or (aig-xor a.upper b.upper) (aig-xor a.lower b.lower))) (a-non-x (aig-or (aig-not a.upper) a.lower)) (b-non-x (aig-or (aig-not b.upper) b.lower)) (true (aig-and (aig-not diff) a-non-x)) (not-false (aig-not (aig-and a-non-x (aig-or diff (aig-not b-non-x)))))) (mv true not-false))))