 The proof is based on the observation that we can build PCF terms of type \((\texttt{bool}\to \texttt{bool}\to \texttt{bool}) \to \texttt{num}\) that recognize the parallel-or function. Specifically, consider the “test” terms \(T_i\) defined as follows, where \(i = {0},1\):