 Then, \({\mathcal{D}\lll T_{0}\rll}\ \texttt{por} = {0}\neq 1 = {\mathcal{D}\lll T_1 \rll }\ \texttt{por} \), where por is defined by table \((\ref{por})\), so \(T_{0} {\simeq_{\textrm{den}}}T_1\) does not hold. However, no program context in PCF can separate \(T_{0}\) and \(T_1\) because por is not definable. This can be shown by characterizing in a combinatorial way the relations of dependence induced by the evaluation process of a program among the evaluation processes of its (sub)terms, as Plotkin does in the Activity Lemma (Plotkin 1977: Lemma 4.2). As an alternative, it is possible to build a computationally adequate models of PCF whose functions enjoy a weak sequentiality property (that we discuss below, in  Section 2.5.1)  and where, therefore, the function por is ruled out: a complete formal proof along these lines is given in Gunter 1992 (sec. 6.1).