Definition:Recursively Defined Mapping/Peano Structure

Definition

Let $\struct {P, 0, s}$ be a Peano structure.

Let $T$ be a set.

Let $g: T \to T$ be a mapping.

Let $f: P \to T$ be the mapping defined as:

$\forall x \in P: \map f x = \begin{cases}

 a & : x = 0 \\
 \map g {\map f n} & : x = \map s n

\end{cases}$

where $a \in T$.

Then $f$ is said to be recursively defined on $P$.