Generate a local theorem saying that a call of
(isodata-gen-new-to-list-of-mv-nth old$ new$ new-fn-unnorm-name m names-to-avoid wrld) → (mv new-to-list-of-mv-nth-name new-to-list-of-mv-nth-event updated-names-to-avoid)
This is generated only if
This could be proved more generally:
if
Function:
(defun isodata-gen-new-to-list-of-mv-nth (old$ new$ new-fn-unnorm-name m names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (symbolp new$) (symbolp new-fn-unnorm-name) (natp m) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-to-list-of-mv-nth)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'new-to-list-of-mv-nth nil names-to-avoid wrld)) (x1...xn (formals old$ wrld)) (new-call (cons new$ x1...xn)) (mv-nth-terms (loop$ for i from 0 to (1- m) collect (cons 'mv-nth (cons i (cons new-call 'nil))))) (formula (cons 'equal (cons new-call (cons (cons 'list mv-nth-terms) 'nil)))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons new$ (cons new-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))))