The function run is undefined if it reaches an error state, or fails to reach an accepting state for any other reason. It can easily be shown that the function real produces a value when applied to a closure. The correctness of the TR-SECD machine is expressed in the following theorem. This remainder of this section contains the important lemmas used to prove Theorem 1. A value environment is defined inductively.
E is a value environment and fv M .
V is closed in E . To control the complexity of the proofs, the correctness proof is factored into a stage which verifies the correctness of environments and substitution, and a later stage which verifies the correctness of the control information. The following lemma is aimed at the first stage. Assume expression M is closed in environment E . Note that the introduction of functions reduce and runenv allow a statement of adequacy using only universally quantified variables.