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