(aig-iff x y) constructs an AIG representing
(aig-iff x y) → aig
Function:
(defun aig-iff (x y) (declare (xargs :guard t)) (let ((__function__ 'aig-iff)) (declare (ignorable __function__)) (aig-or (aig-and x y) (aig-and (aig-not x) (aig-not y)))))
Theorem:
(defthm aig-eval-iff (equal (aig-eval (aig-iff x y) env) (iff (aig-eval x env) (aig-eval y env))))