(a4vec-wildeq-safe-bit au al bu bl) → (mv wildeq-safe-p-upper wildeq-safe-p-lower)
Function:
(defun a4vec-wildeq-safe-bit (au al bu bl) (declare (xargs :guard t)) (let ((__function__ 'a4vec-wildeq-safe-bit)) (declare (ignorable __function__)) (b* ((bz (aig-and (aig-not bu) bl)) ((when (eq bz t)) (mv t t)) (bx (aig-and bu (aig-not bl))) ((when (eq bx t)) (mv t nil)) (axz (aig-xor au al)) ((when (eq axz t)) (mv t bz)) (a=b (aig-iff au bu))) (mv (aig-or a=b (aig-or bz bx) axz) (aig-or (aig-and a=b (aig-not bx) (aig-not axz)) bz)))))
Theorem:
(defthm a4vec-wildeq-safe-bit-eval (b* (((mv upper lower) (a4vec-wildeq-safe-bit a.upper a.lower b.upper b.lower))) (and (equal (aig-eval upper env) (or (iff (aig-eval a.upper env) (aig-eval b.upper env)) (and (not (aig-eval b.upper env)) (aig-eval b.lower env)) (and (aig-eval b.upper env) (not (aig-eval b.lower env))) (xor (aig-eval a.upper env) (aig-eval a.lower env)))) (equal (aig-eval lower env) (or (and (iff (aig-eval a.upper env) (aig-eval b.upper env)) (not (and (aig-eval b.upper env) (not (aig-eval b.lower env)))) (iff (aig-eval a.upper env) (aig-eval a.lower env))) (and (not (aig-eval b.upper env)) (aig-eval b.lower env)))))))