English
If f is Partrec' on n and g is Partrec' on (n+1), then the composed mapping fun v => Part.map (λ a => g (a :: v)) (f v) is Partrec' on n.
Русский
Если f — Partrec' на n и g — Partrec' на (n+1), то отображение v ↦ Part.map(λa, g(a :: v)) (f v) есть Partrec' на n.
LaTeX
$$$$\forall \{n\} \{f : \mathrm{PFun} (\mathrm{List.Vector} \mathbb{N} n) \mathbb{N}\} \{g : \mathrm{List.Vector} \mathbb{N} (n+1) \to \mathbb{N}\},\; \mathrm{Partrec'}(f) \to \mathrm{Partrec'}((n+1)\,g) \to \mathrm{Partrec'}\Bigl(\lambda v. \mathrm{Part}.map( (\lambda a. g(a ::ᵥ v)) )(f v)\Bigr).$$$$
Lean4
protected theorem map {n f} {g : List.Vector ℕ (n + 1) → ℕ} (hf : @Partrec' n f) (hg : @Partrec' (n + 1) g) :
@Partrec' n fun v => (f v).map fun a => g (a ::ᵥ v) := by simpa [(Part.bind_some_eq_map _ _).symm] using hf.bind hg
