Smn for the fixed acceptable numbering

Generate the following finite program. Parse its input as exactly an n-entry tuple of canonical numerals, entering an endless walk on failure. Retain those entries, write the literal canonical numerals $a_1,\dots ,a_m$ into new zones, and form the tuple with arity header $1^{m+n}0$, the m parameter blocks and the n retained input blocks. Each word block w is written as $1^{\mathrm{\mid }w\mathrm{\mid }}0w$. Run the raw evaluator on program e and that tuple word, with canonical output normalization. F1 implements the evaluator and the literal-writing chains; F2 implements the parser and tuple construction. Encode the resulting finite table and return its length-lex index. This defines $s_m^n$.

Code generation does not execute e. It scans only the finite arities, parameter numerals and fixed evaluator template, expanding each literal into a finite writing-state chain. It therefore halts for every allowed input, even when e is malformed or represents a divergent function. A single generator handles all m,n by loops over their finite numerals and parameter list. On malformed generator inputs it may return a fixed index; the stated compiler uses only the valid ones.

On the tuple for $\mathbf{y}$, the generated parser succeeds and supplies exactly $E(\mathrm{bin}(\mathbf{a}),\mathrm{bin}(\mathbf{y}))$ to the raw e-evaluator. Every preprocessing operation terminates. Thus its subsequent run has exactly the canonical output of that evaluation or diverges exactly when that evaluation is undefined. This proves the displayed equality of domains and values, including zero parameters, zero-valued inputs, malformed e and empty partial domains. For m=n=1 the construction simply prepends one stored numeral and changes the arity header to two.