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. The SECD Machine Recall that the objects manipulated by the original SECD machine differ from those manipulated by the TR-SECD machine only in the fact that code may follow the call symbol.