(bfr-=-uu a b) → a=b
Function:
(defun bfr-=-uu (a b) (declare (xargs :guard (and (true-listp a) (true-listp b)))) (let ((__function__ 'bfr-=-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 (bfr-iff head1 head2))) (bfr-and first-eq (bfr-=-uu tail1 tail2)))))
Theorem:
(defthm bfr-=-uu-correct (b* ((a=b (bfr-=-uu a b))) (and (equal (bfr-eval a=b env) (equal (bfr-list->u a env) (bfr-list->u b env))))))
Theorem:
(defthm bfr-=-uu-deps (b* ((a=b (bfr-=-uu a b))) (implies (and (not (pbfr-list-depends-on varname param a)) (not (pbfr-list-depends-on varname param b))) (and (not (pbfr-depends-on varname param a=b))))))