English
A specialized composition: if f depends on the head of a vector and g is Partrec' on n, then f ∘ g is Partrec'.
Русский
Уточненная композиция: если f зависит от головы вектора, а g — Partrec' на n, то f ∘ g — Partrec'.
LaTeX
$$$$\forall {n} {f : PFun Nat Nat} {g : \mathrm{List.Vector} \mathbb{N} n \to \mathbb{N}}, \; \mathrm{Nat.Partrec'}(f.head) \to \mathrm{Nat.Partrec'}(\mathrm{PFun.lift} g) \to \mathrm{Nat.Partrec'}(\lambda v. f (g v)).$$$$
Lean4
theorem comp₁ {n} (f : ℕ →. ℕ) {g : List.Vector ℕ n → ℕ} (hf : @Partrec' 1 fun v => f v.head) (hg : @Partrec' n g) :
@Partrec' n fun v => f (g v) := by simpa using hf.comp' (Partrec'.cons hg Partrec'.nil)
