Theorems about reading variables and variable renaming.
Reading corresponding variables from related computation states yields the same value, if both readings suceed.
Theorem:
(defthm read-var-value-when-renamevar (implies (and (cstate-renamevarp old-cstate new-cstate ren) (not (reserrp (var-renamevar old-var new-var ren)))) (b* ((old-val (read-var-value old-var old-cstate)) (new-val (read-var-value new-var new-cstate))) (implies (and (not (reserrp old-val)) (not (reserrp new-val))) (equal old-val new-val)))))
Theorem:
(defthm read-vars-values-when-renamevar (implies (and (cstate-renamevarp old-cstate new-cstate ren) (not (reserrp (var-list-renamevar old-vars new-vars ren)))) (b* ((old-vals (read-vars-values old-vars old-cstate)) (new-vals (read-vars-values new-vars new-cstate))) (implies (and (not (reserrp old-vals)) (not (reserrp new-vals))) (equal old-vals new-vals)))))