Check whether
(tailrec-check-nonrec-conditions combine-nonrec nonrec? r q) → (mv yes/no combine)
The conditions are that
Function:
(defun tailrec-check-nonrec-conditions (combine-nonrec nonrec? r q) (declare (xargs :guard (and (pseudo-termp combine-nonrec) (pseudo-termp nonrec?) (symbolp r) (symbolp q)))) (let ((__function__ 'tailrec-check-nonrec-conditions)) (declare (ignorable __function__)) (if (member-eq r (all-vars nonrec?)) (mv nil nil) (let ((combine (subst-expr1 q nonrec? combine-nonrec))) (if (set-equiv (all-vars combine) (list q r)) (mv t combine) (mv nil nil))))))
Theorem:
(defthm booleanp-of-tailrec-check-nonrec-conditions.yes/no (b* (((mv ?yes/no ?combine) (tailrec-check-nonrec-conditions combine-nonrec nonrec? r q))) (booleanp yes/no)) :rule-classes :rewrite)