 Definition 2.12 (Inequational full abstraction). A continuous model \({\langle {\{ {{{D}^{\sigma}}} \mid \sigma \in \texttt{Types}}\},{\lll \cdot\rll \cdot} \rangle}\) of PCF is inequationally fully abstract if, for closed terms \(e,e'\), \(e \precsim_{\textrm{obs}} e'\) implies \({\lll e\rll } \sqsubseteq {\lll e'\rll }\).