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