English
If pf is a Partrec' on a vector-valued function, then the corresponding scalar Partrec function on the encoded input exists; i.e., Partrec' f implies Partrec f when f takes a vector input encoded as a single natural.
Русский
Если pf — частично вычислимая функция над вектором, то существует соответствующая скалярная частично вычислимая функция; то есть Partrec' f предполагает Partrec f для входа, закодированного в одно натуральное число.
LaTeX
$$$$\forall {n,f},\; \mathrm{Partrec'}(f) \Rightarrow \mathrm{Partrec}(f).$$$$
Lean4
theorem to_part {n f} (pf : @Partrec' n f) : _root_.Partrec f := by
induction pf with
| prim hf => exact hf.to_prim.to_comp
| comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
| rfind _ hf =>
have := hf.comp (vector_cons.comp snd fst)
have := ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp this).to₂.partrec₂
exact _root_.Partrec.rfind this
