 Kleene normal form theorem

For every partial computable function $f(\mathbf{x})$, there are total primitive recursive functions $C,U$ such thatHere $C$ is zero exactly on codes of valid halting computation histories for the chosen program and input, and $U$ extracts the final output. Coding finite configurations and finite histories makes checking every local step a bounded primitive recursive operation. If a computation halts, some history code passes and every passing code has the same output; if it does not halt, none passes. This is the usual normal-form version with the program index fixed; a universal predicate can also retain that index as an input.