(sv::aig-ite-bvv-fn-aux c v1 v0) → vv
Function:
(defun sv::aig-ite-bvv-fn-aux (c v1 v0) (declare (xargs :guard (and (true-listp v1) (true-listp v0)))) (let ((__function__ 'sv::aig-ite-bvv-fn-aux)) (declare (ignorable __function__)) (b* (((when (and (atom v1) (atom v0))) nil) ((mv v11 v1r) (car/cdr v1)) ((mv v01 v0r) (car/cdr v0)) (tail (sv::aig-ite-bvv-fn-aux c v1r v0r)) (head (acl2::aig-ite c v11 v01))) (sv::aig-ucons head tail))))
Theorem:
(defthm sv::true-listp-of-aig-ite-bvv-fn-aux (b* ((vv (sv::aig-ite-bvv-fn-aux c v1 v0))) (true-listp vv)) :rule-classes :type-prescription)
Theorem:
(defthm sv::aig-ite-bvv-fn-aux-correct (b* ((vv (sv::aig-ite-bvv-fn-aux c v1 v0))) (and (equal (sv::aig-list->u vv env) (if (acl2::aig-eval c env) (sv::aig-list->u v1 env) (sv::aig-list->u v0 env))))))