Equivalence of Reduction and Natural Semantics

Note: We use the leftmost-outermost evaluation strategy in this proof.

Proof: We proceed by induction on the height of the derivation tree for . Consider only the case when is an application, i.e. , or else it follows trivially. Then for some By induction, Then the derivation is leftmost-outermost. Now , so by induction, We have There is a sequence . The proof that is by induction on The base case is trivial. So assume must be an application, namely , for some and . At some point, the outer redex must be reduced, so suppose this happens at the k-th step. In the first k steps we have the reduction of to and since , follows by induction. Then we have As , by induction, So follows by definition of .