 Definition 1.2 (Observational equivalence) Given any two program phrases \(e,e'\), they are observational equivalent, written \(e \simeq_{\mathcal{O}}e'\), when, for all program contexts \(C\blbr\) and all program values \(v\):   \[C[e] \opDownarrow v\  \text{ if and only if }\  C[e'] \opDownarrow v.\]  