Decompose
Function:
(defun tailrec-find-nonrec-term (combine-nonrec term-to-try r q) (declare (xargs :guard (and (pseudo-termp combine-nonrec) (pseudo-termp term-to-try) (symbolp r) (symbolp q)))) (let ((__function__ 'tailrec-find-nonrec-term)) (declare (ignorable __function__)) (b* (((mv found combine) (tailrec-check-nonrec-conditions combine-nonrec term-to-try r q)) ((when found) (mv t term-to-try combine)) ((when (or (variablep term-to-try) (fquotep term-to-try))) (mv nil nil nil))) (tailrec-find-nonrec-terms combine-nonrec (fargs term-to-try) r q))))
Function:
(defun tailrec-find-nonrec-terms (combine-nonrec terms-to-try r q) (declare (xargs :guard (and (pseudo-termp combine-nonrec) (pseudo-term-listp terms-to-try) (symbolp r) (symbolp q)))) (let ((__function__ 'tailrec-find-nonrec-terms)) (declare (ignorable __function__)) (cond ((endp terms-to-try) (mv nil nil nil)) (t (b* (((mv found nonrec combine) (tailrec-find-nonrec-term combine-nonrec (car terms-to-try) r q)) ((when found) (mv t nonrec combine))) (tailrec-find-nonrec-terms combine-nonrec (cdr terms-to-try) r q))))))