Editing Primitive recursive function (section)

===Addition===

A definition of the 2-ary function <math>Add</math>, to compute the sum of its arguments, can be obtained using the primitive recursion operator <math>\rho</math>. To this end, the well-known equations 
:<math>\begin{array}{rcll}
0+y & = & y & \text{ and} \\
S(x)+y & = & S(x+y) & . \\
\end{array}</math>
are "rephrased in primitive recursive function terminology": In the definition of <math>\rho(g,h)</math>, the first equation suggests to choose <math>g = P_1^1</math> to obtain <math>Add(0,y) = g(y) = y</math>; the second equation suggests to choose <math>h = S \circ P_2^3</math> to obtain <math>Add(S(x),y) = h(x,Add(x,y),y) = (S \circ P_2^3)(x,Add(x,y),y) = S(Add(x,y))</math>. Therefore, the addition function can be defined as <math>Add = \rho(P_1^1,S \circ P_2^3)</math>. As a computation example,
:<math>\begin{array}{lll}
& Add(1,7) \\
= & \rho(P_1^1,S \circ P_2^3) \; (S(0),7) & \text{ by Def. } Add, S \\
= & (S \circ P_2^3)(0,Add(0,7),7) & \text{ by case } \rho(g,h) \; (S(...),...) \\
= & S(Add(0,7)) & \text{ by Def. } \circ, P_2^3 \\
= & S( \; \rho(P_1^1,S \circ P_2^3) \; (0,7) \; ) & \text{ by Def. } Add \\
= & S(P_1^1(7)) & \text{ by case } \rho(g,h) \; (0,...) \\
= & S(7) & \text{ by Def. } P_1^1 \\
= & 8 & \text{ by Def. } S . \\ 
\end{array}</math>