Check if the static parameters do not change
in the arguments of the recursive calls of
(parteval-unchanging-static-in-rec-calls-p rec-calls-with-tests old$ y1...ym wrld) → yes/no
This is used to check if a recursive
Function:
(defun parteval-unchanging-static-in-rec-calls-p (rec-calls-with-tests old$ y1...ym wrld) (declare (xargs :guard (and (pseudo-tests-and-call-listp rec-calls-with-tests) (symbolp old$) (symbol-listp y1...ym) (plist-worldp wrld)))) (let ((__function__ 'parteval-unchanging-static-in-rec-calls-p)) (declare (ignorable __function__)) (or (endp rec-calls-with-tests) (b* ((rec-call-with-tests (car rec-calls-with-tests)) (rec-call (access tests-and-call rec-call-with-tests :call)) (rec-args (fargs rec-call))) (and (parteval-unchanging-static-in-rec-args-p rec-args old$ y1...ym wrld) (parteval-unchanging-static-in-rec-calls-p (cdr rec-calls-with-tests) old$ y1...ym wrld))))))
Theorem:
(defthm booleanp-of-parteval-unchanging-static-in-rec-calls-p (b* ((yes/no (parteval-unchanging-static-in-rec-calls-p rec-calls-with-tests old$ y1...ym wrld))) (booleanp yes/no)) :rule-classes :rewrite)