Theorems about computation states and variable renamings, not involving dynamic semantic operations.
If two computation states are related by variable renaming, they are also related by a larger variable renaming. This is proved by first proving a similar theorem for local states.
The motivation for this theorem is that, when a list of statements (in a block) is executed, execution may not reach the end of the statements. However, statically, when we consider that list of statements, we extend the variable renaming according to the whole list of statements. Since we want to show that execution preserves the variable renaming relation between computation states, we need to able to relate the final states with the final variable renamings, which may be larger due to execution ending before the end. So this theorem enables us to bridge this gap.
Theorem:
(defthm lstate-match-renamevarp-of-larger (implies (and (lstatep old-lstate) (lstatep new-lstate) (lstate-renamevarp old-lstate new-lstate ren) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (lstate-match-renamevarp old-lstate new-lstate ren1)))
Theorem:
(defthm lstate-renamevarp-of-larger (implies (and (lstatep old-lstate) (lstatep new-lstate) (lstate-renamevarp old-lstate new-lstate ren) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (lstate-renamevarp old-lstate new-lstate ren1)))
Theorem:
(defthm cstate-renamevarp-of-larger (implies (and (cstate-renamevarp old-cstate new-cstate ren) (subsetp-equal (renaming->list ren) (renaming->list ren1))) (cstate-renamevarp old-cstate new-cstate ren1)))