		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-test-of-updates-term

Generate the instantiation of the exit test of fn with calls to the iterated argument update functions.

Signature
(defarbrec-gen-test-of-updates-term x1...xn$ test update-names$ iterations) → terms
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).; test — Guard (pseudo-termp test).; update-names$ — Guard (symbol-listp update-names$).; iterations — Guard (pseudo-termp iterations).
Returns: terms — A pseudo-termp.

This is the term test<(update*-x1 iterations x1 ... xn), ..., (update*-xn iterations x1 ... xn)>, where the iterations term is passed as argument to this function.

Definitions and Theorems

Function: defarbrec-gen-test-of-updates-term

(defun defarbrec-gen-test-of-updates-term
       (x1...xn$ test update-names$ iterations)
  (declare (xargs :guard (and (symbol-listp x1...xn$)
                              (pseudo-termp test)
                              (symbol-listp update-names$)
                              (pseudo-termp iterations))))
  (let ((__function__ 'defarbrec-gen-test-of-updates-term))
    (declare (ignorable __function__))
    (subcor-var x1...xn$
                (apply-terms-same-args update-names$
                                       (cons iterations x1...xn$))
                test)))