Proof that variable renaming preserves the execution behavior.

We start by extending the variable renaming relation from the abstract syntax to the dynamic semantic entities, namely function environments and computation states (and their constituents). For these, we define the relation as a predicate, instead of a function that may return errors, as we never need to return anything if the relation holds (while, for certain abstract syntax entities, we need to return additional information, e.g. the extended renaming.

Then we prove theorems relating variable renamings to the various dynamic semantic operations. Examples of these operations are writing variables, finding functions in environments, and so on.

Next, we show some properties of computation states and variable renamings, which do not involve dynamic semantic operations.

Then we prove theorems saying that executing a list of statements yields a computation state with a superset of the starting variables, and that executing loop iterations yields a computation state with the same variables as the starting state. These theorems are independent from variable renaming, and could be moved to a more central place, possibly complemented by similar properties for executing other kinds of abstract syntax entities.

Then we prove some theorems about limit errors. In particular, we prove that several dynamic semantic operations never return limit errors. These theorems are actually independent from variable renaming, and could be moved to a more central place.

Before proving the main theorems,
we prove two preliminary ones having to do with
the use of `restrict-vars` in execution,
when dealing with parallel executions related by variable renaming.

Finally we prove theorems about the execution functions and variable renaming. We do that by induction, using a custom induction schema.

- Restrict-vars-when-renamevar
- Theorems about restricting variables and variable renaming.
- Function-environments-when-renaming-variables
- Theorems about function environments and variable renaming.
- Exec-when-renamevar
- Main theorems of the proof that variable renaming preserves the execution behavior.
- Exec-when-renamevar-restrict-vars-lemmas
- Theorems about restricting variables in parallel executions related by variable renaming.
- Lstate-match-renamevarp
- Value matching part of the variable renaming relation over local states.
- Soutcome-result-renamevarp
- Variable renaming relation over statement outcome results.
- Lstate-renamevarp
- Variable renaming relation over local states.
- Reserr-limitp-theorems
- Theorems about
`reserr-limitp`. - Eoutcome-result-renamevarp
- Variable renaming relation over expression outcome results.
- Eoutcome-renamevarp
- Variable renaming relation over expression outcomes.
- Soutcome-renamevarp
- Variable renaming relation over statement outcomes.
- Cstate-renamevarp-with-larger-renaming
- Theorems about computation states and variable renamings, not involving dynamic semantic operations.
- Cstate-renamevarp
- Variable renaming relation over computation states.
- Funinfo-renamevarp
- Variable renaming relation over function information.
- Funscope-renamevarp
- Variable renaming relation over function scopes.
- Funenv-renamevarp
- Variable renaming relation over function environments.
- Path/paths-renamevar-theorems
- Theorems about variable renaming for paths.
- Init-local-when-renamevar
- Theorems about local state initialization and variable renaming.
- Write-var/vars-value/values-when-renamevar
- Theorems about writing variables and variable renaming.
- Add-var/vars-value/values-when-renamevar
- Theorems about adding variables and variable renamings.
- Read-var/vars-value/values-when-renamevar
- Theorems about reading variables and variable renaming.
- Vars-of-cstate-after-exec
- Theorems about the variables in a computation state after execution of certain kinds of constructs.