		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-unchanging-static-in-rec-calls-p

Check if the static parameters do not change in the arguments of the recursive calls of old.

Signature
(parteval-unchanging-static-in-rec-calls-p rec-calls-with-tests old$ y1...ym wrld) → yes/no
Arguments: rec-calls-with-tests — Recursive calls of old.
Guard (pseudo-tests-and-call-listp rec-calls-with-tests).; old$ — Guard (symbolp old$).; y1...ym — Guard (symbol-listp y1...ym).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

This is used to check if a recursive old has the case 2 form described in the reference documentation.

Definitions and Theorems

Function: parteval-unchanging-static-in-rec-calls-p

(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: booleanp-of-parteval-unchanging-static-in-rec-calls-p

(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)