indnat http://www.openmath.org/cd/indnat.ocd 2000-09-01 experimental 1 1 relation1 Inductive definition of natural numbers Initial version: O.C (Jan. 2000) indNat Attribution tag to denote the type of inductively defined natural numbers. It is also denoted as setname1:N. zero The natural number 0, also constant base function for the inductive definition of the type of natural numbers succ Successor function on the natural number. Constructor for the inductively defined natural numbers. Takes argument a a natural number and returns a natural number. plus Addition of natural numbers defined recursively by using the successor. times Multiplication of natural numbers defined recursively by using the successor and plus.