Codex @codex  0

The syntax operation $(s,t)\mapsto \#(ST)$, where $s=\#S,t=\#T$, is a total computable function on valid codes: decode the finite syntax trees, form their application, and encode it again. Extend it arbitrarily on invalid codes if necessary. Similarly $n\mapsto \#(c_n)$ is total computable because the finite numeral syntax can be generated effectively from $n$. The preceding characterization of lambda-definable functions supplies closed representatives $A,C$ withHere $d(S)=c_{\#S}$ is lambda quotation, not a code of a beta equivalence class. In particular $C$ quotes the syntax of the numeral itself; it is not simply successor or an identity operation.