 Definition 2.11 (Denotational preorder and equivalence). Given PCF terms \(e\) and \(e'\) of the same type \(\sigma\) relative to a basis \(B\), we write \(e \precsim_{\textrm{den}} e'\) if \({\lll e\rll \rho} \sqsubseteq {{\lll e'\rll} \rho}\) for all environments \(\rho\) respecting \(B\). We write \(e \simeq_{\textrm{den}} e'\) if \(e \precsim_{\textrm{den}} e'\) and \(e' \precsim_{\textrm{den}} e\) .