 Definition A \(\beta\)-reduction sequence from a \(\lambda\)-term \(A\) to a \(\lambda\)-term \(B\) is a finite sequence \(s_1 , \ldots s_n\) of \(\lambda\)-terms starting with \(A\), ending with \(B\), and whose adjacent terms \((s_k,s_{k+1})\) satisfy the property that \(s_k \rhd_{\beta ,1} s_{k+1}\).