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