English
For f,g : α →. σ with f,g Nat.Partrec, there exists k : α →. σ with k Nat.Partrec such that for all a, x ∈ k a iff x ∈ f a ∨ x ∈ g a, and Dom(ka) = Dom(fa) ∪ Dom(ga).
Русский
Для f, g : α →. σ, где f,g частично рекурсивны, существует k : α →. σ, для которого k(a) определено тогда и только тогда, когда x принадлежит f(a) или g(a), и домен k(a) равен объединению доменов f(a) и g(a).
LaTeX
$$$\\exists k : α →. σ, Nat.Partrec k ∧ \\forall a, (\\forall x \\in k a, x \\in f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)$$$
Lean4
theorem merge' {f g : α →. σ} (hf : Partrec f) (hg : Partrec g) :
∃ k : α →. σ, Partrec k ∧ ∀ a, (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom) :=
by
let ⟨k, hk, H⟩ := Nat.Partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_iff.1 hg)
let k' (a : α) := (k (encode a)).bind fun n => (decode (α := σ) n : Part σ)
refine ⟨k', ((nat_iff.2 hk).comp Computable.encode).bind (Computable.decode.ofOption.comp snd).to₂, fun a => ?_⟩
have : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a := by
intro x h'
simp only [k', mem_coe, mem_bind_iff, Option.mem_def] at h'
obtain ⟨n, hn, hx⟩ := h'
have := (H _).1 _ hn
simp only [decode₂_encode, coe_some, bind_some, mem_map_iff] at this
obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this <;> simp only [encodek, Option.some_inj] at hx <;> rw [hx] at ha
· exact Or.inl ha
· exact Or.inr ha
refine ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, ?_⟩⟩
intro h
rw [bind_dom]
have hk : (k (encode a)).Dom := (H _).2.2 (by simpa only [encodek₂, bind_some, coe_some] using h)
exists hk
simp only [mem_map_iff, mem_coe, mem_bind_iff, Option.mem_def] at H
obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩ <;> simp only [e.symm, encodek, coe_some, some_dom]
