 Clause (1) of the definition simply says that if we are to substitute \(M\) for \(x\) and we are dealing simply with \(x\), then the result is just \(M\). Clause (2) says that nothing happens when we are dealing (only) with a variable different from \(x\) but we are to substitute something for \(x\). Clause (3) tells us that substitution unconditionally distributes over applications. Clauses (4) and (5) concern abstraction terms and parallel clauses (1) and (2) (or rather, clauses (2) and (1), in opposite order): If the bound variable \(z\) of the abstraction term \(\lambda z[A]\) is identical to the variable \(x\) for which we are to do a substitution, then we do not perform any substitution (that is, substitution “stops”). This coheres with the intention that \(M[x := N]\) is supposed to denote the substitution of \(N\) for the free occurrences of \(x\) in \(M\). If \(M\) is an abstraction term \(\lambda x[A]\) whose bound variable is \(x\), then \(x\) does not occurr freely in \(M\), so there is nothing to do. This explains clause 4. Clause (5), finally, says that if the bound variable of an abstraction term differs from \(x\), then at least \(x\) has the “chance ” to occur freely in the abstraction term, and substitution continues into the body of the abstraction term.