(aabf-ite-buu-fn-aux c v1 v0 man) → (mv vv new-man)
Function:
(defun aabf-ite-buu-fn-aux (c v1 v0 man) (declare (xargs :guard (and (true-listp v1) (true-listp v0)))) (declare (xargs :guard (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v0 man)))) (let ((__function__ 'aabf-ite-buu-fn-aux)) (declare (ignorable __function__)) (b* (((when (and (atom v1) (atom v0))) (mv nil man)) (v11 (aabf-car v1)) (v1r (cdr v1)) (v01 (aabf-car v0)) (v0r (cdr v0)) ((mv tail man) (aabf-ite-buu-fn-aux c v1r v0r man)) ((mv head man) (aabf-ite c v11 v01 man))) (mv (aabf-ucons head tail) man))))
Theorem:
(defthm trivial-theorem-about-aabf-ite-buu-fn-aux (b* nil (b* ((?ignore (aabf-ite-buu-fn-aux c v1 v0 man))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-aabf-ite-buu-fn-aux.vv (b* (((mv ?vv ?new-man) (aabf-ite-buu-fn-aux c v1 v0 man))) (true-listp vv)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-extension-p-of-aabf-ite-buu-fn-aux (b* (((mv ?vv ?new-man) (aabf-ite-buu-fn-aux c v1 v0 man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-ite-buu-fn-aux (b* (((mv vv new-man) (aabf-ite-buu-fn-aux c v1 v0 man))) (implies (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v0 man)) (and (aabflist-p vv new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-ite-buu-fn-aux (b* (((mv vv new-man) (aabf-ite-buu-fn-aux c v1 v0 man))) (implies (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v0 man)) (and (equal (bools->uint (aabflist-eval vv env new-man)) (if (aabf-eval c env man) (bools->uint (aabflist-eval v1 env man)) (bools->uint (aabflist-eval v0 env man))))))))
Theorem:
(defthm aabf-pred-of-aabf-ite-buu-fn-aux (b* (((mv vv new-man) (aabf-ite-buu-fn-aux c v1 v0 man))) (implies (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v0 man) (aabf-pred c man) (aabflist-pred v1 man) (aabflist-pred v0 man)) (and (aabflist-pred vv new-man)))))