English
Given two partial recursive functions f and g and a compatibility condition H, there exists k such that k(a) captures exactly the union of f(a) and g(a), and membership in k(a) is equivalent to membership in f(a) or g(a).
Русский
Пусть есть две частично рекурсивные функции f и g и условие совместимости H; тогда существует k, такой что k(a) содержит ровно объединение f(a) и g(a), и x ∈ k(a) эквивалентно x ∈ f(a) или x ∈ g(a).
LaTeX
$$$\\exists k : α →. σ, Partrec k ∧ ∀ a x, x ∈ k a \\leftrightarrow x ∈ f a ∨ x ∈ g a$$$
Lean4
theorem merge {f g : α →. σ} (hf : Partrec f) (hg : Partrec g) (H : ∀ (a), ∀ x ∈ f a, ∀ y ∈ g a, x = y) :
∃ k : α →. σ, Partrec k ∧ ∀ a x, x ∈ k a ↔ x ∈ f a ∨ x ∈ g a :=
let ⟨k, hk, K⟩ := merge' hf hg
⟨k, hk, fun a x =>
⟨(K _).1 _, fun h => by
have : (k a).Dom := (K _).2.2 (h.imp Exists.fst Exists.fst)
refine ⟨this, ?_⟩
rcases h with h | h <;> rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'
· exact mem_unique h' h
· exact (H _ _ h _ h').symm
· exact H _ _ h' _ h
· exact mem_unique h' h⟩⟩
