Theorems about adding variables and variable renamings.
Adding corresponding variables with the same value to related computation states yields related computation states.
Theorem:
(defthm add-var-value-when-renamevar (implies (and (cstate-renamevarp old-cstate new-cstate ren) (identifierp old-var) (identifierp new-var)) (b* ((ren1 (add-var-to-var-renaming old-var new-var ren)) (old-cstate1 (add-var-value old-var val old-cstate)) (new-cstate1 (add-var-value new-var val new-cstate))) (implies (and (not (reserrp ren1)) (not (reserrp old-cstate1)) (not (reserrp new-cstate1))) (cstate-renamevarp old-cstate1 new-cstate1 ren1)))))
Theorem:
(defthm add-vars-values-when-renamevar (implies (and (cstate-renamevarp old-cstate new-cstate ren) (identifier-listp old-vars) (identifier-listp new-vars)) (b* ((ren1 (add-vars-to-var-renaming old-vars new-vars ren)) (old-cstate1 (add-vars-values old-vars vals old-cstate)) (new-cstate1 (add-vars-values new-vars vals new-cstate))) (implies (and (not (reserrp ren1)) (not (reserrp old-cstate1)) (not (reserrp new-cstate1))) (cstate-renamevarp old-cstate1 new-cstate1 ren1)))))