Every property of the underlying program is a property of the
transformed program.
- Augmentation:
- If holds for of underlying program,
|| also holds because name no variables assigned in
. Since furthermore initial condition of underlying program is preserved,
all proofs are preserved.
- Restricted Union:
- Added statements do not write into underlying variables. From locality
corollary and the fact that underlying program does not mention superposed
variables in its proof, all proofs are preserved.