Theorems about writing variables and variable renaming.
Writing the same values in corresponding variables of related computation states yields related computation states.
Theorem:
(defthm write-var-value-when-renamevar (implies (and (cstate-renamevarp old-cstate new-cstate ren) (not (reserrp (var-renamevar old-var new-var ren))) (identifierp old-var) (identifierp new-var)) (b* ((old-cstate1 (write-var-value old-var val old-cstate)) (new-cstate1 (write-var-value new-var val new-cstate))) (implies (and (not (reserrp old-cstate1)) (not (reserrp new-cstate1))) (cstate-renamevarp old-cstate1 new-cstate1 ren)))))
Theorem:
(defthm write-vars-values-when-renamevar (implies (and (cstate-renamevarp old-cstate new-cstate ren) (not (reserrp (var-list-renamevar old-vars new-vars ren))) (identifier-listp old-vars) (identifier-listp new-vars)) (b* ((old-cstate1 (write-vars-values old-vars vals old-cstate)) (new-cstate1 (write-vars-values new-vars vals new-cstate))) (implies (and (not (reserrp old-cstate1)) (not (reserrp new-cstate1))) (cstate-renamevarp old-cstate1 new-cstate1 ren)))))