Generate the conjunction of the implications,
in the
(isodata-gen-oldp-of-rec-call-args-under-contexts rec-calls arg-isomaps) → oldp-of-rec-call-args-under-contexts
This function generates the subformula
(and (implies context1<x1,...,xn> (and (oldp update1-x1<x1,...,xn>) ... (oldp update1-xp<x1,...,xn>))) ... (implies contextr<x1,...,xn> (and (oldp updater-x1<x1,...,xn>) ... (oldp updater-xp<x1,...,xn>))))
of the
Function:
(defun isodata-gen-oldp-of-rec-call-args-under-contexts (rec-calls arg-isomaps) (declare (xargs :guard (and (pseudo-tests-and-call-listp rec-calls) (isodata-symbol-isomap-alistp arg-isomaps)))) (let ((__function__ 'isodata-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 (isodata-gen-oldp-of-terms (fargs rec-call) arg-isomaps))) (isodata-gen-oldp-of-rec-call-args-under-contexts (cdr rec-calls) arg-isomaps)))))