 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.