Finite witness array coding
= Finite witness array coding
In a <primitive recursion>, an existential representation of the step <function> may need a different witness tuple at every time. Code each coordinate of the finite witness array by a separate beta-function code pair. All row witnesses then have bounded remainder quantifiers under the bounded time quantifier, while the finitely many code pairs remain in the outer unrestricted existential block.