Generate
(expdata-gen-forth-image-instances-to-mv-nth term res-surjmaps wrld) → lemma-instances
Function:
(defun expdata-gen-forth-image-instances-to-mv-nth (term res-surjmaps wrld) (declare (xargs :guard (and (pseudo-termp term) (expdata-pos-surjmap-alistp res-surjmaps) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-forth-image-instances-to-mv-nth)) (declare (ignorable __function__)) (b* (((when (endp res-surjmaps)) nil) (j (caar res-surjmaps)) (surjmap (cdar res-surjmaps)) (forth-image (expdata-surjmap->forth-image surjmap)) (var (expdata-formal-of-forth surjmap wrld)) (mv-nth-of-term (fcons-term* 'mv-nth (1- j) term)) (instance (cons ':instance (cons forth-image (cons ':extra-bindings-ok (cons (cons var (cons mv-nth-of-term 'nil)) 'nil))))) (instances (expdata-gen-forth-image-instances-to-mv-nth term (cdr res-surjmaps) wrld))) (cons instance instances))))
Theorem:
(defthm true-list-listp-of-expdata-gen-forth-image-instances-to-mv-nth (b* ((lemma-instances (expdata-gen-forth-image-instances-to-mv-nth term res-surjmaps wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)