 Due to the simplicity of the example, the substitution of \(t\) for \(x\) in \(Bx\) and in \(Ax\) seems to be easy to understand and to perform. However, a definition of substitution for FOL (and in general, for an abstract syntax, that is, for a language with a variable binding operator) has to guarantee that no free occurrence of a variable in the substituted expression becomes bound in the resulting expression.