Terminology 23: Given some recursively specified notion, we may argue using structural induction that some general observation is justified for each and every instance of the notion. Such an argument is carried out as follows:
(i) Show that the observation is justified for each of the base cases.
(ii) For each recursion rule, show under the induction hypothesis that the observation is justified for arbitrary and sufficient inputs, that is also is for the corresponding output. We refer to this the inductive step.