Recognize statement terms that are not expression terms returning C values.
(atc-stmt-noncval-termp term wrld) → yes/no
We just check if the term is an if, an mv, a let, an mv-let, or a call of a recursive function, which we therefore assume to be a target function.
Function:
(defun atc-stmt-noncval-termp (term wrld) (declare (xargs :guard (and (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'atc-stmt-noncval-termp)) (declare (ignorable __function__)) (b* (((mv ifp & & &) (check-if-call term)) ((when ifp) t) ((mv mvp &) (check-list-call term)) ((when mvp) t) ((mv mv-letp & & & & & &) (check-mv-let-call term)) ((when mv-letp) t)) (case-match term ((fn . &) (or (consp fn) (consp (irecursivep+ fn wrld)))) (& nil)))))
Theorem:
(defthm booleanp-of-atc-stmt-noncval-termp (b* ((yes/no (atc-stmt-noncval-termp term wrld))) (booleanp yes/no)) :rule-classes :rewrite)