tail — Mathlib

English

If f is Partrec' on vectors, then the tail function v ↦ f(v.tail) is Partrec'.

Русский

Если f — Partrec' на векторах, то tail(v) даёт Partrec' для v.tail.

LaTeX

$$$$\forall n,\; \mathrm{Nat.Partrec'}(f) \Rightarrow \mathrm{Nat.Partrec'}(\lambda v. f(v.tail)).$$$$

Lean4

theorem tail {n f} (hf : @Partrec' n f) : @Partrec' n.succ fun v => f v.tail :=
  (hf.comp _ fun i => @prim _ _ <| Nat.Primrec'.get i.succ).of_eq fun v => by simp; rw [← ofFn_get v.tail]; congr;
    funext i; simp

Похожие утверждения