(bfr-ite-bss-fn-aux c v1 v0) → vv
Function:
(defun bfr-ite-bss-fn-aux (c v1 v0) (declare (xargs :guard (and (true-listp v1) (true-listp v0)))) (let ((__function__ 'bfr-ite-bss-fn-aux)) (declare (ignorable __function__)) (b* (((mv head1 tail1 end1) (first/rest/end v1)) ((mv head0 tail0 end0) (first/rest/end v0)) ((when (and end1 end0)) (bfr-sterm (bfr-ite-fn c head1 head0))) (rst (bfr-ite-bss-fn-aux c tail1 tail0)) (head (bfr-ite c head1 head0))) (bfr-scons head rst))))
Theorem:
(defthm true-listp-of-bfr-ite-bss-fn-aux (b* ((vv (bfr-ite-bss-fn-aux c v1 v0))) (true-listp vv)) :rule-classes :type-prescription)
Theorem:
(defthm bfr-ite-bss-fn-aux-correct (b* ((vv (bfr-ite-bss-fn-aux c v1 v0))) (and (equal (bfr-list->s vv env) (if (bfr-eval c env) (bfr-list->s v1 env) (bfr-list->s v0 env))))))
Theorem:
(defthm bfr-ite-bss-fn-aux-deps (b* ((vv (bfr-ite-bss-fn-aux c v1 v0))) (implies (and (not (pbfr-depends-on varname param c)) (not (pbfr-list-depends-on varname param v1)) (not (pbfr-list-depends-on varname param v0))) (and (not (pbfr-list-depends-on varname param vv))))))