English
If f is Partrec' on (n+1)-tuples, then the function v ↦ Nat.rfindOpt (λ a. ofNat (Option ℕ) (f (a ::ᵥ v))) is Partrec' on n-tuples.
Русский
Если f — Partrec' на векторах размерности n+1, то функция v ↦ Nat.rfindOpt(λ a. some или none) является Partrec' на размерности n.
LaTeX
$$$$\forall {n} {f : \mathrm{List.Vector} \mathbb{N} (n+1) \to \mathbb{N}}, \; \mathrm{Nat.Partrec'}(f) \Rightarrow \mathrm{Nat.Partrec'}\Bigl(\lambda v. \mathrm{Nat}.rfindOpt(\lambda a. \mathrm{ofNat}(\mathrm{Option}\,\mathbb{N})(f(a ::ᵥ v)))\Bigr).$$$$
Lean4
protected theorem bind {n f g} (hf : @Partrec' n f) (hg : @Partrec' (n + 1) g) :
@Partrec' n fun v => (f v).bind fun a => g (a ::ᵥ v) :=
(@comp n (n + 1) g (fun i => Fin.cases f (fun i v => some (v.get i)) i) hg fun i =>
by
refine Fin.cases ?_ (fun i => ?_) i <;> simp [*]
exact prim (Nat.Primrec'.get _)).of_eq
fun v => by simp [mOfFn, Part.bind_assoc, pure]
