Properties about execution without function calls.
We prove that, when executing code without function calls, the function environment has no effect: execution gives the same results with different function environments.