Sometimes a sequence $(s_n)_{n \in \mathbf{N}}$, where $\mathbf{N}$ is the set of natural numbers, is defined as follows: (a) let $s_0 = ...$; (b) for $n \geq0$ assume that $s_0, s_1, s_2, \dots, s_n$ have already been defined; then define $s_{n+1}$ in terms of$s_0, s_1, s_2, \dots, s_n$ by .....
What is a precise statement of the mathematical theorem justifying that "complete recursion" (an analog of "complete" induction)? Where might one find it stated in the literature along with a proof?
I ask this because so often even the definition of the factorial function is wrongly based upon too weak a theorem. [Justifying the usual definition requires not "ordinary" recursion, but rather "primitive recursion" — start with a set $X$, an element $c \in X$, and a function $G : X \times \mathbf{N} \rightarrow X$; then the theorem on primitive recursion asserts the existence of a unique function $f : \mathbf{N} \rightarrow X$ such that $f(0) = c$ and, for each $n \in \mathbf{N}$, $f(n+1) = G(n, f(n))$.]
The issue is mainly being able to say what kind of function or relation replaces such $G$ when one is dealing with a "function" that has a variable number of arguments.
Here's an attempt at such a thorem. Is this valid? And is there some place specific in the literature where it appears?
Theorem. Let $X$ be a set, let $c \in X$, and let $G : \bigcup_{n=1}^{\infty} X^{n} \rightarrow X$ be a given map (where $X^{n}$ denotes the $n$-fold Cartesian product of $X$ with itself). Then there is a unique map $f : \mathbf{N} \rightarrow X$ such that $f(0) = c$ and, for each $n \in \mathbf{N}$, we have $f(n+1) = G(f(0), f(1), f(2), \dots, f(n))$.
I claim that complete recursion is not more powerful than ordinary recursion. To see this, I'll use ordinary recursion to prove the theorem about complete recursion.
So suppose $G:X^{<\omega}\rightarrow X$, for some set $X$, and $c\in X$ are given. We want to find a function $f\colon\mathbb N\rightarrow X$ such that for all $n\in\mathbb N$: $$ f(n+1)=G(f\upharpoonright n),$$ (where $f\upharpoonright n$ is the restriction of $f$ to a function with domain $n=\{0,1,\dots,n-1\}$ (and $0=\emptyset$)).
To do this, let $Y=X^{<\omega}$ and define $G':Y\rightarrow Y$ by $$G'(x_1,\dots,x_n)=(x_1,\dots,x_n)^\smallfrown G(x_1,\dots,x_n),$$ (where $^\smallfrown$ denotes concatenation of sequences). Now, define $f':\mathbb N\rightarrow Y$ by ordinary recursion so that $f'(0)=(c)$ (that is, a tuple of length $1$ with coordinate $c$) and for $n\in\mathbb N$: $$f'(n+1)=G'(f'(n)).$$
We now have to see how to get our desired $f$ from $f'$. I will prove by induction that if we define $f(n)$ to be the last coordinate of $f'(n)$, then $f$ is as desired, so $f(0)=c$ and $f(n+1)=G(f\upharpoonright n)$ for all $n\in\mathbb N$.
We show something stronger, namely that for all $n\in\mathbb N$ we have that $$f'(n)=f\upharpoonright n+1.$$ This is obvious for $n=0$. Assume it holds true for some $n$ and note that $$ f'(n+1)=G'(f'(n))=G'(f\upharpoonright n+1)=(f\upharpoonright n+1)^\smallfrown G(f\upharpoonright n+1)=f\upharpoonright n+2,$$ where the first equality follows from the definition of $f'$, the second by induction hypothesis, the third by definition of $G'$ and the last by definition of $f$. Thus, by induction, the above representation of $f'(n)$ is proved.
Now, it is easy to see that $f$ is as desired: $f(0)=c$ by definition and that $f(n+1)=G(f\upharpoonright n)$ for all $n\in\mathbb N$ can be seen from above equation.
EDIT: Sorry, I forgot to say anything about uniqueness. The proof for this is (I imagine) the same as for the ordinary recursion theorem. If you had two functions $f,g$ both satisfying the recursive definition, note that there'd be a least place $n$ where they differ. Now, $n\neq 0$ because $f(0)=c=g(0)$. Thus $n>0$ and $f\upharpoonright n=g\upharpoonright n$. But we then have $f(n)=G(f\upharpoonright n)=G(g\upharpoonright n)=g(n)$, contradicting the assumption that there were two such functions. (You can also prove by induction that $f\upharpoonright n=g\upharpoonright n$ for all $n\in\mathbb N$.)