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