Terminology 2: A recursive specification (or recursive definition if we are able to be precise enough) of some notion is given by the following:
(a) Rules specifying certain instances of the notion, called the base cases, without invoking other instances of the notion to do so.
(b) Recursion rules, each invoking hypothetical instances, called inputs, of the notion in order to specify a new instance of the notion, the output.

Given a recursively specified notion \mathfrak{R} , we may show by structural induction that some assertion is evident for every instance of \mathfrak{R} as follows:
(i) Showing that the assertion is evident for each base case of \mathfrak{X} .
(ii) For each recursion rule, showing under the induction hypothesis that the assertion is evident for arbitrary and sufficient inputs, so is it for the corresponding output. We call this the inductive step of the proof.