Generate the conjunction of the implications,
in the
(expdata-gen-oldp-of-rec-call-args-under-contexts rec-calls arg-surjmaps) → oldp-of-rec-call-args-under-contexts
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
Function:
(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)))))