Generate the concatenation of
all the
(isodata-gen-all-back-of-forth-instances-to-mv-nth old$ rec-calls arg-isomaps res-isomaps wrld) → lemma-instances
Function:
(defun isodata-gen-all-back-of-forth-instances-to-mv-nth (old$ rec-calls arg-isomaps res-isomaps wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-tests-and-call-listp rec-calls) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-all-back-of-forth-instances-to-mv-nth)) (declare (ignorable __function__)) (b* (((when (endp rec-calls)) nil) (tests-and-call (car rec-calls)) (rec-call (access tests-and-call tests-and-call :call)) (updates (fargs rec-call)) (x1...xn (formals old$ wrld)) (back-of-x1...xn (isodata-gen-back-of-terms x1...xn arg-isomaps)) (updates-back (subcor-var-lst x1...xn back-of-x1...xn updates)) (old-of-updates-back (fcons-term old$ updates-back)) (instances (isodata-gen-back-of-forth-instances-to-mv-nth old-of-updates-back res-isomaps wrld)) (more-instances (isodata-gen-all-back-of-forth-instances-to-mv-nth old$ (cdr rec-calls) arg-isomaps res-isomaps wrld))) (append instances more-instances))))
Theorem:
(defthm true-list-listp-of-isodata-gen-all-back-of-forth-instances-to-mv-nth (b* ((lemma-instances (isodata-gen-all-back-of-forth-instances-to-mv-nth old$ rec-calls arg-isomaps res-isomaps wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)