		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-oldp-of-rec-call-args-under-contexts

Generate the conjunction of the implications, in the :oldp-of-rec-call-args applicability condition, that correspond to the recursive calls of old.

Signature
(expdata-gen-oldp-of-rec-call-args-under-contexts rec-calls arg-surjmaps) → oldp-of-rec-call-args-under-contexts
Arguments: rec-calls — Guard (pseudo-tests-and-call-listp rec-calls).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).
Returns: oldp-of-rec-call-args-under-contexts — A pseudo-termp.

This function generates the subformula

(and (implies context1<x1,...,xn>
              (and (oldp update1-y1<x1,...,xn>)
                   ...
                   (oldp update1-yp<x1,...,xn>)))
     ...
     (implies contextm<x1,...,xn>
              (and (oldp updatem-y1<x1,...,xn>)
                   ...
                   (oldp updatem-yp<x1,...,xn>))))

of the :oldp-of-rec-call-args applicability condition.

Definitions and Theorems

Function: expdata-gen-oldp-of-rec-call-args-under-contexts

(defun expdata-gen-oldp-of-rec-call-args-under-contexts
       (rec-calls arg-surjmaps)
 (declare
  (xargs :guard (and (pseudo-tests-and-call-listp rec-calls)
                     (expdata-symbol-surjmap-alistp arg-surjmaps))))
 (let
  ((__function__ 'expdata-gen-oldp-of-rec-call-args-under-contexts))
  (declare (ignorable __function__))
  (b* (((when (endp rec-calls)) *t*)
       (tests-and-call (car rec-calls))
       (tests (access tests-and-call tests-and-call :tests))
       (rec-call (access tests-and-call tests-and-call :call))
       (context (conjoin tests)))
   (conjoin2
     (implicate context
                (conjoin (expdata-gen-oldp-of-terms (fargs rec-call)
                                                    arg-surjmaps)))
     (expdata-gen-oldp-of-rec-call-args-under-contexts
          (cdr rec-calls)
          arg-surjmaps)))))