 Definition (one-step \(\beta\)-reduction \(\rhd_{\beta ,1})\) For \(\lambda\)-terms \(A\) and \(B\), we say that \(A\) \(\beta\)-reduces in one step to \(B\), written \(A \rhd_{\beta ,1} B\), just in case there exists an (occurrence of a) subterm \(C\) of \(A\), a variable \(x\), and \(\lambda\)-terms \(M\) and \(N\) such that \(C \equiv(\lambda x[M])N\) and \(B\) is \(A\) except that the occurrence of \(C\) in \(A\) is replaced by \(M[x := N]\).