(sv::aig-=-uu a b) → a=b
Function:
(defun sv::aig-=-uu (a b) (declare (xargs :guard (and (true-listp a) (true-listp b)))) (let ((__function__ 'sv::aig-=-uu)) (declare (ignorable __function__)) (b* (((when (and (atom a) (atom b))) t) ((mv head1 tail1) (car/cdr a)) ((mv head2 tail2) (car/cdr b)) (first-eq (acl2::aig-iff head1 head2))) (acl2::aig-and first-eq (sv::aig-=-uu tail1 tail2)))))
Theorem:
(defthm sv::aig-=-uu-correct (b* ((a=b (sv::aig-=-uu a b))) (and (equal (acl2::aig-eval a=b env) (equal (sv::aig-list->u a env) (sv::aig-list->u b env))))))