		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-unchanging-static-in-rec-args-p

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

Signature
(parteval-unchanging-static-in-rec-args-p rec-args old$ yj...ym wrld) → yes/no
Arguments: rec-args — Arguments of a recursive call of old.
Guard (pseudo-term-listp rec-args).; old$ — Guard (symbolp old$).; yj...ym — Guard (symbol-listp yj...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-args-p

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

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