Generate
(isodata-gen-forth-image-instances-to-x1...xn arg-isomaps wrld) → lemma-instances
Function:
(defun isodata-gen-forth-image-instances-to-x1...xn (arg-isomaps wrld) (declare (xargs :guard (and (isodata-symbol-isomap-alistp arg-isomaps) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-forth-image-instances-to-x1...xn)) (declare (ignorable __function__)) (b* (((when (endp arg-isomaps)) nil) (arg (caar arg-isomaps)) (isomap (cdar arg-isomaps)) (forth-image (isodata-isomap->forth-image isomap)) (forth-arg (isodata-formal-of-unary (isodata-isomap->forth isomap) wrld)) (instance (list :instance forth-image :extra-bindings-ok (list forth-arg arg))) (instances (isodata-gen-forth-image-instances-to-x1...xn (cdr arg-isomaps) wrld))) (cons instance instances))))
Theorem:
(defthm true-list-listp-of-isodata-gen-forth-image-instances-to-x1...xn (b* ((lemma-instances (isodata-gen-forth-image-instances-to-x1...xn arg-isomaps wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)