Theorems about local state initialization and variable renaming.
Starting with no variables, if old and new local states are initialized with corresponding variables, and with identical values for each pair of corresponding input variables, the resulting computation states are related by variable renaming. This theorem serves to establish the relation between computation states at the beginning of function execution.
Theorem:
(defthm init-local-when-renamevar (b* ((ren0 (add-vars-to-var-renaming old-in-vars new-in-vars (renaming nil))) (ren (add-vars-to-var-renaming old-out-vars new-out-vars ren0)) (old-cstate1 (init-local old-in-vars vals old-out-vars old-cstate)) (new-cstate1 (init-local new-in-vars vals new-out-vars new-cstate))) (implies (and (not (reserrp ren0)) (not (reserrp ren)) (not (reserrp old-cstate1)) (not (reserrp new-cstate1)) (identifier-listp old-in-vars) (identifier-listp new-in-vars) (identifier-listp old-out-vars) (identifier-listp new-out-vars)) (cstate-renamevarp old-cstate1 new-cstate1 ren))))