Generate the theorem that says that the new function maps values in the new representation to values in the old representation.
(expdata-gen-newp-of-new-thm old$ arg-surjmaps res-surjmaps new$ new-to-old$ newp-of-new$ newp-of-new-enable$ appcond-thm-names wrld) → (mv newp-of-new-local-event newp-of-new-exported-event)
Function:
(defun expdata-gen-newp-of-new-thm (old$ arg-surjmaps res-surjmaps new$ new-to-old$ newp-of-new$ newp-of-new-enable$ appcond-thm-names wrld) (declare (xargs :guard (and (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (expdata-pos-surjmap-alistp res-surjmaps) (symbolp new$) (symbolp new-to-old$) (symbolp newp-of-new$) (booleanp newp-of-new-enable$) (symbol-symbol-alistp appcond-thm-names) (plist-worldp wrld)))) (declare (xargs :guard (consp res-surjmaps))) (let ((__function__ 'expdata-gen-newp-of-new-thm)) (declare (ignorable __function__)) (b* ((formula (expdata-gen-newp-of-new-thm-formula old$ arg-surjmaps res-surjmaps new$ wrld)) (formula (untranslate formula t wrld)) (hints (expdata-gen-newp-of-new-thm-hints appcond-thm-names old$ arg-surjmaps res-surjmaps new-to-old$ wrld))) (evmac-generate-defthm newp-of-new$ :formula formula :hints hints :enable newp-of-new-enable$))))