Not_All_URM_Computable_Functions_are_Primitive_Recursive
Provedcomputabilityprimitive-recursive-functionsproofwiki
There exist URM computable functions which are not primitive recursive.
Preamble
import Mathlib.Computability.Primrec import Mathlib.Computability.Partrec
Formal statement
theorem Not_All_URM_Computable_Functions_are_Primitive_Recursive : ∃ (f : ℕ → ℕ), Nat.Partrec (↑f) ∧ ¬Nat.Primrec f := by sorry
Source