English
If f: α→ℕ and p: α→ℕ→Prop with decidable_rel, hf and hp primitive recursive, then x ↦ (f(x)).findGreatest(p(x)) is primitive recursive.
Русский
Если f: α→ℕ и p: α→ℕ→Prop с распознаваемым отношением, hf и hp примитивно вычисимы, то x ↦ (f(x)).findGreatest(p(x)) примитивно вычисима.
LaTeX
$$$\\forall {f:\\alpha\\to\\mathbb{N}}\\ {p:\\alpha\\to\\mathbb{N}\\to\\mathrm{Prop}} [DecidableRel p],\\ Primrec f\\to PrimrecRel p\\to Primrec (\\lambda x. (f\\,x).findGreatest(p\\,x))$$$
Lean4
theorem nat_findGreatest {f : α → ℕ} {p : α → ℕ → Prop} [DecidableRel p] (hf : Primrec f) (hp : PrimrecRel p) :
Primrec fun x => (f x).findGreatest (p x) :=
(nat_rec' (h := fun x nih => if p x (nih.1 + 1) then nih.1 + 1 else nih.2) hf (const 0)
(ite (hp.comp fst (snd |> fst.comp |> succ.comp)) (snd |> fst.comp |> succ.comp) (snd.comp snd))).of_eq
fun x => by induction f x <;> simp [Nat.findGreatest, *]
