关于陶哲轩《Analysis I》中递归序列相关“procedure”的技术问询

最近啃陶哲轩的《Analysis I》，读到他定义递归序列的段落时卡壳了——有两个疑问没搞明白。虽说之前已经有不少人针对这段内容提问过，但我的问题和那些都不一样。先把目前能明确的第一个问题列出来，之后我会附上这段原文，还有陶哲轩后来对他在这里证明的命题的形式化表述：

• 想彻底弄清楚，陶哲轩在段落第一句里提到的procedure到底指的是什么？

（注：原内容中第二个问题及后续的原文段落、命题形式化表述未完整粘贴）

备注：内容来源于stack exchange，提问作者Princess Mia