 Definition 2.11 (Observational preorder and equivalence) Given PCF terms \(e\) and \(e'\) of the same type \(\sigma\), we write \(e \precsim_{\textrm{obs}} e'\) (read \(e\) is observationally less defined than \(e'\)) if, for every program context \(C\blbr\) with a hole of type \(\sigma\) and any value \(v\),   \[C[e] \opDownarrow v \ \text{ implies that } \ C[e'] \opDownarrow v.\]   We say that \(e\) and \(e'\) are observationally equivalent, and write \(e \simeq_{\textrm{obs}} e'\), if \(e \precsim_{\textrm{obs}} e'\) and \(e' \precsim_{\textrm{obs}} e\).