Types and Programming Languages

A.2 Proposition

For all original terms g, (, where g′ is stuck) iff ( wrong).

To prove this, we proceed in several steps. First, we remark that the new transitions we have added do not invalidate Theorem 3.5.14.