 In other words, to prove that ∀xα(x) one proves that α(0) is the case, and that α(succ(n)) follows from the assumption that α(n). The implementation of induction in a reasoning system presents very challenging search control problems. The most important of these is the ability to determine the particular way in which induction will be applied during the proof, that is, finding the appropriate induction schema. Related issues include selecting the proper variable of induction, and recognizing all the possible cases for the base and the inductive steps.