Generate
(expdata-gen-forth-image-instances-to-terms-back terms old$ arg-surjmaps wrld) → lemma-instances
Function:
(defun expdata-gen-forth-image-instances-to-terms-back-aux (terms arg-surjmaps x1...xn back-of-x1...xn wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (expdata-symbol-surjmap-alistp arg-surjmaps) (symbol-listp x1...xn) (pseudo-term-listp back-of-x1...xn) (plist-worldp wrld)))) (declare (xargs :guard (= (len terms) (len arg-surjmaps)))) (let ((__function__ 'expdata-gen-forth-image-instances-to-terms-back-aux)) (declare (ignorable __function__)) (b* (((when (endp terms)) nil) (term (car terms)) (surjmap (cdar arg-surjmaps)) (forth-image (expdata-surjmap->forth-image surjmap)) (var (expdata-formal-of-forth surjmap wrld)) (term-with-back (subcor-var x1...xn back-of-x1...xn term)) (instance (list :instance forth-image :extra-bindings-ok (list var term-with-back))) (instances (expdata-gen-forth-image-instances-to-terms-back-aux (cdr terms) (cdr arg-surjmaps) x1...xn back-of-x1...xn wrld))) (cons instance instances))))
Theorem:
(defthm true-list-listp-of-expdata-gen-forth-image-instances-to-terms-back-aux (b* ((lemma-instances (expdata-gen-forth-image-instances-to-terms-back-aux terms arg-surjmaps x1...xn back-of-x1...xn wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)
Function:
(defun expdata-gen-forth-image-instances-to-terms-back (terms old$ arg-surjmaps wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (plist-worldp wrld)))) (declare (xargs :guard (= (len terms) (len arg-surjmaps)))) (let ((__function__ 'expdata-gen-forth-image-instances-to-terms-back)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (back-of-x1...xn (expdata-gen-back-of-terms x1...xn arg-surjmaps))) (expdata-gen-forth-image-instances-to-terms-back-aux terms arg-surjmaps x1...xn back-of-x1...xn wrld))))
Theorem:
(defthm true-list-listp-of-expdata-gen-forth-image-instances-to-terms-back (b* ((lemma-instances (expdata-gen-forth-image-instances-to-terms-back terms old$ arg-surjmaps wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)