English
Every Primrec f is representable as a Primrec' function (conversion between notions).
Русский
Каждая Primrec f эквивалентна Primrec' f (преобразование между понятиями).
LaTeX
$$$\forall {n\ f},\ Primrec\ f \to\ @Primrec' n f$$
Lean4
theorem of_prim {n f} : Primrec f → @Primrec' n f :=
suffices ∀ f, Nat.Primrec f → @Primrec' 1 fun v => f v.head from fun hf =>
(pred.comp₁ _ <|
(this _ hf).comp₁ (fun m => Encodable.encode <| (@decode (List.Vector ℕ n) _ m).map f) Primrec'.encode).of_eq
fun i => by simp [encodek]
fun f hf => by
induction hf with
| zero => exact const 0
| succ => exact succ
| left => exact unpair₁ head
| right => exact unpair₂ head
| pair _ _ hf hg => exact natPair.comp₂ _ hf hg
| comp _ _ hf hg => exact hf.comp₁ _ hg
| prec _ _ hf hg =>
simpa using
prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
(hg.comp₁ _ <| natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
