Recursive_Function_uses_One_Minimization
Disprovedcomputabilityproofwikirecursion-theory
Every recursive function can be obtained from the basic primitive recursive functions using * substitution * primitive recursion * at most one minimization on a function.
Preamble
import Mathlib.Computability.Partrec import Mathlib.Computability.Primrec
Formal statement
theorem Recursive_Function_uses_One_Minimization : ∀ (f : ℕ →. ℕ), Nat.Partrec f → ∃ (g : ℕ → ℕ), Nat.Primrec g ∧ ∀ n, f n = Nat.rfind (fun m => some (decide (g (Nat.pair n m) = 0))) := by sorry
Source