Function_Obtained_by_Minimization_from_URM_Computable_Functions
Provedcomputabilityproofwikiurm-programs
Let the function be a URM computable function. Let be the function obtained by minimization from thus . Then is also URM computable.
Preamble
import Mathlib.Computability.Partrec
Formal statement
theorem Function_Obtained_by_Minimization_from_URM_Computable_Functions (f : ℕ → ℕ → ℕ) (hf : Computable₂ f) : Nat.Partrec (fun n => Nat.rfind (fun m => some (decide (f n m = 0)))) := by sorry
Source