		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

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

Theorems about adding variables and variable renamings.

Adding corresponding variables with the same value to related computation states yields related computation states.

Definitions and Theorems

Theorem: add-var-value-when-renamevar

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

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