Such inductive definitions are possible due to the definition of natural numbers as a construction (i.e. inductive data type). Note that some of the "+" symbols appearing in this definition are part of the notation of the successor constructor.