Generate lemma instances where
a variable is instantiated with
a call of the new function
on
(expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back lemma var rec-calls old$ arg-surjmaps new$ wrld) → lemma-instances
Function:
(defun expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back (lemma var rec-calls old$ arg-surjmaps new$ wrld) (declare (xargs :guard (and (symbolp lemma) (symbolp var) (pseudo-tests-and-call-listp rec-calls) (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (symbolp new$) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back)) (declare (ignorable __function__)) (b* (((when (endp rec-calls)) nil) (tests-and-call (car rec-calls)) (rec-call (access tests-and-call tests-and-call :call)) (rec-call-args (fargs rec-call)) (x1...xn (formals old$ wrld)) (back-of-x1...xn (expdata-gen-back-of-terms x1...xn arg-surjmaps)) (rec-call-args-back (subcor-var-lst x1...xn back-of-x1...xn rec-call-args)) (forth-of-rec-call-args-back (expdata-gen-forth-of-terms rec-call-args-back arg-surjmaps)) (new-call (fcons-term new$ forth-of-rec-call-args-back)) (instance (cons ':instance (cons lemma (cons ':extra-bindings-ok (cons (cons var (cons new-call 'nil)) 'nil))))) (instances (expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back lemma var (cdr rec-calls) old$ arg-surjmaps new$ wrld))) (cons instance instances))))
Theorem:
(defthm true-list-listp-of-expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back (b* ((lemma-instances (expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back lemma var rec-calls old$ arg-surjmaps new$ wrld))) (true-list-listp lemma-instances)) :rule-classes :rewrite)