English
There exists a computable f: Code → ℕ → Code such that for all c, n, x, eval f(c,n) x = eval c (pair n x).
Русский
Существует вычислимая функция f: Code → ℕ → Code такая, что для всех c, n, x выполняется eval f(c,n) x = eval c (pair n x).
LaTeX
$$$\\exists f:\\, Code \\to\\mathbb{N} \\to Code\\,\\bigl(\\mathrm{Computable}_2\\ f\\bigr) \\wedge \\forall c\\,\\forall n\\,\\forall x,\\ \\mathrm{eval}(f\\,c\\,n)\\,x = \\mathrm{eval}\\,c\\ (\\mathrm{Nat.pair}(n,x))$$$
Lean4
/-- The $S_n^m$ theorem: There is a computable function, namely `Nat.Partrec.Code.curry`, that takes a
program and a ℕ `n`, and returns a new program using `n` as the first argument.
-/
theorem smn : ∃ f : Code → ℕ → Code, Computable₂ f ∧ ∀ c n x, eval (f c n) x = eval c (Nat.pair n x) :=
⟨curry, Primrec₂.to_comp primrec₂_curry, eval_curry⟩
