 Definition The syntactic functions \(\mathbf{FV}\) and \(\mathbf{BV}\) (for ‘free variable’ and ‘bound variable’, respectively) are defined on the set of \(\lambda\)-terms by structural induction thus: