Decision procedures are widely used in automated reasoning tools in order to reason about data structures. Their scope is typically limited, though, and many conjectures occurring in practical applications fall outside the theory handled by a decision procedure. Typically, reasoning about functions that are defined on those data structures is needed. For this, inductive reasoning has to be employed.

In this work, families of function definitions and conjectures are identified for which inductive validity can be decided using implicit induction methods and decision procedures for an underlying decidable theory. The results significantly extend the results obtained in (Kapur & Subramaniam, 2000), which were obtained using explicit induction schemes. Firstly, we allow performing induction on nonlinear terms, which enables us to decide conjectures like gcd(x, x) = x. Secondly, we allow for mutually recursive function definitions. Thirdly, we allow general terms from the decidable theory on inductive positions, which is needed to decide conjectures such as gcd(2x, 2) = 2. These contributions are crucial for successfully integrating inductive reasoning into decision procedures.