Recognize expression terms returning C values.
(atc-c-valued-termp term wrld) → yes/no
We just check whether the term is either a pure expression term returning a C value or is a call of a non-recursive function, which we therefore assume to be a target function.
Function:
(defun atc-c-valued-termp (term wrld) (declare (xargs :guard (and (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'atc-c-valued-termp)) (declare (ignorable __function__)) (b* (((when (atc-pure-c-valued-termp term)) t)) (case-match term ((fn . &) (and (symbolp fn) (not (irecursivep+ fn wrld)))) (& nil)))))
Theorem:
(defthm booleanp-of-atc-c-valued-termp (b* ((yes/no (atc-c-valued-termp term wrld))) (booleanp yes/no)) :rule-classes :rewrite)