In Types and Programming Languages by Pierce, when talking about untyped arithmetic expressions in Chapter 3, there are two theorems:
$-→$ is single-step evaluation relation:
3.5.4 Theorem [Determinacy of one-step evaluation]: If $t -→ t'$ and $t -→ t''$ , then $t' = t''$ .
$-→ ∗$ is multi-step evaluation relation:
3.5.11 Theorem [Uniqueness of normal forms]: If $t -→ ∗ u$ and $t -→ ∗ u'$ , where $u$ and $u'$ are both normal forms, then $u = u'$.
Do the two theorems also apply to all (or most) the other languages/systems in the book, or only to the untyped arithmetic expressions?
From my limited experiences in a few programming languages, it seems that an expression is always evaluated in exactly one deterministic process, so I wonder if both theorems apply to all the languages.