		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Write-var/vars-value/values-when-renamevar

Theorems about writing variables and variable renaming.

Writing the same values in corresponding variables of related computation states yields related computation states.

Definitions and Theorems

Theorem: write-var-value-when-renamevar

(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: write-vars-values-when-renamevar

(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)))))