| < Free Open Study > |
|
If in the augmented semantics and t contains wrong as a subterm, then g is stuck in the original semantics.
Proof: Straightforward induction on (augmented) evaluation derivations.
Combining this with Lemma A.3 yields the "if" (Þ) half of Proposition A.2, and we are finished.
We prove the two directions of the "iff" separately, in Propositions A.7 and A.9. In each case, we begin with a technical lemma establishing some useful properties of multi-(small-)step evaluation.
| < Free Open Study > |
|