English
For two natural-number partial recursive functions f and g, there exists a partial recursive h such that for every a, h(a) contains exactly the elements of f(a) or g(a), and the domain of h(a) is the union of the domains of f(a) and g(a).
Русский
Для двух частично рекурсивных функций f и g над Натами существует частично рекурсивная h так, чтобы для каждого a множество h(a) содержало ровно элементы f(a) или g(a), и домен h(a) равнялся объединению доменов f(a) и g(a).
LaTeX
$$$\\forall a, x,\\ x \\in h(a) \\iff x \\in f(a) \\lor x \\in g(a) \\quad\\land\\ (h(a)).Dom \\leftrightarrow (f(a)).Dom \\lor (g(a)).Dom$$$
Lean4
theorem merge' {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g) :
∃ h, Nat.Partrec h ∧ ∀ a, (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom) :=
by
obtain ⟨cf, rfl⟩ := Code.exists_code.1 hf
obtain ⟨cg, rfl⟩ := Code.exists_code.1 hg
have : Nat.Partrec fun n => Nat.rfindOpt fun k => cf.evaln k n <|> cg.evaln k n :=
Partrec.nat_iff.1
(Partrec.rfindOpt <|
Primrec.option_orElse.to_comp.comp (Code.primrec_evaln.to_comp.comp <| (snd.pair (const cf)).pair fst)
(Code.primrec_evaln.to_comp.comp <| (snd.pair (const cg)).pair fst))
refine ⟨_, this, fun n => ?_⟩
have :
∀ x ∈ rfindOpt fun k ↦ HOrElse.hOrElse (Code.evaln k cf n) fun _x ↦ Code.evaln k cg n,
x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n :=
by
intro x h
obtain ⟨k, e⟩ := Nat.rfindOpt_spec h
revert e
simp only [Option.mem_def]
rcases e' : cf.evaln k n with - | y <;> simp <;> intro e
· exact Or.inr (Code.evaln_sound e)
· subst y
exact Or.inl (Code.evaln_sound e')
refine ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, ?_⟩⟩
intro h
rw [Nat.rfindOpt_dom]
simp only [dom_iff_mem, Code.evaln_complete, Option.mem_def] at h
obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h
· refine ⟨k, x, ?_⟩
simp only [e, Option.orElse_some, Option.mem_def, Option.orElse_eq_orElse]
· refine ⟨k, ?_⟩
rcases cf.evaln k n with - | y
· exact ⟨x, by simp only [e, Option.mem_def, Option.orElse_eq_orElse, Option.orElse_none]⟩
· exact ⟨y, by simp only [Option.orElse_eq_orElse, Option.orElse_some, Option.mem_def]⟩
