Generate a local theorem saying that a call of
(isodata-gen-old-to-list-of-mv-nth old$ old-fn-unnorm-name m names-to-avoid wrld) → (mv old-to-list-of-mv-nth-name old-to-list-of-mv-nth-event updated-names-to-avoid)
This is similar to isodata-gen-new-to-list-of-mv-nth.
Function:
(defun isodata-gen-old-to-list-of-mv-nth (old$ old-fn-unnorm-name m names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (symbolp old-fn-unnorm-name) (natp m) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-old-to-list-of-mv-nth)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'old-to-list-of-mv-nth nil names-to-avoid wrld)) (x1...xn (formals old$ wrld)) (old-call (cons old$ x1...xn)) (mv-nth-terms (loop$ for i from 0 to (1- m) collect (cons 'mv-nth (cons i (cons old-call 'nil))))) (formula (cons 'equal (cons old-call (cons (cons 'list mv-nth-terms) 'nil)))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old$ (cons old-fn-unnorm-name '(mv-nth))) 'nil)) 'nil))) 'nil)) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :enable nil))) (mv name event names-to-avoid))))