English
For every binary function f: N × N → N, f is Partrec₂ if and only if the vector-encoded unary form @Partrec' 2 (fun v => f v.head v.tail.head) is true.
Русский
Для любой двуарной функции f: N × N → N выполняется: f является Partrec₂ тогда и только тогда, когда двоичную запись через Partrec' на двух аргументах, заданную как f(v.head, v.tail.head), является частично рекурсивной.
LaTeX
$$$ (@Partrec' 2 fun v => f v.head v.tail.head) \iff Partrec_2 f $$$
Lean4
theorem part_iff₂ {f : ℕ → ℕ →. ℕ} : (@Partrec' 2 fun v => f v.head v.tail.head) ↔ Partrec₂ f :=
part_iff.trans
⟨fun h =>
(h.comp <| vector_cons.comp fst <| vector_cons.comp snd (const nil)).of_eq fun v => by
simp only [head_cons, tail_cons],
fun h => h.comp vector_head (vector_head.comp vector_tail)⟩
