English
A technical lemma describing how to construct a witness for merge' using encoded codes and decodings.
Русский
Техническая лемма о конструировании свидетеля для merge' с использованием кодирования и декодирования.
LaTeX
$$/* technical matching lemma for merge' (omitted for brevity) */$$
Lean4
theorem cond {c : α → Bool} {f : α →. σ} {g : α →. σ} (hc : Computable c) (hf : Partrec f) (hg : Partrec g) :
Partrec fun a => cond (c a) (f a) (g a) :=
let ⟨cf, ef⟩ := exists_code.1 hf
let ⟨cg, eg⟩ := exists_code.1 hg
((eval_part.comp (Computable.cond hc (const cf) (const cg)) Computable.encode).bind
((@Computable.decode σ _).comp snd).ofOption.to₂).of_eq
fun a => by cases c a <;> simp [ef, eg, encodek]
