Generate the concatenation of
all the
(expdata-gen-all-back-of-forth-instances-to-mv-nth rec-calls res-surjmaps wrld) → lemma-instances
Function:
(defun expdata-gen-all-back-of-forth-instances-to-mv-nth (rec-calls res-surjmaps wrld) (declare (xargs :guard (and (pseudo-tests-and-call-listp rec-calls) (expdata-pos-surjmap-alistp res-surjmaps) (plist-worldp wrld)))) (let ((__function__ 'expdata-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)) (instances (expdata-gen-back-of-forth-instances-to-mv-nth updates res-surjmaps wrld)) (more-instances (expdata-gen-all-back-of-forth-instances-to-mv-nth (cdr rec-calls) res-surjmaps wrld))) (append instances more-instances))))
Theorem:
(defthm true-list-listp-of-expdata-gen-all-back-of-forth-instances-to-mv-nth (b* ((lemma-instances (expdata-gen-all-back-of-forth-instances-to-mv-nth rec-calls res-surjmaps wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)