Primitive recursive functions and mutual recursion

Let $g$ and $g'$ be primitive recursive, of arity 2, and let $a,a'\in\mathbb{N}$. Define $f$ and $f'$ by the following formulae:

$f(0)=a$

$f'(0)=a'$

$f(n+1)=g(n,f'(n))$

$f'(n+1)=g'(n,f(n))$.

How would you show these ($f$ and $f'$) are primitive recursive?

As soon as you know one is, the other one follows immediately, so I suppose you have to somehow prove it about both at once.

Replacing the formula for $f$ in the one for $f'$, it's easy to get that $$f'(n+1)=g'\bigg(n,\ g\big(n-1,\ f'(n-1)\big)\bigg),$$ which shows how $f'$ can be realized as composition of p.r. functions ($g$ and $g'$) and $f'$ itself, as soon as you have TWO initial values for $f'$ (which isn't hard). So intuitively that shows why it should be p.r. Symmetrically for $f$. However, I don't know how to turn this into a formal proof, or even if this is the right approach.

It's easy to see that the last formula above looks sort of like the basic formula for primitive recursion (as in http://en.wikipedia.org/wiki/Primitive_recursive#Role_of_the_projection_functions ), but I don't know if that helps.

Finally, I have looked at $f(i)$ for $i=0..4$ (and hence for $f'(i)$, due to the symmetry), and the pattern seems to be $$f(i)=g\bigg(i-1,g'\Big(i-2,g\big(i-3,g'(\dots,\star)\big)\Big)\bigg),$$ where $\star\in\{a,a'\}.$ I suppose this is sort of the proof ($f$ can be realized as a series of compositions of $g$ and $g'$, both of which are p.r.), but I don't know how to make it rigorous, and somehow it doesn't seem so satisfying to actually write out $f$ and $f'$ as iterative recursions of $g$ and $g'$, so another approach would be appreciated.

-

Mutual recursion is usually handled by collecting the different "streams" of output together. For example, let's assume we have constructed a primitive recursive pairing/unpairing function. Then I can define a function $F$ by primitive recursion: $$F(0) = \mathsf{pair}(a, a')$$ $$F(n+1) = \mathsf{pair}(g(n, \mathsf{right}(F(n))), g'(n, \mathsf{left}(F(n)))$$ The functions you want are then obtained by composition: $$f(n) = \mathsf{left}(F(n))$$ $$f'(n) = \mathsf{right}(F(n))$$
One way to do this is to define a single function $h$ such that $h(2n) = f(n)$ and $h(2n+1) = f'(n)$. You can do this without first defining $f$ or $f'$ because primitive recursive functions are closed under effective definitions by cases. Once you have defined $h$, you can use it to define $f$ and $f'$ by composition.