tail — Mathlib

English

If f is Primrec' then its tail is Primrec' on the successor length.

Русский

Если f примитивно-рекурсивна, то ее хвост относится на следующую длину вектора.

LaTeX

$$$$ (\\text{tail}):\\, (\\forall n, f)\\ \\Rightarrow\\ (\\forall n+1, \\text{tail}(f)) $$$$

Lean4

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

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