A.3 Lemma

---

A.3 Lemma

The augmented evaluation relation is deterministic.

This means that whenever g can take a single step to g′ in the original semantics, it can also step to g′ in the augmented semantics, and furthermore that g′ is the only term g can step to in the new semantics.

Next, we show that a term that is (already) stuck in the original semantics will always evaluate to wrong in the augmented semantics.

---